Theorem axmulass 10301

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 10325. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)

Assertion

Ref	Expression
axmulass	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Proof of Theorem axmulass

Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 𝑓 𝑔 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcnqs 10286	. 2 ⊢ ℂ = ((R × R) / ◡ E )
2		mulcnsrec 10288	. 2 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → ([⟨𝑥, 𝑦⟩]◡ E · [⟨𝑧, 𝑤⟩]◡ E ) = [⟨((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))), ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤))⟩]◡ E )
3		mulcnsrec 10288	. 2 ⊢ (((𝑧 ∈ R ∧ 𝑤 ∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) → ([⟨𝑧, 𝑤⟩]◡ E · [⟨𝑣, 𝑢⟩]◡ E ) = [⟨((𝑧 ·R 𝑣) +R (-1R ·R (𝑤 ·R 𝑢))), ((𝑤 ·R 𝑣) +R (𝑧 ·R 𝑢))⟩]◡ E )
4		mulcnsrec 10288	. 2 ⊢ (((((𝑥 ·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 10288	. 2 ⊢ (((𝑥 ∈ 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 10228	. . . . 5 ⊢ ((𝑥 ∈ R ∧ 𝑧 ∈ R) → (𝑥 ·R 𝑧) ∈ R)
7		m1r 10226	. . . . . 6 ⊢ -1R ∈ R
8		mulclsr 10228	. . . . . 6 ⊢ ((𝑦 ∈ R ∧ 𝑤 ∈ R) → (𝑦 ·R 𝑤) ∈ R)
9		mulclsr 10228	. . . . . 6 ⊢ ((-1R ∈ R ∧ (𝑦 ·R 𝑤) ∈ R) → (-1R ·R (𝑦 ·R 𝑤)) ∈ R)
10	7, 8, 9	sylancr 581	. . . . 5 ⊢ ((𝑦 ∈ R ∧ 𝑤 ∈ R) → (-1R ·R (𝑦 ·R 𝑤)) ∈ R)
11		addclsr 10227	. . . . 5 ⊢ (((𝑥 ·R 𝑧) ∈ R ∧ (-1R ·R (𝑦 ·R 𝑤)) ∈ R) → ((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R)
12	6, 10, 11	syl2an 589	. . . 4 ⊢ (((𝑥 ∈ R ∧ 𝑧 ∈ R) ∧ (𝑦 ∈ R ∧ 𝑤 ∈ R)) → ((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R)
13	12	an4s 650	. . 3 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → ((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R)
14		mulclsr 10228	. . . . 5 ⊢ ((𝑦 ∈ R ∧ 𝑧 ∈ R) → (𝑦 ·R 𝑧) ∈ R)
15		mulclsr 10228	. . . . 5 ⊢ ((𝑥 ∈ R ∧ 𝑤 ∈ R) → (𝑥 ·R 𝑤) ∈ R)
16		addclsr 10227	. . . . 5 ⊢ (((𝑦 ·R 𝑧) ∈ R ∧ (𝑥 ·R 𝑤) ∈ R) → ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R)
17	14, 15, 16	syl2anr 590	. . . 4 ⊢ (((𝑥 ∈ R ∧ 𝑤 ∈ R) ∧ (𝑦 ∈ R ∧ 𝑧 ∈ R)) → ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R)
18	17	an42s 651	. . 3 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R)
19	13, 18	jca 507	. 2 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → (((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R ∧ ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R))
20		mulclsr 10228	. . . . 5 ⊢ ((𝑧 ∈ R ∧ 𝑣 ∈ R) → (𝑧 ·R 𝑣) ∈ R)
21		mulclsr 10228	. . . . . 6 ⊢ ((𝑤 ∈ R ∧ 𝑢 ∈ R) → (𝑤 ·R 𝑢) ∈ R)
22		mulclsr 10228	. . . . . 6 ⊢ ((-1R ∈ R ∧ (𝑤 ·R 𝑢) ∈ R) → (-1R ·R (𝑤 ·R 𝑢)) ∈ R)
23	7, 21, 22	sylancr 581	. . . . 5 ⊢ ((𝑤 ∈ R ∧ 𝑢 ∈ R) → (-1R ·R (𝑤 ·R 𝑢)) ∈ R)
24		addclsr 10227	. . . . 5 ⊢ (((𝑧 ·R 𝑣) ∈ R ∧ (-1R ·R (𝑤 ·R 𝑢)) ∈ R) → ((𝑧 ·R 𝑣) +R (-1R ·R (𝑤 ·R 𝑢))) ∈ R)
25	20, 23, 24	syl2an 589	. . . 4 ⊢ (((𝑧 ∈ R ∧ 𝑣 ∈ R) ∧ (𝑤 ∈ R ∧ 𝑢 ∈ R)) → ((𝑧 ·R 𝑣) +R (-1R ·R (𝑤 ·R 𝑢))) ∈ R)
26	25	an4s 650	. . 3 ⊢ (((𝑧 ∈ R ∧ 𝑤 ∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) → ((𝑧 ·R 𝑣) +R (-1R ·R (𝑤 ·R 𝑢))) ∈ R)
27		mulclsr 10228	. . . . 5 ⊢ ((𝑤 ∈ R ∧ 𝑣 ∈ R) → (𝑤 ·R 𝑣) ∈ R)
28		mulclsr 10228	. . . . 5 ⊢ ((𝑧 ∈ R ∧ 𝑢 ∈ R) → (𝑧 ·R 𝑢) ∈ R)
29		addclsr 10227	. . . . 5 ⊢ (((𝑤 ·R 𝑣) ∈ R ∧ (𝑧 ·R 𝑢) ∈ R) → ((𝑤 ·R 𝑣) +R (𝑧 ·R 𝑢)) ∈ R)
30	27, 28, 29	syl2anr 590	. . . 4 ⊢ (((𝑧 ∈ R ∧ 𝑢 ∈ R) ∧ (𝑤 ∈ R ∧ 𝑣 ∈ R)) → ((𝑤 ·R 𝑣) +R (𝑧 ·R 𝑢)) ∈ R)
31	30	an42s 651	. . 3 ⊢ (((𝑧 ∈ R ∧ 𝑤 ∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) → ((𝑤 ·R 𝑣) +R (𝑧 ·R 𝑢)) ∈ R)
32	26, 31	jca 507	. 2 ⊢ (((𝑧 ∈ R ∧ 𝑤 ∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) → (((𝑧 ·R 𝑣) +R (-1R ·R (𝑤 ·R 𝑢))) ∈ R ∧ ((𝑤 ·R 𝑣) +R (𝑧 ·R 𝑢)) ∈ R))
33		ovex 6942	. . . 4 ⊢ (𝑥 ·R (𝑧 ·R 𝑣)) ∈ V
34		ovex 6942	. . . 4 ⊢ (𝑥 ·R (-1R ·R (𝑤 ·R 𝑢))) ∈ V
35		ovex 6942	. . . 4 ⊢ (-1R ·R (𝑦 ·R (𝑤 ·R 𝑣))) ∈ V
36		addcomsr 10231	. . . 4 ⊢ (𝑓 +R 𝑔) = (𝑔 +R 𝑓)
37		addasssr 10232	. . . 4 ⊢ ((𝑓 +R 𝑔) +R ℎ) = (𝑓 +R (𝑔 +R ℎ))
38		ovex 6942	. . . 4 ⊢ (-1R ·R (𝑦 ·R (𝑧 ·R 𝑢))) ∈ V
39	33, 34, 35, 36, 37, 38	caov42 7132	. . 3 ⊢ (((𝑥 ·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 10235	. . . 4 ⊢ (𝑥 ·R ((𝑧 ·R 𝑣) +R (-1R ·R (𝑤 ·R 𝑢)))) = ((𝑥 ·R (𝑧 ·R 𝑣)) +R (𝑥 ·R (-1R ·R (𝑤 ·R 𝑢))))
41		distrsr 10235	. . . . . 6 ⊢ (𝑦 ·R ((𝑤 ·R 𝑣) +R (𝑧 ·R 𝑢))) = ((𝑦 ·R (𝑤 ·R 𝑣)) +R (𝑦 ·R (𝑧 ·R 𝑢)))
42	41	oveq2i 6921	. . . . 5 ⊢ (-1R ·R (𝑦 ·R ((𝑤 ·R 𝑣) +R (𝑧 ·R 𝑢)))) = (-1R ·R ((𝑦 ·R (𝑤 ·R 𝑣)) +R (𝑦 ·R (𝑧 ·R 𝑢))))
43		distrsr 10235	. . . . 5 ⊢ (-1R ·R ((𝑦 ·R (𝑤 ·R 𝑣)) +R (𝑦 ·R (𝑧 ·R 𝑢)))) = ((-1R ·R (𝑦 ·R (𝑤 ·R 𝑣))) +R (-1R ·R (𝑦 ·R (𝑧 ·R 𝑢))))
44	42, 43	eqtri 2849	. . . 4 ⊢ (-1R ·R (𝑦 ·R ((𝑤 ·R 𝑣) +R (𝑧 ·R 𝑢)))) = ((-1R ·R (𝑦 ·R (𝑤 ·R 𝑣))) +R (-1R ·R (𝑦 ·R (𝑧 ·R 𝑢))))
45	40, 44	oveq12i 6922	. . 3 ⊢ ((𝑥 ·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 3417	. . . . . 6 ⊢ 𝑥 ∈ V
47	7	elexi 3430	. . . . . 6 ⊢ -1R ∈ V
48		vex 3417	. . . . . 6 ⊢ 𝑧 ∈ V
49		mulcomsr 10233	. . . . . 6 ⊢ (𝑓 ·R 𝑔) = (𝑔 ·R 𝑓)
50		distrsr 10235	. . . . . 6 ⊢ (𝑓 ·R (𝑔 +R ℎ)) = ((𝑓 ·R 𝑔) +R (𝑓 ·R ℎ))
51		ovex 6942	. . . . . 6 ⊢ (𝑦 ·R 𝑤) ∈ V
52		vex 3417	. . . . . 6 ⊢ 𝑣 ∈ V
53		mulasssr 10234	. . . . . 6 ⊢ ((𝑓 ·R 𝑔) ·R ℎ) = (𝑓 ·R (𝑔 ·R ℎ))
54	46, 47, 48, 49, 50, 51, 52, 53	caovdilem 7134	. . . . 5 ⊢ (((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ·R 𝑣) = ((𝑥 ·R (𝑧 ·R 𝑣)) +R (-1R ·R ((𝑦 ·R 𝑤) ·R 𝑣)))
55		mulasssr 10234	. . . . . . 7 ⊢ ((𝑦 ·R 𝑤) ·R 𝑣) = (𝑦 ·R (𝑤 ·R 𝑣))
56	55	oveq2i 6921	. . . . . 6 ⊢ (-1R ·R ((𝑦 ·R 𝑤) ·R 𝑣)) = (-1R ·R (𝑦 ·R (𝑤 ·R 𝑣)))
57	56	oveq2i 6921	. . . . 5 ⊢ ((𝑥 ·R (𝑧 ·R 𝑣)) +R (-1R ·R ((𝑦 ·R 𝑤) ·R 𝑣))) = ((𝑥 ·R (𝑧 ·R 𝑣)) +R (-1R ·R (𝑦 ·R (𝑤 ·R 𝑣))))
58	54, 57	eqtri 2849	. . . 4 ⊢ (((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ·R 𝑣) = ((𝑥 ·R (𝑧 ·R 𝑣)) +R (-1R ·R (𝑦 ·R (𝑤 ·R 𝑣))))
59		vex 3417	. . . . . . 7 ⊢ 𝑦 ∈ V
60		vex 3417	. . . . . . 7 ⊢ 𝑤 ∈ V
61		vex 3417	. . . . . . 7 ⊢ 𝑢 ∈ V
62	59, 46, 48, 49, 50, 60, 61, 53	caovdilem 7134	. . . . . 6 ⊢ (((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ·R 𝑢) = ((𝑦 ·R (𝑧 ·R 𝑢)) +R (𝑥 ·R (𝑤 ·R 𝑢)))
63	62	oveq2i 6921	. . . . 5 ⊢ (-1R ·R (((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ·R 𝑢)) = (-1R ·R ((𝑦 ·R (𝑧 ·R 𝑢)) +R (𝑥 ·R (𝑤 ·R 𝑢))))
64		distrsr 10235	. . . . . 6 ⊢ (-1R ·R ((𝑦 ·R (𝑧 ·R 𝑢)) +R (𝑥 ·R (𝑤 ·R 𝑢)))) = ((-1R ·R (𝑦 ·R (𝑧 ·R 𝑢))) +R (-1R ·R (𝑥 ·R (𝑤 ·R 𝑢))))
65		ovex 6942	. . . . . . . 8 ⊢ (𝑤 ·R 𝑢) ∈ V
66	47, 46, 65, 49, 53	caov12 7127	. . . . . . 7 ⊢ (-1R ·R (𝑥 ·R (𝑤 ·R 𝑢))) = (𝑥 ·R (-1R ·R (𝑤 ·R 𝑢)))
67	66	oveq2i 6921	. . . . . 6 ⊢ ((-1R ·R (𝑦 ·R (𝑧 ·R 𝑢))) +R (-1R ·R (𝑥 ·R (𝑤 ·R 𝑢)))) = ((-1R ·R (𝑦 ·R (𝑧 ·R 𝑢))) +R (𝑥 ·R (-1R ·R (𝑤 ·R 𝑢))))
68	64, 67	eqtri 2849	. . . . 5 ⊢ (-1R ·R ((𝑦 ·R (𝑧 ·R 𝑢)) +R (𝑥 ·R (𝑤 ·R 𝑢)))) = ((-1R ·R (𝑦 ·R (𝑧 ·R 𝑢))) +R (𝑥 ·R (-1R ·R (𝑤 ·R 𝑢))))
69	63, 68	eqtri 2849	. . . 4 ⊢ (-1R ·R (((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ·R 𝑢)) = ((-1R ·R (𝑦 ·R (𝑧 ·R 𝑢))) +R (𝑥 ·R (-1R ·R (𝑤 ·R 𝑢))))
70	58, 69	oveq12i 6922	. . 3 ⊢ ((((𝑥 ·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 2860	. 2 ⊢ ((((𝑥 ·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 6942	. . . 4 ⊢ (𝑦 ·R (𝑧 ·R 𝑣)) ∈ V
73		ovex 6942	. . . 4 ⊢ (𝑦 ·R (-1R ·R (𝑤 ·R 𝑢))) ∈ V
74		ovex 6942	. . . 4 ⊢ (𝑥 ·R (𝑤 ·R 𝑣)) ∈ V
75		ovex 6942	. . . 4 ⊢ (𝑥 ·R (𝑧 ·R 𝑢)) ∈ V
76	72, 73, 74, 36, 37, 75	caov42 7132	. . 3 ⊢ (((𝑦 ·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 10235	. . . 4 ⊢ (𝑦 ·R ((𝑧 ·R 𝑣) +R (-1R ·R (𝑤 ·R 𝑢)))) = ((𝑦 ·R (𝑧 ·R 𝑣)) +R (𝑦 ·R (-1R ·R (𝑤 ·R 𝑢))))
78		distrsr 10235	. . . 4 ⊢ (𝑥 ·R ((𝑤 ·R 𝑣) +R (𝑧 ·R 𝑢))) = ((𝑥 ·R (𝑤 ·R 𝑣)) +R (𝑥 ·R (𝑧 ·R 𝑢)))
79	77, 78	oveq12i 6922	. . 3 ⊢ ((𝑦 ·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 7134	. . . 4 ⊢ (((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ·R 𝑣) = ((𝑦 ·R (𝑧 ·R 𝑣)) +R (𝑥 ·R (𝑤 ·R 𝑣)))
81	46, 47, 48, 49, 50, 51, 61, 53	caovdilem 7134	. . . . 5 ⊢ (((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ·R 𝑢) = ((𝑥 ·R (𝑧 ·R 𝑢)) +R (-1R ·R ((𝑦 ·R 𝑤) ·R 𝑢)))
82		mulasssr 10234	. . . . . . . 8 ⊢ ((𝑦 ·R 𝑤) ·R 𝑢) = (𝑦 ·R (𝑤 ·R 𝑢))
83	82	oveq2i 6921	. . . . . . 7 ⊢ (-1R ·R ((𝑦 ·R 𝑤) ·R 𝑢)) = (-1R ·R (𝑦 ·R (𝑤 ·R 𝑢)))
84	47, 59, 65, 49, 53	caov12 7127	. . . . . . 7 ⊢ (-1R ·R (𝑦 ·R (𝑤 ·R 𝑢))) = (𝑦 ·R (-1R ·R (𝑤 ·R 𝑢)))
85	83, 84	eqtri 2849	. . . . . 6 ⊢ (-1R ·R ((𝑦 ·R 𝑤) ·R 𝑢)) = (𝑦 ·R (-1R ·R (𝑤 ·R 𝑢)))
86	85	oveq2i 6921	. . . . 5 ⊢ ((𝑥 ·R (𝑧 ·R 𝑢)) +R (-1R ·R ((𝑦 ·R 𝑤) ·R 𝑢))) = ((𝑥 ·R (𝑧 ·R 𝑢)) +R (𝑦 ·R (-1R ·R (𝑤 ·R 𝑢))))
87	81, 86	eqtri 2849	. . . 4 ⊢ (((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ·R 𝑢) = ((𝑥 ·R (𝑧 ·R 𝑢)) +R (𝑦 ·R (-1R ·R (𝑤 ·R 𝑢))))
88	80, 87	oveq12i 6922	. . 3 ⊢ ((((𝑦 ·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 2860	. 2 ⊢ ((((𝑦 ·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 8125	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1111   = wceq 1656   ∈ wcel 2164   E cep 5256  ^◡ccnv 5345  (class class class)co 6910  Rcnr 10009  -1_Rcm1r 10012   +_R cplr 10013   ·_R cmr 10014  ℂcc 10257   · cmul 10264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214  ax-inf2 8822

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-int 4700  df-iun 4744  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-om 7332  df-1st 7433  df-2nd 7434  df-wrecs 7677  df-recs 7739  df-rdg 7777  df-1o 7831  df-oadd 7835  df-omul 7836  df-er 8014  df-ec 8016  df-qs 8020  df-ni 10016  df-pli 10017  df-mi 10018  df-lti 10019  df-plpq 10052  df-mpq 10053  df-ltpq 10054  df-enq 10055  df-nq 10056  df-erq 10057  df-plq 10058  df-mq 10059  df-1nq 10060  df-rq 10061  df-ltnq 10062  df-np 10125  df-1p 10126  df-plp 10127  df-mp 10128  df-ltp 10129  df-enr 10199  df-nr 10200  df-plr 10201  df-mr 10202  df-m1r 10206  df-c 10265  df-mul 10271

This theorem is referenced by: (None)