Theorem axdistr 5266

Description: Distributive law for complex numbers. Axiom 13 of 25 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 5249	. 2 |- CC = ((R. X. R.)/.`'E)
2		addcnsrec 5250	. 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 5251	. 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 5251	. 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 5251	. 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 5250	. 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 5179	. . . 4 |- ((z e. R. /\ v e. R.) -> (z +R v) e. R.)
8		addclsr 5179	. . . 4 |- ((w e. R. /\ u e. R.) -> (w +R u) e. R.)
9	7, 8	anim12i 333	. . 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 508	. 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 5179	. . . . 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 5180	. . . . 5 |- ((x e. R. /\ z e. R.) -> (x .R z) e. R.)
13		mulclsr 5180	. . . . . 6 |- ((y e. R. /\ w e. R.) -> (y .R w) e. R.)
14		m1r 5178	. . . . . . 7 |- -1R e. R.
15		mulclsr 5180	. . . . . . 7 |- ((-1R e. R. /\ (y .R w) e. R.) -> (-1R .R (y .R w)) e. R.)
16	14, 15	mpan 694	. . . . . 6 |- ((y .R w) e. R. -> (-1R .R (y .R w)) e. R.)
17	13, 16	syl 10	. . . . 5 |- ((y e. R. /\ w e. R.) -> (-1R .R (y .R w)) e. R.)
18	11, 12, 17	syl2an 454	. . . 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 508	. . 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 5179	. . . . . 6 |- (((y .R z) e. R. /\ (x .R w) e. R.) -> ((y .R z) +R (x .R w)) e. R.)
21		mulclsr 5180	. . . . . 6 |- ((y e. R. /\ z e. R.) -> (y .R z) e. R.)
22		mulclsr 5180	. . . . . 6 |- ((x e. R. /\ w e. R.) -> (x .R w) e. R.)
23	20, 21, 22	syl2an 454	. . . . 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 436	. . . 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 509	. . 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 288	. 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 5179	. . . . 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 5180	. . . . 5 |- ((x e. R. /\ v e. R.) -> (x .R v) e. R.)
29		mulclsr 5180	. . . . . 6 |- ((y e. R. /\ u e. R.) -> (y .R u) e. R.)
30		mulclsr 5180	. . . . . . 7 |- ((-1R e. R. /\ (y .R u) e. R.) -> (-1R .R (y .R u)) e. R.)
31	14, 30	mpan 694	. . . . . 6 |- ((y .R u) e. R. -> (-1R .R (y .R u)) e. R.)
32	29, 31	syl 10	. . . . 5 |- ((y e. R. /\ u e. R.) -> (-1R .R (y .R u)) e. R.)
33	27, 28, 32	syl2an 454	. . . 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 508	. . 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 5179	. . . . . 6 |- (((y .R v) e. R. /\ (x .R u) e. R.) -> ((y .R v) +R (x .R u)) e. R.)
36		mulclsr 5180	. . . . . 6 |- ((y e. R. /\ v e. R.) -> (y .R v) e. R.)
37		mulclsr 5180	. . . . . 6 |- ((x e. R. /\ u e. R.) -> (x .R u) e. R.)
38	35, 36, 37	syl2an 454	. . . . 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 436	. . . 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 509	. . 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 288	. 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 1811	. . . . 5 |- z e. V
43		visset 1811	. . . . 5 |- v e. V
44	42, 43	distrsr 5187	. . . 4 |- (x .R (z +R v)) = ((x .R z) +R (x .R v))
45		visset 1811	. . . . . . 7 |- w e. V
46		visset 1811	. . . . . . 7 |- u e. V
47	45, 46	distrsr 5187	. . . . . 6 |- (y .R (w +R u)) = ((y .R w) +R (y .R u))
48	47	opreq2i 3969	. . . . 5 |- (-1R .R (y .R (w +R u))) = (-1R .R ((y .R w) +R (y .R u)))
49		oprex 3980	. . . . . 6 |- (y .R w) e. V
50		oprex 3980	. . . . . 6 |- (y .R u) e. V
51	49, 50	distrsr 5187	. . . . 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 1494	. . . 4 |- (-1R .R (y .R (w +R u))) = ((-1R .R (y .R w)) +R (-1R .R (y .R u)))
53	44, 52	opreq12i 3970	. . 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 3980	. . . 4 |- (x .R z) e. V
55		oprex 3980	. . . 4 |- (x .R v) e. V
56		oprex 3980	. . . 4 |- (-1R .R