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 ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → (A · (B + C)) = ((A · B) + (A · C)))

Proof of Theorem axdistr

Step	Hyp	Ref	Expression
1		dfcnqs 5249	. 2 ⊢ ℂ = ((R × R) / ◡E)
2		addcnsrec 5250	. 2 ⊢ (((z ∈ R ⋀ w ∈ R) ⋀ (v ∈ R ⋀ u ∈ R)) → ([⟨z, w⟩]◡E + [⟨v, u⟩]◡E) = [⟨(z +R v), (w +R u)⟩]◡E)
3		mulcnsrec 5251	. 2 ⊢ (((x ∈ R ⋀ y ∈ R) ⋀ ((z +R v) ∈ R ⋀ (w +R u) ∈ R)) → ([⟨x, y⟩]◡E · [⟨(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 ∈ R ⋀ y ∈ R) ⋀ (z ∈ R ⋀ w ∈ R)) → ([⟨x, y⟩]◡E · [⟨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 ∈ R ⋀ y ∈ R) ⋀ (v ∈ R ⋀ u ∈ R)) → ([⟨x, y⟩]◡E · [⟨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))) ∈ R ⋀ ((y ·R z) +R (x ·R w)) ∈ R) ⋀ (((x ·R v) +R (-1R ·R (y ·R u))) ∈ R ⋀ ((y ·R v) +R (x ·R u)) ∈ 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 ∈ R ⋀ v ∈ R) → (z +R v) ∈ R)
8		addclsr 5179	. . . 4 ⊢ ((w ∈ R ⋀ u ∈ R) → (w +R u) ∈ R)
9	7, 8	anim12i 333	. . 3 ⊢ (((z ∈ R ⋀ v ∈ R) ⋀ (w ∈ R ⋀ u ∈ R)) → ((z +R v) ∈ R ⋀ (w +R u) ∈ R))
10	9	an4s 508	. 2 ⊢ (((z ∈ R ⋀ w ∈ R) ⋀ (v ∈ R ⋀ u ∈ R)) → ((z +R v) ∈ R ⋀ (w +R u) ∈ R))
11		addclsr 5179	. . . . 5 ⊢ (((x ·R z) ∈ R ⋀ (-1R ·R (y ·R w)) ∈ R) → ((x ·R z) +R (-1R ·R (y ·R w))) ∈ R)
12		mulclsr 5180	. . . . 5 ⊢ ((x ∈ R ⋀ z ∈ R) → (x ·R z) ∈ R)
13		mulclsr 5180	. . . . . 6 ⊢ ((y ∈ R ⋀ w ∈ R) → (y ·R w) ∈ R)
14		m1r 5178	. . . . . . 7 ⊢ -1R ∈ R
15		mulclsr 5180	. . . . . . 7 ⊢ ((-1R ∈ R ⋀ (y ·R w) ∈ R) → (-1R ·R (y ·R w)) ∈ R)
16	14, 15	mpan 694	. . . . . 6 ⊢ ((y ·R w) ∈ R → (-1R ·R (y ·R w)) ∈ R)
17	13, 16	syl 10	. . . . 5 ⊢ ((y ∈ R ⋀ w ∈ R) → (-1R ·R (y ·R w)) ∈ R)
18	11, 12, 17	syl2an 454	. . . 4 ⊢ (((x ∈ R ⋀ z ∈ R) ⋀ (y ∈ R ⋀ w ∈ R)) → ((x ·R z) +R (-1R ·R (y ·R w))) ∈ R)
19	18	an4s 508	. . 3 ⊢ (((x ∈ R ⋀ y ∈ R) ⋀ (z ∈ R ⋀ w ∈ R)) → ((x ·R z) +R (-1R ·R (y ·R w))) ∈ R)
20		addclsr 5179	. . . . . 6 ⊢ (((y ·R z) ∈ R ⋀ (x ·R w) ∈ R) → ((y ·R z) +R (x ·R w)) ∈ R)
21		mulclsr 5180	. . . . . 6 ⊢ ((y ∈ R ⋀ z ∈ R) → (y ·R z) ∈ R)
22		mulclsr 5180	. . . . . 6 ⊢ ((x ∈ R ⋀ w ∈ R) → (x ·R w) ∈ R)
23	20, 21, 22	syl2an 454	. . . . 5 ⊢ (((y ∈ R ⋀ z ∈ R) ⋀ (x ∈ R ⋀ w ∈ R)) → ((y ·R z) +R (x ·R w)) ∈ R)
24	23	ancoms 436	. . . 4 ⊢ (((x ∈ R ⋀ w ∈ R) ⋀ (y ∈ R ⋀ z ∈ R)) → ((y ·R z) +R (x ·R w)) ∈ R)
25	24	an42s 509	. . 3 ⊢ (((x ∈ R ⋀ y ∈ R) ⋀ (z ∈ R ⋀ w ∈ R)) → ((y ·R z) +R (x ·R w)) ∈ R)
26	19, 25	jca 288	. 2 ⊢ (((x ∈ R ⋀ y ∈ R) ⋀ (z ∈ R ⋀ w ∈ R)) → (((x ·R z) +R (-1R ·R (y ·R w))) ∈ R ⋀ ((y ·R z) +R (x ·R w)) ∈ R))
27		addclsr 5179	. . . . 5 ⊢ (((x ·R v) ∈ R ⋀ (-1R ·R (y ·R u)) ∈ R) → ((x ·R v) +R (-1R ·R (y ·R u))) ∈ R)
28		mulclsr 5180	. . . . 5 ⊢ ((x ∈ R ⋀ v ∈ R) → (x ·R v) ∈ R)
29		mulclsr 5180	. . . . . 6 ⊢ ((y ∈ R ⋀ u ∈ R) → (y ·R u) ∈ R)
30		mulclsr 5180	. . . . . . 7 ⊢ ((-1R ∈ R ⋀ (y ·R u) ∈ R) → (-1R ·R (y ·R u)) ∈ R)
31	14, 30	mpan 694	. . . . . 6 ⊢ ((y ·R u) ∈ R → (-1R ·R (y ·R u)) ∈ R)
32	29, 31	syl 10	. . . . 5 ⊢ ((y ∈ R ⋀ u ∈ R) → (-1R ·R (y ·R u)) ∈ R)
33	27, 28, 32	syl2an 454	. . . 4 ⊢ (((x ∈ R ⋀ v ∈ R) ⋀ (y ∈ R ⋀ u ∈ R)) → ((x ·R v) +R (-1R ·R (y ·R u))) ∈ R)
34	33	an4s 508	. . 3 ⊢ (((x ∈ R ⋀ y ∈ R) ⋀ (v ∈ R ⋀ u ∈ R)) → ((x ·R v) +R (-1R ·R (y ·R u))) ∈ R)
35		addclsr 5179	. . . . . 6 ⊢ (((y ·R v) ∈ R ⋀ (x ·R u) ∈ R) → ((y ·R v) +R (x ·R u)) ∈ R)
36		mulclsr 5180	. . . . . 6 ⊢ ((y ∈ R ⋀ v ∈ R) → (y ·R v) ∈ R)
37		mulclsr 5180	. . . . . 6 ⊢ ((x ∈ R ⋀ u ∈ R) → (x ·R u) ∈ R)
38	35, 36, 37	syl2an 454	. . . . 5 ⊢ (((y ∈ R ⋀ v ∈ R) ⋀ (x ∈ R ⋀ u ∈ R)) → ((y ·R v) +R (x ·R u)) ∈ R)
39	38	ancoms 436	. . . 4 ⊢ (((x ∈ R ⋀ u ∈ R) ⋀ (y ∈ R ⋀ v ∈ R)) → ((y ·R v) +R (x ·R u)) ∈ R)
40	39	an42s 509	. . 3 ⊢ (((x ∈ R ⋀ y ∈ R) ⋀ (v ∈ R ⋀ u ∈ R)) → ((y ·R v) +R (x ·R u)) ∈ R)
41	34, 40	jca 288	. 2 ⊢ (((x ∈ R ⋀ y ∈ R) ⋀ (v ∈ R ⋀ u ∈ R)) → (((x ·R v) +R (-1R ·R (y ·R u))) ∈ R ⋀ ((y ·R v) +R (x ·R u)) ∈ R))
42		visset 1811	. . . . 5 ⊢ z ∈ V
43		visset 1811	. . . . 5 ⊢ v ∈ V
44	42, 43	distrsr 5187	. . . 4 ⊢ (x ·R (z +R v)) = ((x ·R z) +R (x ·R v))
45		visset 1811	. . . . . . 7 ⊢ w ∈ V
46		visset 1811	. . . . . . 7 ⊢ u ∈ 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) ∈ V
50		oprex 3980	. . . . . 6 ⊢ (y ·R u) ∈ 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) ∈ V
55		oprex 3980	. . . 4 ⊢ (x ·R v) ∈ V
56		oprex 3980	. . . 4 ⊢ (-1R ·R (y ·R w)) ∈ V
57		visset 1811	. . . . 5 ⊢ f ∈ V
58		visset 1811	. . . . 5 ⊢ g ∈ V
59	57, 58	addcomsr 5183	. . . 4 ⊢ (f +R g) = (g +R f)
60		visset 1811	. . . . 5 ⊢ h ∈ V
61	58, 60	addasssr 5184	. . . 4 ⊢ ((f +R g) +R h) = (f +R (g +R h))
62		oprex 3980	. . . 4 ⊢ (-1R ·R (y ·R u)) ∈ V
63	54, 55, 56, 59, 61, 62	caopr4 4061	. . 3 ⊢ (((x ·R z) +R (x ·R v)) +R ((-1R ·R (y ·R w)) +R (-1R ·R (y ·R u)))) = (((x ·R z) +R (-1R ·R (y ·R w))) +R ((x ·R v) +R (-1R ·R (y ·R u))))
64	53, 63	eqtr 1494	. 2 ⊢ ((x ·R (z +R v)) +R (-1R ·R (y ·R (w +R u)))) = (((x ·R z) +R (-1R ·R (y ·R w))) +R ((x ·R v) +R (-1R ·R (y ·R u))))
65	42, 43	distrsr 5187	. . . 4 ⊢ (y ·R (z +R v)) = ((y ·R z) +R (y ·R v))
66	45, 46	distrsr 5187	. . . 4 ⊢ (x ·R (w +R u)) = ((x ·R w) +R (x ·R u))
67	65, 66	opreq12i 3970	. . 3 ⊢ ((y ·R (z +R v)) +R (x ·R (w +R u))) = (((y ·R z) +R (y ·R v)) +R ((x ·R w) +R (x ·R u)))
68		oprex 3980	. . . 4 ⊢ (y ·R z) ∈ V
69		oprex 3980	. . . 4 ⊢ (y ·R v) ∈ V
70		oprex 3980	. . . 4 ⊢ (x ·R w) ∈ V
71		oprex 3980	. . . 4 ⊢ (x ·R u) ∈ V
72	68, 69, 70, 59, 61, 71	caopr4 4061	. . 3 ⊢ (((y ·R z) +R (y ·R v)) +R ((x ·R w) +R (x ·R u))) = (((y ·R z) +R (x ·R w)) +R ((y ·R v) +R (x ·R u)))
73	67, 72	eqtr 1494	. 2 ⊢ ((y ·R (z +R v)) +R (x ·R (w +R u))) = (((y ·R z) +R (x ·R w)) +R ((y ·R v) +R (x ·R u)))
74	1, 2, 3, 4, 5, 6, 10, 26, 41, 64, 73	ecoprdi 4318	1 ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) → (A · (B + C)) = ((A · B) + (A · C)))

