MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axdistr Structured version   Visualization version   GIF version

Theorem axdistr 9964
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 9988 be used later. Instead, use adddi 10010. (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.
StepHypRef Expression
1 dfcnqs 9948 . 2 ℂ = ((R × R) / E )
2 addcnsrec 9949 . 2 (((𝑧R𝑤R) ∧ (𝑣R𝑢R)) → ([⟨𝑧, 𝑤⟩] E + [⟨𝑣, 𝑢⟩] E ) = [⟨(𝑧 +R 𝑣), (𝑤 +R 𝑢)⟩] E )
3 mulcnsrec 9950 . 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 9950 . 2 (((𝑥R𝑦R) ∧ (𝑧R𝑤R)) → ([⟨𝑥, 𝑦⟩] E · [⟨𝑧, 𝑤⟩] E ) = [⟨((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))), ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤))⟩] E )
5 mulcnsrec 9950 . 2 (((𝑥R𝑦R) ∧ (𝑣R𝑢R)) → ([⟨𝑥, 𝑦⟩] E · [⟨𝑣, 𝑢⟩] E ) = [⟨((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))), ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢))⟩] E )
6 addcnsrec 9949 . 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 9889 . . . 4 ((𝑧R𝑣R) → (𝑧 +R 𝑣) ∈ R)
8 addclsr 9889 . . . 4 ((𝑤R𝑢R) → (𝑤 +R 𝑢) ∈ R)
97, 8anim12i 589 . . 3 (((𝑧R𝑣R) ∧ (𝑤R𝑢R)) → ((𝑧 +R 𝑣) ∈ R ∧ (𝑤 +R 𝑢) ∈ R))
109an4s 868 . 2 (((𝑧R𝑤R) ∧ (𝑣R𝑢R)) → ((𝑧 +R 𝑣) ∈ R ∧ (𝑤 +R 𝑢) ∈ R))
11 mulclsr 9890 . . . . 5 ((𝑥R𝑧R) → (𝑥 ·R 𝑧) ∈ R)
12 m1r 9888 . . . . . 6 -1RR
13 mulclsr 9890 . . . . . 6 ((𝑦R𝑤R) → (𝑦 ·R 𝑤) ∈ R)
14 mulclsr 9890 . . . . . 6 ((-1RR ∧ (𝑦 ·R 𝑤) ∈ R) → (-1R ·R (𝑦 ·R 𝑤)) ∈ R)
1512, 13, 14sylancr 694 . . . . 5 ((𝑦R𝑤R) → (-1R ·R (𝑦 ·R 𝑤)) ∈ R)
16 addclsr 9889 . . . . 5 (((𝑥 ·R 𝑧) ∈ R ∧ (-1R ·R (𝑦 ·R 𝑤)) ∈ R) → ((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R)
1711, 15, 16syl2an 494 . . . 4 (((𝑥R𝑧R) ∧ (𝑦R𝑤R)) → ((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R)
1817an4s 868 . . 3 (((𝑥R𝑦R) ∧ (𝑧R𝑤R)) → ((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R)
19 mulclsr 9890 . . . . 5 ((𝑦R𝑧R) → (𝑦 ·R 𝑧) ∈ R)
20 mulclsr 9890 . . . . 5 ((𝑥R𝑤R) → (𝑥 ·R 𝑤) ∈ R)
21 addclsr 9889 . . . . 5 (((𝑦 ·R 𝑧) ∈ R ∧ (𝑥 ·R 𝑤) ∈ R) → ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R)
2219, 20, 21syl2anr 495 . . . 4 (((𝑥R𝑤R) ∧ (𝑦R𝑧R)) → ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R)
2322an42s 869 . . 3 (((𝑥R𝑦R) ∧ (𝑧R𝑤R)) → ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R)
2418, 23jca 554 . 2 (((𝑥R𝑦R) ∧ (𝑧R𝑤R)) → (((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R ∧ ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R))
25 mulclsr 9890 . . . . 5 ((𝑥R𝑣R) → (𝑥 ·R 𝑣) ∈ R)
26 mulclsr 9890 . . . . . 6 ((𝑦R𝑢R) → (𝑦 ·R 𝑢) ∈ R)
27 mulclsr 9890 . . . . . 6 ((-1RR ∧ (𝑦 ·R 𝑢) ∈ R) → (-1R ·R (𝑦 ·R 𝑢)) ∈ R)
2812, 26, 27sylancr 694 . . . . 5 ((𝑦R𝑢R) → (-1R ·R (𝑦 ·R 𝑢)) ∈ R)
29 addclsr 9889 . . . . 5 (((𝑥 ·R 𝑣) ∈ R ∧ (-1R ·R (𝑦 ·R 𝑢)) ∈ R) → ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))) ∈ R)
3025, 28, 29syl2an 494 . . . 4 (((𝑥R𝑣R) ∧ (𝑦R𝑢R)) → ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))) ∈ R)
3130an4s 868 . . 3 (((𝑥R𝑦R) ∧ (𝑣R𝑢R)) → ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))) ∈ R)
32 mulclsr 9890 . . . . 5 ((𝑦R𝑣R) → (𝑦 ·R 𝑣) ∈ R)
33 mulclsr 9890 . . . . 5 ((𝑥R𝑢R) → (𝑥 ·R 𝑢) ∈ R)
34 addclsr 9889 . . . . 5 (((𝑦 ·R 𝑣) ∈ R ∧ (𝑥 ·R 𝑢) ∈ R) → ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)) ∈ R)
3532, 33, 34syl2anr 495 . . . 4 (((𝑥R𝑢R) ∧ (𝑦R𝑣R)) → ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)) ∈ R)
3635an42s 869 . . 3 (((𝑥R𝑦R) ∧ (𝑣R𝑢R)) → ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)) ∈ R)
3731, 36jca 554 . 2 (((𝑥R𝑦R) ∧ (𝑣R𝑢R)) → (((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))) ∈ R ∧ ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)) ∈ R))
38 distrsr 9897 . . . 4 (𝑥 ·R (𝑧 +R 𝑣)) = ((𝑥 ·R 𝑧) +R (𝑥 ·R 𝑣))
39 distrsr 9897 . . . . . 6 (𝑦 ·R (𝑤 +R 𝑢)) = ((𝑦 ·R 𝑤) +R (𝑦 ·R 𝑢))
4039oveq2i 6646 . . . . 5 (-1R ·R (𝑦 ·R (𝑤 +R 𝑢))) = (-1R ·R ((𝑦 ·R 𝑤) +R (𝑦 ·R 𝑢)))
41 distrsr 9897 . . . . 5 (-1R ·R ((𝑦 ·R 𝑤) +R (𝑦 ·R 𝑢))) = ((-1R ·R (𝑦 ·R 𝑤)) +R (-1R ·R (𝑦 ·R 𝑢)))
4240, 41eqtri 2642 . . . 4 (-1R ·R (𝑦 ·R (𝑤 +R 𝑢))) = ((-1R ·R (𝑦 ·R 𝑤)) +R (-1R ·R (𝑦 ·R 𝑢)))
4338, 42oveq12i 6647 . . 3 ((𝑥 ·R (𝑧 +R 𝑣)) +R (-1R ·R (𝑦 ·R (𝑤 +R 𝑢)))) = (((𝑥 ·R 𝑧) +R (𝑥 ·R 𝑣)) +R ((-1R ·R (𝑦 ·R 𝑤)) +R (-1R ·R (𝑦 ·R 𝑢))))
44 ovex 6663 . . . 4 (𝑥 ·R 𝑧) ∈ V
45 ovex 6663 . . . 4 (𝑥 ·R 𝑣) ∈ V
46 ovex 6663 . . . 4 (-1R ·R (𝑦 ·R 𝑤)) ∈ V
47 addcomsr 9893 . . . 4 (𝑓 +R 𝑔) = (𝑔 +R 𝑓)
48 addasssr 9894 . . . 4 ((𝑓 +R 𝑔) +R ) = (𝑓 +R (𝑔 +R ))
49 ovex 6663 . . . 4 (-1R ·R (𝑦 ·R 𝑢)) ∈ V
5044, 45, 46, 47, 48, 49caov4 6850 . . 3 (((𝑥 ·R 𝑧) +R (𝑥 ·R 𝑣)) +R ((-1R ·R (𝑦 ·R 𝑤)) +R (-1R ·R (𝑦 ·R 𝑢)))) = (((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) +R ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))))
5143, 50eqtri 2642 . 2 ((𝑥 ·R (𝑧 +R 𝑣)) +R (-1R ·R (𝑦 ·R (𝑤 +R 𝑢)))) = (((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) +R ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))))
52 distrsr 9897 . . . 4 (𝑦 ·R (𝑧 +R 𝑣)) = ((𝑦 ·R 𝑧) +R (𝑦 ·R 𝑣))
53 distrsr 9897 . . . 4 (𝑥 ·R (𝑤 +R 𝑢)) = ((𝑥 ·R 𝑤) +R (𝑥 ·R 𝑢))
5452, 53oveq12i 6647 . . 3 ((𝑦 ·R (𝑧 +R 𝑣)) +R (𝑥 ·R (𝑤 +R 𝑢))) = (((𝑦 ·R 𝑧) +R (𝑦 ·R 𝑣)) +R ((𝑥 ·R 𝑤) +R (𝑥 ·R 𝑢)))
55 ovex 6663 . . . 4 (𝑦 ·R 𝑧) ∈ V
56 ovex 6663 . . . 4 (𝑦 ·R 𝑣) ∈ V
57 ovex 6663 . . . 4 (𝑥 ·R 𝑤) ∈ V
58 ovex 6663 . . . 4 (𝑥 ·R 𝑢) ∈ V
5955, 56, 57, 47, 48, 58caov4 6850 . . 3 (((𝑦 ·R 𝑧) +R (𝑦 ·R 𝑣)) +R ((𝑥 ·R 𝑤) +R (𝑥 ·R 𝑢))) = (((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) +R ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)))
6054, 59eqtri 2642 . 2 ((𝑦 ·R (𝑧 +R 𝑣)) +R (𝑥 ·R (𝑤 +R 𝑢))) = (((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) +R ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)))
611, 2, 3, 4, 5, 6, 10, 24, 37, 51, 60ecovdi 7841 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036   = wceq 1481  wcel 1988   E cep 5018  ccnv 5103  (class class class)co 6635  Rcnr 9672  -1Rcm1r 9675   +R cplr 9676   ·R cmr 9677  cc 9919   + caddc 9924   · cmul 9926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-omul 7550  df-er 7727  df-ec 7729  df-qs 7733  df-ni 9679  df-pli 9680  df-mi 9681  df-lti 9682  df-plpq 9715  df-mpq 9716  df-ltpq 9717  df-enq 9718  df-nq 9719  df-erq 9720  df-plq 9721  df-mq 9722  df-1nq 9723  df-rq 9724  df-ltnq 9725  df-np 9788  df-1p 9789  df-plp 9790  df-mp 9791  df-ltp 9792  df-enr 9862  df-nr 9863  df-plr 9864  df-mr 9865  df-m1r 9869  df-c 9927  df-add 9932  df-mul 9933
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator