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 ∈ 𝑹 → x y E -1 ⁢ z w E -1 = x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w E -1
3 mulcnsrec ⊢ z ∈ 𝑹 ∧ w ∈ 𝑹 ∧ v ∈ 𝑹 ∧ u ∈ 𝑹 → z w E -1 ⁢ v u E -1 = z ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 w ⋅ 𝑹 u w ⋅ 𝑹 v + 𝑹 z ⋅ 𝑹 u E -1
4 mulcnsrec ⊢ x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w ∈ 𝑹 ∧ y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w ∈ 𝑹 ∧ v ∈ 𝑹 ∧ u ∈ 𝑹 → x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w E -1 ⁢ v u E -1 = x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w ⋅ 𝑹 u y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w ⋅ 𝑹 v + 𝑹 x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w ⋅ 𝑹 u E -1
5 mulcnsrec ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ z ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 w ⋅ 𝑹 u ∈ 𝑹 ∧ w ⋅ 𝑹 v + 𝑹 z ⋅ 𝑹 u ∈ 𝑹 → x y E -1 ⁢ z ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 w ⋅ 𝑹 u w ⋅ 𝑹 v + 𝑹 z ⋅ 𝑹 u E -1 = x ⋅ 𝑹 z ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 w ⋅ 𝑹 u + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w ⋅ 𝑹 v + 𝑹 z ⋅ 𝑹 u y ⋅ 𝑹 z ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 w ⋅ 𝑹 u + 𝑹 x ⋅ 𝑹 w ⋅ 𝑹 v + 𝑹 z ⋅ 𝑹 u E -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