Theorem axmulcom 5199

Description: Multiplication of complex numbers is commutative. Axiom 10 of 25 for real and complex numbers, derived from ZF set theory.

Assertion

Ref	Expression
axmulcom	|- ((A e. CC /\ B e. CC) -> (A x. B) = (B x. A))

Proof of Theorem axmulcom

Step	Hyp	Ref	Expression
1		dfcnqs 5185	. 2 |- CC = ((R. X. R.)/.`'E)
2		mulcnsrec 5187	. 2 |- (((x e. R. /\ y e. R.) /\ (z e. R. /\ w e. R.)) -> ([<.x, y>.]`'E x. [<.z, w>.]`'E) = [<.((x .R z) +R (-1R .R (y .R w))), ((y .R z) +R (x .R w))>.]`'E)
3		mulcnsrec 5187	. 2 |- (((z e. R. /\ w e. R.) /\ (x e. R. /\ y e. R.)) -> ([<.z, w>.]`'E x. [<.x, y>.]`'E) = [<.((z .R x) +R (-1R .R (w .R y))), ((w .R x) +R (z .R y))>.]`'E)
4		visset 1788	. . . 4 |- x e. V
5		visset 1788	. . . 4 |- z e. V
6	4, 5	mulcomsr 5121	. . 3 |- (x .R z) = (z .R x)
7		visset 1788	. . . . 5 |- y e. V
8		visset 1788	. . . . 5 |- w e. V
9	7, 8	mulcomsr 5121	. . . 4 |- (y .R w) = (w .R y)
10	9	opreq2i 3911	. . 3 |- (-1R .R (y .R w)) = (-1R .R (w .R y))
11	6, 10	opreq12i 3912	. 2 |- ((x .R z) +R (-1R .R (y .R w))) = ((z .R x) +R (-1R .R (w .R y)))
12	7, 5	mulcomsr 5121	. . . 4 |- (y .R z) = (z .R y)
13	4, 8	mulcomsr 5121	. . . 4 |- (x .R w) = (w .R x)
14	12, 13	opreq12i 3912	. . 3 |- ((y .R z) +R (x .R w)) = ((z .R y) +R (w .R x))
15		oprex 3922	. . . 4 |- (z .R y) e. V
16		oprex 3922	. . . 4 |- (w .R x) e. V
17	15, 16	addcomsr 5119	. . 3 |- ((z .R y) +R (w .R x)) = ((w .R x) +R (z .R y))
18	14, 17	eqtr 1471	. 2 |- ((y .R z) +R (x .R w)) = ((w .R x) +R (z .R y))
19	1, 2, 3, 11, 18	ecoprcom 4257	1 |- ((A e. CC /\ B e. CC) -> (A x. B) = (B x. A))

Syntax hints:   -> wi 3   /\ wa 223   = wceq 1099   e. wcel 1105  Ecep 2792  `'ccnv 3132  (class class class)co 3902  R.cnr 4916  -1Rcm1r 4919   +R cplr 4920   .R cmr 4921  CCcc 5155   x. cmul 5162

This theorem is referenced by:  mulcomt 5229  adddirt 5242  mulcom 5246  mulid2t 5340  mul12t 5341  mul23t 5342  muladdt 5344  subdirt 5351  mul02t 5367  mulneg2t 5375  recextlem1 5606  mulcan 5610  mulcan2t 5613  divmul3t 5629  recid2t 5650  divrec2t 5654  div23t 5656  div13t 5657  div12t 5658  divcan4t 5670  rec11rt 5686  divmul13t 5689  divmul24t 5690  divdivdivt 5692  prodgt02t 5734  prodge02t 5736  ltmul2t 5738  lemul2t 5740  lemul2it 5746  lemul2itOLD 5747  ltmulgt12t 5754  ltmuldiv2t 5769  ltdivmul2t 5772  lt2mul2divt 5773  ledivmul2t 5774  lemuldiv2t 5776  times2t 5903  subsqt 6524  crutOLD 6620  replimtOLD 6644  imret 6661  imcjt 6705  abscjt 6720  sqabsaddt 6734  sqabssubt 6735  bccmplt 6851  fsummulc2 6923  caucvg3a 7051  caucvg3lem 7053  geolimilem 7121  cvgratlem1ALT 7133  cvgratlem1 7136  fsum0diag4 7147  efcltlem1 7197  efexpt 7265  efeult 7342  sin2tt 7355  demoivre 7377  ablmul 8016  nvscom 8128  nv1 8180  ipblnfi 8382  sinmpi 8526  cosmpi 8527  circgrpOLD 8571  efper 8582  msra3 8825  hvmulcomt 9061  norm1t 9272  pjthlem7 9354  h1de2b 9606  h1de2bOLD 9607  homul12t 9862  kbmult 10009  riesz3 10124  riesz1t 10127  branmfnt 10165  kbass2t 10176  kbass4t 10178  strlem1 10301

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830  ax-inf2 4549

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-reu 1627  df-rab 1628  df-v 1787  df-sbc 1913  df-csb 1973  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-pss 2026  df-nul 2252  df-if 2333  df-pw 2373  df-sn 2383  df-pr 2384  df-tp 2386  df-op 2387  df-uni 2472  df-int 2502  df-iun 2536  df-br 2588  df-opab 2635  df-tr 2649  df-eprel 2794  df-id 2797  df-po 2804  df-so 2814  df-fr 2880  df-we 2897  df-ord 2914  df-on 2915  df-lim 2916  df-suc 2917  df-om 3095  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-f 3157  df-fv 3161  df-rdg 3871  df-opr 3904  df-oprab 3905  df-1st 4017  df-2nd 4018  df-1o 4071  df-oadd 4073  df-omul 4074  df-er 4199  df-ec 4201  df-qs 4204  df-ni 4923  df-pli 4924  df-mi 4925  df-lti 4926  df-plpq 4958  df-mpq 4959  df-enq 4960  df-nq 4961  df-plq 4962  df-mq 4963  df-rq 4964  df-ltq 4965  df-1q 4966  df-np 5009  df-plp 5011  df-mp 5012  df-ltp 5013  df-plpr 5087  df-mpr 5088  df-enr 5089  df-nr 5090  df-plr 5091  df-mr 5092  df-c 5163  df-mul 5169

Copyright terms: Public domain