Theorem axdistr 11079

Description: Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-distr 11103 be used later. Instead, use adddi 11125. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)

Assertion

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

Proof of Theorem axdistr

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

Step	Hyp	Ref	Expression
1		dfcnqs 11063	. 2 ⊢ ℂ = ((R × R) / ◡ E )
2		addcnsrec 11064	. 2 ⊢ (((𝑧 ∈ R ∧ 𝑤 ∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) → ([⟨𝑧, 𝑤⟩]◡ E + [⟨𝑣, 𝑢⟩]◡ E ) = [⟨(𝑧 +R 𝑣), (𝑤 +R 𝑢)⟩]◡ E )
3		mulcnsrec 11065	. 2 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ ((𝑧 +R 𝑣) ∈ R ∧ (𝑤 +R 𝑢) ∈ R)) → ([⟨𝑥, 𝑦⟩]◡ E · [⟨(𝑧 +R 𝑣), (𝑤 +R 𝑢)⟩]◡ E ) = [⟨((𝑥 ·R (𝑧 +R 𝑣)) +R (-1R ·R (𝑦 ·R (𝑤 +R 𝑢)))), ((𝑦 ·R (𝑧 +R 𝑣)) +R (𝑥 ·R (𝑤 +R 𝑢)))⟩]◡ E )
4		mulcnsrec 11065	. 2 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → ([⟨𝑥, 𝑦⟩]◡ E · [⟨𝑧, 𝑤⟩]◡ E ) = [⟨((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))), ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤))⟩]◡ E )
5		mulcnsrec 11065	. 2 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) → ([⟨𝑥, 𝑦⟩]◡ E · [⟨𝑣, 𝑢⟩]◡ E ) = [⟨((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))), ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢))⟩]◡ E )
6		addcnsrec 11064	. 2 ⊢ (((((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R ∧ ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R) ∧ (((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))) ∈ R ∧ ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)) ∈ R)) → ([⟨((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))), ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤))⟩]◡ E + [⟨((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))), ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢))⟩]◡ E ) = [⟨(((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) +R ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢)))), (((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) +R ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)))⟩]◡ E )
7		addclsr 11004	. . . 4 ⊢ ((𝑧 ∈ R ∧ 𝑣 ∈ R) → (𝑧 +R 𝑣) ∈ R)
8		addclsr 11004	. . . 4 ⊢ ((𝑤 ∈ R ∧ 𝑢 ∈ R) → (𝑤 +R 𝑢) ∈ R)
9	7, 8	anim12i 619	. . 3 ⊢ (((𝑧 ∈ R ∧ 𝑣 ∈ R) ∧ (𝑤 ∈ R ∧ 𝑢 ∈ R)) → ((𝑧 +R 𝑣) ∈ R ∧ (𝑤 +R 𝑢) ∈ R))
10	9	an4s 666	. 2 ⊢ (((𝑧 ∈ R ∧ 𝑤 ∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) → ((𝑧 +R 𝑣) ∈ R ∧ (𝑤 +R 𝑢) ∈ R))
11		mulclsr 11005	. . . . 5 ⊢ ((𝑥 ∈ R ∧ 𝑧 ∈ R) → (𝑥 ·R 𝑧) ∈ R)
12		m1r 11003	. . . . . 6 ⊢ -1R ∈ R
13		mulclsr 11005	. . . . . 6 ⊢ ((𝑦 ∈ R ∧ 𝑤 ∈ R) → (𝑦 ·R 𝑤) ∈ R)
14		mulclsr 11005	. . . . . 6 ⊢ ((-1R ∈ R ∧ (𝑦 ·R 𝑤) ∈ R) → (-1R ·R (𝑦 ·R 𝑤)) ∈ R)
15	12, 13, 14	sylancr 593	. . . . 5 ⊢ ((𝑦 ∈ R ∧ 𝑤 ∈ R) → (-1R ·R (𝑦 ·R 𝑤)) ∈ R)
16		addclsr 11004	. . . . 5 ⊢ (((𝑥 ·R 𝑧) ∈ R ∧ (-1R ·R (𝑦 ·R 𝑤)) ∈ R) → ((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R)
17	11, 15, 16	syl2an 602	. . . 4 ⊢ (((𝑥 ∈ R ∧ 𝑧 ∈ R) ∧ (𝑦 ∈ R ∧ 𝑤 ∈ R)) → ((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R)
18	17	an4s 666	. . 3 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → ((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R)
19		mulclsr 11005	. . . . 5 ⊢ ((𝑦 ∈ R ∧ 𝑧 ∈ R) → (𝑦 ·R 𝑧) ∈ R)
20		mulclsr 11005	. . . . 5 ⊢ ((𝑥 ∈ R ∧ 𝑤 ∈ R) → (𝑥 ·R 𝑤) ∈ R)
21		addclsr 11004	. . . . 5 ⊢ (((𝑦 ·R 𝑧) ∈ R ∧ (𝑥 ·R 𝑤) ∈ R) → ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R)
22	19, 20, 21	syl2anr 603	. . . 4 ⊢ (((𝑥 ∈ R ∧ 𝑤 ∈ R) ∧ (𝑦 ∈ R ∧ 𝑧 ∈ R)) → ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R)
23	22	an42s 667	. . 3 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R)
24	18, 23	jca 516	. 2 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑧 ∈ R ∧ 𝑤 ∈ R)) → (((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R ∧ ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R))
25		mulclsr 11005	. . . . 5 ⊢ ((𝑥 ∈ R ∧ 𝑣 ∈ R) → (𝑥 ·R 𝑣) ∈ R)
26		mulclsr 11005	. . . . . 6 ⊢ ((𝑦 ∈ R ∧ 𝑢 ∈ R) → (𝑦 ·R 𝑢) ∈ R)
27		mulclsr 11005	. . . . . 6 ⊢ ((-1R ∈ R ∧ (𝑦 ·R 𝑢) ∈ R) → (-1R ·R (𝑦 ·R 𝑢)) ∈ R)
28	12, 26, 27	sylancr 593	. . . . 5 ⊢ ((𝑦 ∈ R ∧ 𝑢 ∈ R) → (-1R ·R (𝑦 ·R 𝑢)) ∈ R)
29		addclsr 11004	. . . . 5 ⊢ (((𝑥 ·R 𝑣) ∈ R ∧ (-1R ·R (𝑦 ·R 𝑢)) ∈ R) → ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))) ∈ R)
30	25, 28, 29	syl2an 602	. . . 4 ⊢ (((𝑥 ∈ R ∧ 𝑣 ∈ R) ∧ (𝑦 ∈ R ∧ 𝑢 ∈ R)) → ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))) ∈ R)
31	30	an4s 666	. . 3 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) → ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))) ∈ R)
32		mulclsr 11005	. . . . 5 ⊢ ((𝑦 ∈ R ∧ 𝑣 ∈ R) → (𝑦 ·R 𝑣) ∈ R)
33		mulclsr 11005	. . . . 5 ⊢ ((𝑥 ∈ R ∧ 𝑢 ∈ R) → (𝑥 ·R 𝑢) ∈ R)
34		addclsr 11004	. . . . 5 ⊢ (((𝑦 ·R 𝑣) ∈ R ∧ (𝑥 ·R 𝑢) ∈ R) → ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)) ∈ R)
35	32, 33, 34	syl2anr 603	. . . 4 ⊢ (((𝑥 ∈ R ∧ 𝑢 ∈ R) ∧ (𝑦 ∈ R ∧ 𝑣 ∈ R)) → ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)) ∈ R)
36	35	an42s 667	. . 3 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) → ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)) ∈ R)
37	31, 36	jca 516	. 2 ⊢ (((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧ (𝑣 ∈ R ∧ 𝑢 ∈ R)) → (((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))) ∈ R ∧ ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)) ∈ R))
38		distrsr 11012	. . . 4 ⊢ (𝑥 ·R (𝑧 +R 𝑣)) = ((𝑥 ·R 𝑧) +R (𝑥 ·R 𝑣))
39		distrsr 11012	. . . . . 6 ⊢ (𝑦 ·R (𝑤 +R 𝑢)) = ((𝑦 ·R 𝑤) +R (𝑦 ·R 𝑢))
40	39	oveq2i 7374	. . . . 5 ⊢ (-1R ·R (𝑦 ·R (𝑤 +R 𝑢))) = (-1R ·R ((𝑦 ·R 𝑤) +R (𝑦 ·R 𝑢)))
41		distrsr 11012	. . . . 5 ⊢ (-1R ·R ((𝑦 ·R 𝑤) +R (𝑦 ·R 𝑢))) = ((-1R ·R (𝑦 ·R 𝑤)) +R (-1R ·R (𝑦 ·R 𝑢)))
42	40, 41	eqtri 2763	. . . 4 ⊢ (-1R ·R (𝑦 ·R (𝑤 +R 𝑢))) = ((-1R ·R (𝑦 ·R 𝑤)) +R (-1R ·R (𝑦 ·R 𝑢)))
43	38, 42	oveq12i 7375	. . 3 ⊢ ((𝑥 ·R (𝑧 +R 𝑣)) +R (-1R ·R (𝑦 ·R (𝑤 +R 𝑢)))) = (((𝑥 ·R 𝑧) +R (𝑥 ·R 𝑣)) +R ((-1R ·R (𝑦 ·R 𝑤)) +R (-1R ·R (𝑦 ·R 𝑢))))
44		ovex 7396	. . . 4 ⊢ (𝑥 ·R 𝑧) ∈ V
45		ovex 7396	. . . 4 ⊢ (𝑥 ·R 𝑣) ∈ V
46		ovex 7396	. . . 4 ⊢ (-1R ·R (𝑦 ·R 𝑤)) ∈ V
47		addcomsr 11008	. . . 4 ⊢ (𝑓 +R 𝑔) = (𝑔 +R 𝑓)
48		addasssr 11009	. . . 4 ⊢ ((𝑓 +R 𝑔) +R ℎ) = (𝑓 +R (𝑔 +R ℎ))
49		ovex 7396	. . . 4 ⊢ (-1R ·R (𝑦 ·R 𝑢)) ∈ V
50	44, 45, 46, 47, 48, 49	caov4 7594	. . 3 ⊢ (((𝑥 ·R 𝑧) +R (𝑥 ·R 𝑣)) +R ((-1R ·R (𝑦 ·R 𝑤)) +R (-1R ·R (𝑦 ·R 𝑢)))) = (((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) +R ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))))
51	43, 50	eqtri 2763	. 2 ⊢ ((𝑥 ·R (𝑧 +R 𝑣)) +R (-1R ·R (𝑦 ·R (𝑤 +R 𝑢)))) = (((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) +R ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))))
52		distrsr 11012	. . . 4 ⊢ (𝑦 ·R (𝑧 +R 𝑣)) = ((𝑦 ·R 𝑧) +R (𝑦 ·R 𝑣))
53		distrsr 11012	. . . 4 ⊢ (𝑥 ·R (𝑤 +R 𝑢)) = ((𝑥 ·R 𝑤) +R (𝑥 ·R 𝑢))
54	52, 53	oveq12i 7375	. . 3 ⊢ ((𝑦 ·R (𝑧 +R 𝑣)) +R (𝑥 ·R (𝑤 +R 𝑢))) = (((𝑦 ·R 𝑧) +R (𝑦 ·R 𝑣)) +R ((𝑥 ·R 𝑤) +R (𝑥 ·R 𝑢)))
55		ovex 7396	. . . 4 ⊢ (𝑦 ·R 𝑧) ∈ V
56		ovex 7396	. . . 4 ⊢ (𝑦 ·R 𝑣) ∈ V
57		ovex 7396	. . . 4 ⊢ (𝑥 ·R 𝑤) ∈ V
58		ovex 7396	. . . 4 ⊢ (𝑥 ·R 𝑢) ∈ V
59	55, 56, 57, 47, 48, 58	caov4 7594	. . 3 ⊢ (((𝑦 ·R 𝑧) +R (𝑦 ·R 𝑣)) +R ((𝑥 ·R 𝑤) +R (𝑥 ·R 𝑢))) = (((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) +R ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)))
60	54, 59	eqtri 2763	. 2 ⊢ ((𝑦 ·R (𝑧 +R 𝑣)) +R (𝑥 ·R (𝑤 +R 𝑢))) = (((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) +R ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)))
61	1, 2, 3, 4, 5, 6, 10, 24, 37, 51, 60	ecovdi 8769	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   E cep 5524  ^◡ccnv 5624  (class class class)co 7363  Rcnr 10786  -1_Rcm1r 10789   +_R cplr 10790   ·_R cmr 10791  ℂcc 11034   + caddc 11039   · cmul 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-inf2 9560

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-int 4885  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-om 7814  df-1st 7938  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-1o 8402  df-oadd 8406  df-omul 8407  df-er 8640  df-ec 8642  df-qs 8646  df-ni 10793  df-pli 10794  df-mi 10795  df-lti 10796  df-plpq 10829  df-mpq 10830  df-ltpq 10831  df-enq 10832  df-nq 10833  df-erq 10834  df-plq 10835  df-mq 10836  df-1nq 10837  df-rq 10838  df-ltnq 10839  df-np 10902  df-1p 10903  df-plp 10904  df-mp 10905  df-ltp 10906  df-enr 10976  df-nr 10977  df-plr 10978  df-mr 10979  df-m1r 10983  df-c 11042  df-add 11047  df-mul 11048

This theorem is referenced by: (None)