Theorem axdistr 4074

Description: Distributive law for complex numbers. One of the 28 axioms for real and complex numbers, derived from ZF set theory.

Assertion

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

Proof of Theorem axdistr

Step	Hyp	Ref	Expression
1		dfcnqs 4056	. 2 |- CC = ((R. X. R.)/.`'E)
2		addcnsrec 4057	. 2 |- (((z e. R. /\ w e. R.) /\ (v e. R. /\ u e. R.)) -> ([<.z, w>.]`'E + [<.v, u>.]`'E) = [<.(z +R v), (w +R u)>.]`'E)
3		mulcnsrec 4058	. 2 |- (((x e. R. /\ y e. R.) /\ ((z +R v) e. R. /\ (w +R u) e. R.)) -> ([<.x, y>.]`'E x. [<.(z +R v), (w +R u)>.]`'E) = [<.((x .R (z +R v)) +R (-1R .R (y .R (w +R u)))), ((y .R (z +R v)) +R (x .R (w +R u)))>.]`'E)
4		mulcnsrec 4058	. 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)
5		mulcnsrec 4058	. 2 |- (((x e. R. /\ y e. R.) /\ (v e. R. /\ u e. R.)) -> ([<.x, y>.]`'E x. [<.v, u>.]`'E) = [<.((x .R v) +R (-1R .R (y .R u))), ((y .R v) +R (x .R u))>.]`'E)
6		addcnsrec 4057	. 2 |- (((((x .R z) +R (-1R .R (y .R w))) e. R. /\ ((y .R z) +R (x .R w)) e. R.) /\ (((x .R v) +R (-1R .R (y .R u))) e. R. /\ ((y .R v) +R (x .R u)) e. R.)) -> ([<.((x .R z) +R (-1R .R (y .R w))), ((y .R z) +R (x .R w))>.]`'E + [<.((x .R v) +R (-1R .R (y .R u))), ((y .R v) +R (x .R u))>.]`'E) = [<.(((x .R z) +R (-1R .R (y .R w))) +R ((x .R v) +R (-1R .R (y .R u)))), (((y .R z) +R (x .R w)) +R ((y .R v) +R (x .R u)))>.]`'E)
7		addclsr 3986	. . . 4 |- ((z e. R. /\ v e. R.) -> (z +R v) e. R.)
8		addclsr 3986	. . . 4 |- ((w e. R. /\ u e. R.) -> (w +R u) e. R.)
9	7, 8	anim12i 268	. . 3 |- (((z e. R. /\ v e. R.) /\ (w e. R. /\ u e. R.)) -> ((z +R v) e. R. /\ (w +R u) e. R.))
10	9	an4s 390	. 2 |- (((z e. R. /\ w e. R.) /\ (v e. R. /\ u e. R.)) -> ((z +R v) e. R. /\ (w +R u) e. R.))
11		addclsr 3986	. . . . 5 |- (((x .R z) e. R. /\ (-1R .R (y .R w)) e. R.) -> ((x .R z) +R (-1R .R (y .R w))) e. R.)
12		mulclsr 3987	. . . . 5 |- ((x e. R. /\ z e. R.) -> (x .R z) e. R.)
13		mulclsr 3987	. . . . . 6 |- ((y e. R. /\ w e. R.) -> (y .R w) e. R.)
14		m1r 3985	. . . . . . 7 |- -1R e. R.
15		mulclsr 3987	. . . . . . 7 |- ((-1R e. R. /\ (y .R w) e. R.) -> (-1R .R (y .R w)) e. R.)
16	14, 15	mpan 518	. . . . . 6 |- ((y .R w) e. R. -> (-1R .R (y .R w)) e. R.)
17	13, 16	syl 12	. . . . 5 |- ((y e. R. /\ w e. R.) -> (-1R .R (y .R w)) e. R.)
18	11, 12, 17	syl2an 349	. . . 4 |- (((x e. R. /\ z e. R.) /\ (y e. R. /\ w e. R.)) -> ((x .R z) +R (-1R .R (y .R w))) e. R.)
19	18	an4s 390	. . 3 |- (((x e. R. /\ y e. R.) /\ (z e. R. /\ w e. R.)) -> ((x .R z) +R (-1R .R (y .R w))) e. R.)
20		addclsr 3986	. . . . . 6 |- (((y .R z) e. R. /\ (x .R w) e. R.) -> ((y .R z) +R (x .R w)) e. R.)
21		mulclsr 3987	. . . . . 6 |- ((y e. R. /\ z e. R.) -> (y .R z) e. R.)
22		mulclsr 3987	. . . . . 6 |- ((x e. R. /\ w e. R.) -> (x .R w) e. R.)
23	20, 21, 22	syl2an 349	. . . . 5 |- (((y e. R. /\ z e. R.) /\ (x e. R. /\ w e. R.)) -> ((y .R z) +R (x .R w)) e. R.)
24	23	ancoms 334	. . . 4 |- (((x e. R. /\ w e. R.) /\ (y e. R. /\ z e. R.)) -> ((y .R z) +R (x .R w)) e. R.)
25	24	an42s 391	. . 3 |- (((x e. R. /\ y e. R.) /\ (z e. R. /\ w e. R.)) -> ((y .R z) +R (x .R w)) e. R.)
26	19, 25	jca 236	. 2 |- (((x e. R. /\ y e. R.) /\ (z e. R. /\ w e. R.)) -> (((x .R z) +R (-1R .R (y .R w))) e. R. /\ ((y .R z) +R (x .R w)) e. R.))
27		addclsr 3986	. . . . 5 |- (((x .R v) e. R. /\ (-1R .R (y .R u)) e. R.) -> ((x .R v) +R (-1R .R (y .R u))) e. R.)
28		mulclsr 3987	. . . . 5 |- ((x e. R. /\ v e. R.) -> (x .R v) e. R.)
29		mulclsr 3987	. . . . . 6 |- ((y e. R. /\ u e. R.) -> (y .R u) e. R.)
30		mulclsr 3987	. . . . . . 7 |- ((-1R e. R. /\ (y .R u) e. R.) -> (-1R .R (y .R u)) e. R.)
31	14, 30	mpan 518	. . . . . 6 |- ((y .R u) e. R. -> (-1R .R (y .R u)) e. R.)
32	29, 31	syl 12	. . . . 5 |- ((y e. R. /\ u e. R.) -> (-1R .R (y .R u)) e. R.)
33	27, 28, 32	syl2an 349	. . . 4 |- (((x e. R. /\ v e. R.) /\ (y e. R. /\ u e. R.)) -> ((x .R v) +R (-1R .R (y .R u))) e. R.)
34	33	an4s 390	. . 3 |- (((x e. R. /\ y e. R.) /\ (v e. R. /\ u e. R.)) -> ((x .R v) +R (-1R .R (y .R u))) e. R.)
35		addclsr 3986	. . . . . 6 |- (((y .R v) e. R. /\ (x .R u) e. R.) -> ((y .R v) +R (x .R u)) e. R.)
36		mulclsr 3987	. . . . . 6 |- ((y e. R. /\ v e. R.) -> (y .R v) e. R.)
37		mulclsr 3987	. . . . . 6 |- ((x e. R. /\ u e. R.) -> (x .R u) e. R.)
38	35, 36, 37	syl2an 349	. . . . 5 |- (((y e. R. /\ v e. R.) /\ (x e. R. /\ u e. R.)) -> ((y .R v) +R (x .R u)) e. R.)
39	38	ancoms 334	. . . 4 |- (((x e. R. /\ u e. R.) /\ (y e. R. /\ v e. R.)) -> ((y .R v) +R (x .R u)) e. R.)
40	39	an42s 391	. . 3 |- (((x e. R. /\ y e. R.) /\ (v e. R. /\ u e. R.)) -> ((y .R v) +R (x .R u)) e. R.)
41	34, 40	jca 236	. 2 |- (((x e. R. /\ y e. R.) /\ (v e. R. /\ u e. R.)) -> (((x .R v) +R (-1R .R (y .R u))) e. R. /\ ((y .R v) +R (x .R u)) e. R.))
42		visset 1350	. . . . 5 |- z e. V
43		visset 1350	. . . . 5 |- v e. V
44	42, 43	distrsr 3994	. . . 4 |- (x .R (z +R v)) = ((x .R z) +R (x .R v))
45		visset 1350	. . . . . . 7 |- w e. V
46		visset 1350	. . . . . . 7 |- u e. V
47	45, 46	distrsr 3994	. . . . . 6 |- (y .R (w +R u)) = ((y .R w) +R (y .R u))
48	47	opreq2i 3010	. . . . 5 |- (-1R .R (y .R (w +R u))) = (-1R .R ((y .R w) +R (y .R u)))
49		oprex 3018	. . . . . 6 |- (y .R w) e. V
50		oprex 3018	. . . . . 6 |- (y .R u) e. V
51	49, 50	distrsr 3994	. . . . 5 |- (-1R .R ((y .R w) +R (y .R u))) = ((-1R .R (y .R w)) +R (-1R .R (y .R u)))
52	48, 51	eqtr 1119	. . . 4 |- (-1R .R (y .R (w +R u))) = ((-1R .R (y .R w)) +R (-1R .R (y .R u)))
53	44, 52	opreq12i 3011	. . 3 |- ((x .R (z +R v)) +R (-1R .R (y .R (w +R u)))) = (((x .R z) +R (x .R v)) +R ((-1R .R (y .R w)) +R (-1R .R (y .R u))))
54		oprex 3018	. . . 4 |- (x .R z) e. V
55		oprex 3018	. . . 4 |- (x .R v) e. V
56		oprex 3018	. . . 4 |- (-1R .R (y .R w)) e. V
57		visset 1350	. . . . 5 |- f e. V
58		visset 1350	. . . . 5 |- g e. V
59	57, 58	addcomsr 3990	. . . 4 |- (f +R g) = (g +R f)
60		visset 1350	. . . . 5 |- h e. V
61	58, 60	addasssr 3991	. . . 4 |- ((f +R g) +R h) = (