Metamath Proof Explorer

Theorem axmulass

Description: Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass . (Contributed by NM, 3-Sep-1995) (New usage is discouraged.)

Ref Expression
Assertion axmulass ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A⁢B⁢C=A⁢B⁢C

Proof

Step Hyp Ref Expression
1 dfcnqs ⊢ℂ=𝑹×𝑹/E-1
2 mulcnsrec ⊢x∈𝑹∧y∈𝑹∧z∈𝑹∧w∈𝑹→xyE-1⁢zwE-1=x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹wy⋅𝑹z+𝑹x⋅𝑹wE-1
3 mulcnsrec ⊢z∈𝑹∧w∈𝑹∧v∈𝑹∧u∈𝑹→zwE-1⁢vuE-1=z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹uw⋅𝑹v+𝑹z⋅𝑹uE-1
4 mulcnsrec ⊢x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w∈𝑹∧y⋅𝑹z+𝑹x⋅𝑹w∈𝑹∧v∈𝑹∧u∈𝑹→x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹wy⋅𝑹z+𝑹x⋅𝑹wE-1⁢vuE-1=x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹z+𝑹x⋅𝑹w⋅𝑹uy⋅𝑹z+𝑹x⋅𝑹w⋅𝑹v+𝑹x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹uE-1
5 mulcnsrec ⊢x∈𝑹∧y∈𝑹∧z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹u∈𝑹∧w⋅𝑹v+𝑹z⋅𝑹u∈𝑹→xyE-1⁢z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹uw⋅𝑹v+𝑹z⋅𝑹uE-1=x⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹u+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹z⋅𝑹uy⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹u+𝑹x⋅𝑹w⋅𝑹v+𝑹z⋅𝑹uE-1
6 mulclsr ⊢x∈𝑹∧z∈𝑹→x⋅𝑹z∈𝑹
7 m1r ⊢-1𝑹∈𝑹
8 mulclsr ⊢y∈𝑹∧w∈𝑹→y⋅𝑹w∈𝑹
9 mulclsr ⊢-1𝑹∈𝑹∧y⋅𝑹w∈𝑹→-1𝑹⋅𝑹y⋅𝑹w∈𝑹
10 7 8 9 sylancr ⊢y∈𝑹∧w∈𝑹→-1𝑹⋅𝑹y⋅𝑹w∈𝑹
11 addclsr ⊢x⋅𝑹z∈𝑹∧-1𝑹⋅𝑹y⋅𝑹w∈𝑹→x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w∈𝑹
12 6 10 11 syl2an ⊢x∈𝑹∧z∈𝑹∧y∈𝑹∧w∈𝑹→x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w∈𝑹
13 12 an4s ⊢x∈𝑹∧y∈𝑹∧z∈𝑹∧w∈𝑹→x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w∈𝑹
14 mulclsr ⊢y∈𝑹∧z∈𝑹→y⋅𝑹z∈𝑹
15 mulclsr ⊢x∈𝑹∧w∈𝑹→x⋅𝑹w∈𝑹
16 addclsr ⊢y⋅𝑹z∈𝑹∧x⋅𝑹w∈𝑹→y⋅𝑹z+𝑹x⋅𝑹w∈𝑹
17 14 15 16 syl2anr ⊢x∈𝑹∧w∈𝑹∧y∈𝑹∧z∈𝑹→y⋅𝑹z+𝑹x⋅𝑹w∈𝑹
18 17 an42s ⊢x∈𝑹∧y∈𝑹∧z∈𝑹∧w∈𝑹→y⋅𝑹z+𝑹x⋅𝑹w∈𝑹
19 13 18 jca ⊢x∈𝑹∧y∈𝑹∧z∈𝑹∧w∈𝑹→x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w∈𝑹∧y⋅𝑹z+𝑹x⋅𝑹w∈𝑹
20 mulclsr ⊢z∈𝑹∧v∈𝑹→z⋅𝑹v∈𝑹
21 mulclsr ⊢w∈𝑹∧u∈𝑹→w⋅𝑹u∈𝑹
22 mulclsr ⊢-1𝑹∈𝑹∧w⋅𝑹u∈𝑹→-1𝑹⋅𝑹w⋅𝑹u∈𝑹
23 7 21 22 sylancr ⊢w∈𝑹∧u∈𝑹→-1𝑹⋅𝑹w⋅𝑹u∈𝑹
24 addclsr ⊢z⋅𝑹v∈𝑹∧-1𝑹⋅𝑹w⋅𝑹u∈𝑹→z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹u∈𝑹
25 20 23 24 syl2an ⊢z∈𝑹∧v∈𝑹∧w∈𝑹∧u∈𝑹→z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹u∈𝑹
26 25 an4s ⊢z∈𝑹∧w∈𝑹∧v∈𝑹∧u∈𝑹→z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹u∈𝑹
27 mulclsr ⊢w∈𝑹∧v∈𝑹→w⋅𝑹v∈𝑹
28 mulclsr ⊢z∈𝑹∧u∈𝑹→z⋅𝑹u∈𝑹
29 addclsr ⊢w⋅𝑹v∈𝑹∧z⋅𝑹u∈𝑹→w⋅𝑹v+𝑹z⋅𝑹u∈𝑹
30 27 28 29 syl2anr ⊢z∈𝑹∧u∈𝑹∧w∈𝑹∧v∈𝑹→w⋅𝑹v+𝑹z⋅𝑹u∈𝑹
31 30 an42s ⊢z∈𝑹∧w∈𝑹∧v∈𝑹∧u∈𝑹→w⋅𝑹v+𝑹z⋅𝑹u∈𝑹
32 26 31 jca ⊢z∈𝑹∧w∈𝑹∧v∈𝑹∧u∈𝑹→z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹u∈𝑹∧w⋅𝑹v+𝑹z⋅𝑹u∈𝑹
33 ovex ⊢x⋅𝑹z⋅𝑹v∈V
34 ovex ⊢x⋅𝑹-1𝑹⋅𝑹w⋅𝑹u∈V
35 ovex ⊢-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v∈V
36 addcomsr ⊢f+𝑹g=g+𝑹f
37 addasssr ⊢f+𝑹g+𝑹h=f+𝑹g+𝑹h
38 ovex ⊢-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u∈V
39 33 34 35 36 37 38 caov42 ⊢x⋅𝑹z⋅𝑹v+𝑹x⋅𝑹-1𝑹⋅𝑹w⋅𝑹u+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u=x⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u+𝑹x⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
40 distrsr ⊢x⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹u=x⋅𝑹z⋅𝑹v+𝑹x⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
41 distrsr ⊢y⋅𝑹w⋅𝑹v+𝑹z⋅𝑹u=y⋅𝑹w⋅𝑹v+𝑹y⋅𝑹z⋅𝑹u
42 41 oveq2i ⊢-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹z⋅𝑹u=-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹y⋅𝑹z⋅𝑹u
43 distrsr ⊢-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹y⋅𝑹z⋅𝑹u=-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u
44 42 43 eqtri ⊢-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹z⋅𝑹u=-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u
45 40 44 oveq12i ⊢x⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹u+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹z⋅𝑹u=x⋅𝑹z⋅𝑹v+𝑹x⋅𝑹-1𝑹⋅𝑹w⋅𝑹u+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u
46 vex ⊢x∈V
47 7 elexi ⊢-1𝑹∈V
48 vex ⊢z∈V
49 mulcomsr ⊢f⋅𝑹g=g⋅𝑹f
50 distrsr ⊢f⋅𝑹g+𝑹h=f⋅𝑹g+𝑹f⋅𝑹h
51 ovex ⊢y⋅𝑹w∈V
52 vex ⊢v∈V
53 mulasssr ⊢f⋅𝑹g⋅𝑹h=f⋅𝑹g⋅𝑹h
54 46 47 48 49 50 51 52 53 caovdilem ⊢x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v=x⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v
55 mulasssr ⊢y⋅𝑹w⋅𝑹v=y⋅𝑹w⋅𝑹v
56 55 oveq2i ⊢-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v=-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v
57 56 oveq2i ⊢x⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v=x⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v
58 54 57 eqtri ⊢x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v=x⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v
59 vex ⊢y∈V
60 vex ⊢w∈V
61 vex ⊢u∈V
62 59 46 48 49 50 60 61 53 caovdilem ⊢y⋅𝑹z+𝑹x⋅𝑹w⋅𝑹u=y⋅𝑹z⋅𝑹u+𝑹x⋅𝑹w⋅𝑹u
63 62 oveq2i ⊢-1𝑹⋅𝑹y⋅𝑹z+𝑹x⋅𝑹w⋅𝑹u=-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u+𝑹x⋅𝑹w⋅𝑹u
64 distrsr ⊢-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u+𝑹x⋅𝑹w⋅𝑹u=-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u+𝑹-1𝑹⋅𝑹x⋅𝑹w⋅𝑹u
65 ovex ⊢w⋅𝑹u∈V
66 47 46 65 49 53 caov12 ⊢-1𝑹⋅𝑹x⋅𝑹w⋅𝑹u=x⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
67 66 oveq2i ⊢-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u+𝑹-1𝑹⋅𝑹x⋅𝑹w⋅𝑹u=-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u+𝑹x⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
68 64 67 eqtri ⊢-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u+𝑹x⋅𝑹w⋅𝑹u=-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u+𝑹x⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
69 63 68 eqtri ⊢-1𝑹⋅𝑹y⋅𝑹z+𝑹x⋅𝑹w⋅𝑹u=-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u+𝑹x⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
70 58 69 oveq12i ⊢x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹z+𝑹x⋅𝑹w⋅𝑹u=x⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹z⋅𝑹u+𝑹x⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
71 39 45 70 3eqtr4ri ⊢x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹-1𝑹⋅𝑹y⋅𝑹z+𝑹x⋅𝑹w⋅𝑹u=x⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹u+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹v+𝑹z⋅𝑹u
72 ovex ⊢y⋅𝑹z⋅𝑹v∈V
73 ovex ⊢y⋅𝑹-1𝑹⋅𝑹w⋅𝑹u∈V
74 ovex ⊢x⋅𝑹w⋅𝑹v∈V
75 ovex ⊢x⋅𝑹z⋅𝑹u∈V
76 72 73 74 36 37 75 caov42 ⊢y⋅𝑹z⋅𝑹v+𝑹y⋅𝑹-1𝑹⋅𝑹w⋅𝑹u+𝑹x⋅𝑹w⋅𝑹v+𝑹x⋅𝑹z⋅𝑹u=y⋅𝑹z⋅𝑹v+𝑹x⋅𝑹w⋅𝑹v+𝑹x⋅𝑹z⋅𝑹u+𝑹y⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
77 distrsr ⊢y⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹u=y⋅𝑹z⋅𝑹v+𝑹y⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
78 distrsr ⊢x⋅𝑹w⋅𝑹v+𝑹z⋅𝑹u=x⋅𝑹w⋅𝑹v+𝑹x⋅𝑹z⋅𝑹u
79 77 78 oveq12i ⊢y⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹u+𝑹x⋅𝑹w⋅𝑹v+𝑹z⋅𝑹u=y⋅𝑹z⋅𝑹v+𝑹y⋅𝑹-1𝑹⋅𝑹w⋅𝑹u+𝑹x⋅𝑹w⋅𝑹v+𝑹x⋅𝑹z⋅𝑹u
80 59 46 48 49 50 60 52 53 caovdilem ⊢y⋅𝑹z+𝑹x⋅𝑹w⋅𝑹v=y⋅𝑹z⋅𝑹v+𝑹x⋅𝑹w⋅𝑹v
81 46 47 48 49 50 51 61 53 caovdilem ⊢x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹u=x⋅𝑹z⋅𝑹u+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹u
82 mulasssr ⊢y⋅𝑹w⋅𝑹u=y⋅𝑹w⋅𝑹u
83 82 oveq2i ⊢-1𝑹⋅𝑹y⋅𝑹w⋅𝑹u=-1𝑹⋅𝑹y⋅𝑹w⋅𝑹u
84 47 59 65 49 53 caov12 ⊢-1𝑹⋅𝑹y⋅𝑹w⋅𝑹u=y⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
85 83 84 eqtri ⊢-1𝑹⋅𝑹y⋅𝑹w⋅𝑹u=y⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
86 85 oveq2i ⊢x⋅𝑹z⋅𝑹u+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹u=x⋅𝑹z⋅𝑹u+𝑹y⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
87 81 86 eqtri ⊢x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹u=x⋅𝑹z⋅𝑹u+𝑹y⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
88 80 87 oveq12i ⊢y⋅𝑹z+𝑹x⋅𝑹w⋅𝑹v+𝑹x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹u=y⋅𝑹z⋅𝑹v+𝑹x⋅𝑹w⋅𝑹v+𝑹x⋅𝑹z⋅𝑹u+𝑹y⋅𝑹-1𝑹⋅𝑹w⋅𝑹u
89 76 79 88 3eqtr4ri ⊢y⋅𝑹z+𝑹x⋅𝑹w⋅𝑹v+𝑹x⋅𝑹z+𝑹-1𝑹⋅𝑹y⋅𝑹w⋅𝑹u=y⋅𝑹z⋅𝑹v+𝑹-1𝑹⋅𝑹w⋅𝑹u+𝑹x⋅𝑹w⋅𝑹v+𝑹z⋅𝑹u
90 1 2 3 4 5 19 32 71 89 ecovass ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A⁢B⁢C=A⁢B⁢C