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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) · 𝐶 ) = ( 𝐴 · ( 𝐵 · 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 dfcnqs ⊢ ℂ = ( ( R × R ) / ◡ E )
2 mulcnsrec ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ E · [ ⟨ 𝑧 , 𝑤 ⟩ ] ◡ E ) = [ ⟨ ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) , ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ⟩ ] ◡ E )
3 mulcnsrec ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ◡ E · [ ⟨ 𝑣 , 𝑢 ⟩ ] ◡ E ) = [ ⟨ ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) , ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ⟩ ] ◡ E )
4 mulcnsrec ⊢ ( ( ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ∈ R ∧ ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( [ ⟨ ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) , ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ⟩ ] ◡ E · [ ⟨ 𝑣 , 𝑢 ⟩ ] ◡ E ) = [ ⟨ ( ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ·R 𝑣 ) +R ( -1R ·R ( ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ·R 𝑢 ) ) ) , ( ( ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ·R 𝑣 ) +R ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ·R 𝑢 ) ) ⟩ ] ◡ E )
5 mulcnsrec ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ∈ R ∧ ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ∈ R ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ E · [ ⟨ ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) , ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ⟩ ] ◡ E ) = [ ⟨ ( ( 𝑥 ·R ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) +R ( -1R ·R ( 𝑦 ·R ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ) ) ) , ( ( 𝑦 ·R ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) +R ( 𝑥 ·R ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ) ) ⟩ ] ◡ E )
6 mulclsr ⊢ ( ( 𝑥 ∈ R ∧ 𝑧 ∈ R ) → ( 𝑥 ·R 𝑧 ) ∈ R )
7 m1r ⊢ -1R ∈ R
8 mulclsr ⊢ ( ( 𝑦 ∈ R ∧ 𝑤 ∈ R ) → ( 𝑦 ·R 𝑤 ) ∈ R )
9 mulclsr ⊢ ( ( -1R ∈ R ∧ ( 𝑦 ·R 𝑤 ) ∈ R ) → ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ∈ R )
10 7 8 9 sylancr ⊢ ( ( 𝑦 ∈ R ∧ 𝑤 ∈ R ) → ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ∈ R )
11 addclsr ⊢ ( ( ( 𝑥 ·R 𝑧 ) ∈ R ∧ ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ∈ R ) → ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ∈ R )
12 6 10 11 syl2an ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑧 ∈ R ) ∧ ( 𝑦 ∈ R ∧ 𝑤 ∈ R ) ) → ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ∈ R )
13 12 an4s ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ) → ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ∈ R )
14 mulclsr ⊢ ( ( 𝑦 ∈ R ∧ 𝑧 ∈ R ) → ( 𝑦 ·R 𝑧 ) ∈ R )
15 mulclsr ⊢ ( ( 𝑥 ∈ R ∧ 𝑤 ∈ R ) → ( 𝑥 ·R 𝑤 ) ∈ R )
16 addclsr ⊢ ( ( ( 𝑦 ·R 𝑧 ) ∈ R ∧ ( 𝑥 ·R 𝑤 ) ∈ R ) → ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ∈ R )
17 14 15 16 syl2anr ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑦 ∈ R ∧ 𝑧 ∈ R ) ) → ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ∈ R )
18 17 an42s ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ) → ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ∈ R )
19 13 18 jca ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ) → ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ∈ R ∧ ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ∈ R ) )
20 mulclsr ⊢ ( ( 𝑧 ∈ R ∧ 𝑣 ∈ R ) → ( 𝑧 ·R 𝑣 ) ∈ R )
21 mulclsr ⊢ ( ( 𝑤 ∈ R ∧ 𝑢 ∈ R ) → ( 𝑤 ·R 𝑢 ) ∈ R )
22 mulclsr ⊢ ( ( -1R ∈ R ∧ ( 𝑤 ·R 𝑢 ) ∈ R ) → ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ∈ R )
23 7 21 22 sylancr ⊢ ( ( 𝑤 ∈ R ∧ 𝑢 ∈ R ) → ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ∈ R )
24 addclsr ⊢ ( ( ( 𝑧 ·R 𝑣 ) ∈ R ∧ ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ∈ R ) → ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ∈ R )
25 20 23 24 syl2an ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑣 ∈ R ) ∧ ( 𝑤 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ∈ R )
26 25 an4s ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ∈ R )
27 mulclsr ⊢ ( ( 𝑤 ∈ R ∧ 𝑣 ∈ R ) → ( 𝑤 ·R 𝑣 ) ∈ R )
28 mulclsr ⊢ ( ( 𝑧 ∈ R ∧ 𝑢 ∈ R ) → ( 𝑧 ·R 𝑢 ) ∈ R )
29 addclsr ⊢ ( ( ( 𝑤 ·R 𝑣 ) ∈ R ∧ ( 𝑧 ·R 𝑢 ) ∈ R ) → ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ∈ R )
30 27 28 29 syl2anr ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑢 ∈ R ) ∧ ( 𝑤 ∈ R ∧ 𝑣 ∈ R ) ) → ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ∈ R )
31 30 an42s ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ∈ R )
32 26 31 jca ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ∈ R ∧ ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ∈ R ) )
33 ovex ⊢ ( 𝑥 ·R ( 𝑧 ·R 𝑣 ) ) ∈ V
34 ovex ⊢ ( 𝑥 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ∈ V
35 ovex ⊢ ( -1R ·R ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) ) ) ∈ V
36 addcomsr ⊢ ( 𝑓 +R 𝑔 ) = ( 𝑔 +R 𝑓 )
37 addasssr ⊢ ( ( 𝑓 +R 𝑔 ) +R ℎ ) = ( 𝑓 +R ( 𝑔 +R ℎ ) )
38 ovex ⊢ ( -1R ·R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) ∈ V
39 33 34 35 36 37 38 caov42 ⊢ ( ( ( 𝑥 ·R ( 𝑧 ·R 𝑣 ) ) +R ( 𝑥 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) +R ( ( -1R ·R ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) ) ) +R ( -1R ·R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) ) ) = ( ( ( 𝑥 ·R ( 𝑧 ·R 𝑣 ) ) +R ( -1R ·R ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) ) ) ) +R ( ( -1R ·R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) +R ( 𝑥 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) )
40 distrsr ⊢ ( 𝑥 ·R ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) = ( ( 𝑥 ·R ( 𝑧 ·R 𝑣 ) ) +R ( 𝑥 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) )
41 distrsr ⊢ ( 𝑦 ·R ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ) = ( ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) ) +R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) )
42 41 oveq2i ⊢ ( -1R ·R ( 𝑦 ·R ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ) ) = ( -1R ·R ( ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) ) +R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) )
43 distrsr ⊢ ( -1R ·R ( ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) ) +R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) ) = ( ( -1R ·R ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) ) ) +R ( -1R ·R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) )
44 42 43 eqtri ⊢ ( -1R ·R ( 𝑦 ·R ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ) ) = ( ( -1R ·R ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) ) ) +R ( -1R ·R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) )
45 40 44 oveq12i ⊢ ( ( 𝑥 ·R ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) +R ( -1R ·R ( 𝑦 ·R ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ) ) ) = ( ( ( 𝑥 ·R ( 𝑧 ·R 𝑣 ) ) +R ( 𝑥 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) +R ( ( -1R ·R ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) ) ) +R ( -1R ·R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) ) )
46 vex ⊢ 𝑥 ∈ V
47 7 elexi ⊢ -1R ∈ V
48 vex ⊢ 𝑧 ∈ V
49 mulcomsr ⊢ ( 𝑓 ·R 𝑔 ) = ( 𝑔 ·R 𝑓 )
50 distrsr ⊢ ( 𝑓 ·R ( 𝑔 +R ℎ ) ) = ( ( 𝑓 ·R 𝑔 ) +R ( 𝑓 ·R ℎ ) )
51 ovex ⊢ ( 𝑦 ·R 𝑤 ) ∈ V
52 vex ⊢ 𝑣 ∈ V
53 mulasssr ⊢ ( ( 𝑓 ·R 𝑔 ) ·R ℎ ) = ( 𝑓 ·R ( 𝑔 ·R ℎ ) )
54 46 47 48 49 50 51 52 53 caovdilem ⊢ ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ·R 𝑣 ) = ( ( 𝑥 ·R ( 𝑧 ·R 𝑣 ) ) +R ( -1R ·R ( ( 𝑦 ·R 𝑤 ) ·R 𝑣 ) ) )
55 mulasssr ⊢ ( ( 𝑦 ·R 𝑤 ) ·R 𝑣 ) = ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) )
56 55 oveq2i ⊢ ( -1R ·R ( ( 𝑦 ·R 𝑤 ) ·R 𝑣 ) ) = ( -1R ·R ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) ) )
57 56 oveq2i ⊢ ( ( 𝑥 ·R ( 𝑧 ·R 𝑣 ) ) +R ( -1R ·R ( ( 𝑦 ·R 𝑤 ) ·R 𝑣 ) ) ) = ( ( 𝑥 ·R ( 𝑧 ·R 𝑣 ) ) +R ( -1R ·R ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) ) ) )
58 54 57 eqtri ⊢ ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ·R 𝑣 ) = ( ( 𝑥 ·R ( 𝑧 ·R 𝑣 ) ) +R ( -1R ·R ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) ) ) )
59 vex ⊢ 𝑦 ∈ V
60 vex ⊢ 𝑤 ∈ V
61 vex ⊢ 𝑢 ∈ V
62 59 46 48 49 50 60 61 53 caovdilem ⊢ ( ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ·R 𝑢 ) = ( ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) +R ( 𝑥 ·R ( 𝑤 ·R 𝑢 ) ) )
63 62 oveq2i ⊢ ( -1R ·R ( ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ·R 𝑢 ) ) = ( -1R ·R ( ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) +R ( 𝑥 ·R ( 𝑤 ·R 𝑢 ) ) ) )
64 distrsr ⊢ ( -1R ·R ( ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) +R ( 𝑥 ·R ( 𝑤 ·R 𝑢 ) ) ) ) = ( ( -1R ·R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) +R ( -1R ·R ( 𝑥 ·R ( 𝑤 ·R 𝑢 ) ) ) )
65 ovex ⊢ ( 𝑤 ·R 𝑢 ) ∈ V
66 47 46 65 49 53 caov12 ⊢ ( -1R ·R ( 𝑥 ·R ( 𝑤 ·R 𝑢 ) ) ) = ( 𝑥 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) )
67 66 oveq2i ⊢ ( ( -1R ·R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) +R ( -1R ·R ( 𝑥 ·R ( 𝑤 ·R 𝑢 ) ) ) ) = ( ( -1R ·R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) +R ( 𝑥 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) )
68 64 67 eqtri ⊢ ( -1R ·R ( ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) +R ( 𝑥 ·R ( 𝑤 ·R 𝑢 ) ) ) ) = ( ( -1R ·R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) +R ( 𝑥 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) )
69 63 68 eqtri ⊢ ( -1R ·R ( ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ·R 𝑢 ) ) = ( ( -1R ·R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) +R ( 𝑥 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) )
70 58 69 oveq12i ⊢ ( ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ·R 𝑣 ) +R ( -1R ·R ( ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ·R 𝑢 ) ) ) = ( ( ( 𝑥 ·R ( 𝑧 ·R 𝑣 ) ) +R ( -1R ·R ( 𝑦 ·R ( 𝑤 ·R 𝑣 ) ) ) ) +R ( ( -1R ·R ( 𝑦 ·R ( 𝑧 ·R 𝑢 ) ) ) +R ( 𝑥 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) )
71 39 45 70 3eqtr4ri ⊢ ( ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ·R 𝑣 ) +R ( -1R ·R ( ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ·R 𝑢 ) ) ) = ( ( 𝑥 ·R ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) +R ( -1R ·R ( 𝑦 ·R ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ) ) )
72 ovex ⊢ ( 𝑦 ·R ( 𝑧 ·R 𝑣 ) ) ∈ V
73 ovex ⊢ ( 𝑦 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ∈ V
74 ovex ⊢ ( 𝑥 ·R ( 𝑤 ·R 𝑣 ) ) ∈ V
75 ovex ⊢ ( 𝑥 ·R ( 𝑧 ·R 𝑢 ) ) ∈ V
76 72 73 74 36 37 75 caov42 ⊢ ( ( ( 𝑦 ·R ( 𝑧 ·R 𝑣 ) ) +R ( 𝑦 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) +R ( ( 𝑥 ·R ( 𝑤 ·R 𝑣 ) ) +R ( 𝑥 ·R ( 𝑧 ·R 𝑢 ) ) ) ) = ( ( ( 𝑦 ·R ( 𝑧 ·R 𝑣 ) ) +R ( 𝑥 ·R ( 𝑤 ·R 𝑣 ) ) ) +R ( ( 𝑥 ·R ( 𝑧 ·R 𝑢 ) ) +R ( 𝑦 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) )
77 distrsr ⊢ ( 𝑦 ·R ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) = ( ( 𝑦 ·R ( 𝑧 ·R 𝑣 ) ) +R ( 𝑦 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) )
78 distrsr ⊢ ( 𝑥 ·R ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ) = ( ( 𝑥 ·R ( 𝑤 ·R 𝑣 ) ) +R ( 𝑥 ·R ( 𝑧 ·R 𝑢 ) ) )
79 77 78 oveq12i ⊢ ( ( 𝑦 ·R ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) +R ( 𝑥 ·R ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ) ) = ( ( ( 𝑦 ·R ( 𝑧 ·R 𝑣 ) ) +R ( 𝑦 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) +R ( ( 𝑥 ·R ( 𝑤 ·R 𝑣 ) ) +R ( 𝑥 ·R ( 𝑧 ·R 𝑢 ) ) ) )
80 59 46 48 49 50 60 52 53 caovdilem ⊢ ( ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ·R 𝑣 ) = ( ( 𝑦 ·R ( 𝑧 ·R 𝑣 ) ) +R ( 𝑥 ·R ( 𝑤 ·R 𝑣 ) ) )
81 46 47 48 49 50 51 61 53 caovdilem ⊢ ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ·R 𝑢 ) = ( ( 𝑥 ·R ( 𝑧 ·R 𝑢 ) ) +R ( -1R ·R ( ( 𝑦 ·R 𝑤 ) ·R 𝑢 ) ) )
82 mulasssr ⊢ ( ( 𝑦 ·R 𝑤 ) ·R 𝑢 ) = ( 𝑦 ·R ( 𝑤 ·R 𝑢 ) )
83 82 oveq2i ⊢ ( -1R ·R ( ( 𝑦 ·R 𝑤 ) ·R 𝑢 ) ) = ( -1R ·R ( 𝑦 ·R ( 𝑤 ·R 𝑢 ) ) )
84 47 59 65 49 53 caov12 ⊢ ( -1R ·R ( 𝑦 ·R ( 𝑤 ·R 𝑢 ) ) ) = ( 𝑦 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) )
85 83 84 eqtri ⊢ ( -1R ·R ( ( 𝑦 ·R 𝑤 ) ·R 𝑢 ) ) = ( 𝑦 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) )
86 85 oveq2i ⊢ ( ( 𝑥 ·R ( 𝑧 ·R 𝑢 ) ) +R ( -1R ·R ( ( 𝑦 ·R 𝑤 ) ·R 𝑢 ) ) ) = ( ( 𝑥 ·R ( 𝑧 ·R 𝑢 ) ) +R ( 𝑦 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) )
87 81 86 eqtri ⊢ ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ·R 𝑢 ) = ( ( 𝑥 ·R ( 𝑧 ·R 𝑢 ) ) +R ( 𝑦 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) )
88 80 87 oveq12i ⊢ ( ( ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ·R 𝑣 ) +R ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ·R 𝑢 ) ) = ( ( ( 𝑦 ·R ( 𝑧 ·R 𝑣 ) ) +R ( 𝑥 ·R ( 𝑤 ·R 𝑣 ) ) ) +R ( ( 𝑥 ·R ( 𝑧 ·R 𝑢 ) ) +R ( 𝑦 ·R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) )
89 76 79 88 3eqtr4ri ⊢ ( ( ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ·R 𝑣 ) +R ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ·R 𝑢 ) ) = ( ( 𝑦 ·R ( ( 𝑧 ·R 𝑣 ) +R ( -1R ·R ( 𝑤 ·R 𝑢 ) ) ) ) +R ( 𝑥 ·R ( ( 𝑤 ·R 𝑣 ) +R ( 𝑧 ·R 𝑢 ) ) ) )
90 1 2 3 4 5 19 32 71 89 ecovass ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) · 𝐶 ) = ( 𝐴 · ( 𝐵 · 𝐶 ) ) )