Syntax hints:   → wi 3   ⋀ wa 223   ⋀ w3a 774   = wceq 955   ∈ wcel 957  Ecep 2827  ^◡ccnv 3166  (class class class)co 3960  Rcnr 4980  -1_Rcm1r 4983   +_R cplr 4984   ·_R cmr 4985  ℂcc 5219   + caddc 5224   · cmul 5226

This theorem is referenced by:  adddit 5296  adddirt 5306  adddi 5313  cnegext 5335  muladdt 5408  muladd11t 5409  subdit 5414  conjmult 5767  nnmulclt 5903  expmult 6547  bernneq 6602  imret 6731  imretOLD 6732  fsummulc1 7001  binomlem5 7038  efexpt 7350  efi4pt 7413  cos01bndlem3 7449  demoivre 7462  cnring 8147  cnvc 8187  ipasslem2 8475  efgh 8697  shftefif1olem 8725  hhph 9032  hhphOLD 9033  mslb1 10580

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2690  ax-sep 2700  ax-nul 2707  ax-pow 2739  ax-pr 2776  ax-un 2863  ax-inf2 4612

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-ral 1648  df-rex 1649  df-reu 1650  df-rab 1651  df-v 1810  df-sbc 1940  df-csb 2000  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-pss 2053  df-nul 2279  df-if 2360  df-pw 2400  df-sn 2410  df-pr 2411  df-tp 2413  df-op 2414  df-uni 2501  df-int 2531  df-iun 2565  df-br 2617  df-opab 2664  df-tr 2678  df-eprel 2829  df-id 2832  df-po 2837  df-so 2847  df-fr 2914  df-we 2931  df-ord 2948  df-on 2949  df-lim 2950  df-suc 2951  df-om 3129  df-xp 3181  df-rel 3182  df-cnv 3183  df-co 3184  df-dm 3185  df-rn 3186  df-res 3187  df-ima 3188  df-fun 3189  df-fn 3190  df-f 3191  df-fv 3195  df-rdg 3929  df-opr 3962  df-oprab 3963  df-1st 4076  df-2nd 4077  df-1o 4130  df-oadd 4132  df-omul 4133  df-er 4258  df-ec 4260  df-qs 4263  df-ni 4987  df-pli 4988  df-mi 4989  df-lti 4990  df-plpq 5022  df-mpq 5023  df-enq 5024  df-nq 5025  df-plq 5026  df-mq 5027  df-rq 5028  df-ltq 5029  df-1q 5030  df-np 5073  df-1p 5074  df-plp 5075  df-mp 5076  df-ltp 5077  df-plpr 5151  df-mpr 5152  df-enr 5153  df-nr 5154  df-plr 5155  df-mr 5156  df-m1r 5160  df-c 5227  df-plus 5232  df-mul 5233

Copyright terms: Public domain