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

Theorem axdistr 10426
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 10450 be used later. Instead, use adddi 10472. (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 10410 . 2 ℂ = ((R × R) / E )
2 addcnsrec 10411 . 2 (((𝑧R𝑤R) ∧ (𝑣R𝑢R)) → ([⟨𝑧, 𝑤⟩] E + [⟨𝑣, 𝑢⟩] E ) = [⟨(𝑧 +R 𝑣), (𝑤 +R 𝑢)⟩] E )
3 mulcnsrec 10412 . 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 10412 . 2 (((𝑥R𝑦R) ∧ (𝑧R𝑤R)) → ([⟨𝑥, 𝑦⟩] E · [⟨𝑧, 𝑤⟩] E ) = [⟨((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))), ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤))⟩] E )
5 mulcnsrec 10412 . 2 (((𝑥R𝑦R) ∧ (𝑣R𝑢R)) → ([⟨𝑥, 𝑦⟩] E · [⟨𝑣, 𝑢⟩] E ) = [⟨((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))), ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢))⟩] E )
6 addcnsrec 10411 . 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 10351 . . . 4 ((𝑧R𝑣R) → (𝑧 +R 𝑣) ∈ R)
8 addclsr 10351 . . . 4 ((𝑤R𝑢R) → (𝑤 +R 𝑢) ∈ R)
97, 8anim12i 612 . . 3 (((𝑧R𝑣R) ∧ (𝑤R𝑢R)) → ((𝑧 +R 𝑣) ∈ R ∧ (𝑤 +R 𝑢) ∈ R))
109an4s 656 . 2 (((𝑧R𝑤R) ∧ (𝑣R𝑢R)) → ((𝑧 +R 𝑣) ∈ R ∧ (𝑤 +R 𝑢) ∈ R))
11 mulclsr 10352 . . . . 5 ((𝑥R𝑧R) → (𝑥 ·R 𝑧) ∈ R)
12 m1r 10350 . . . . . 6 -1RR
13 mulclsr 10352 . . . . . 6 ((𝑦R𝑤R) → (𝑦 ·R 𝑤) ∈ R)
14 mulclsr 10352 . . . . . 6 ((-1RR ∧ (𝑦 ·R 𝑤) ∈ R) → (-1R ·R (𝑦 ·R 𝑤)) ∈ R)
1512, 13, 14sylancr 587 . . . . 5 ((𝑦R𝑤R) → (-1R ·R (𝑦 ·R 𝑤)) ∈ R)
16 addclsr 10351 . . . . 5 (((𝑥 ·R 𝑧) ∈ R ∧ (-1R ·R (𝑦 ·R 𝑤)) ∈ R) → ((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R)
1711, 15, 16syl2an 595 . . . 4 (((𝑥R𝑧R) ∧ (𝑦R𝑤R)) → ((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R)
1817an4s 656 . . 3 (((𝑥R𝑦R) ∧ (𝑧R𝑤R)) → ((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R)
19 mulclsr 10352 . . . . 5 ((𝑦R𝑧R) → (𝑦 ·R 𝑧) ∈ R)
20 mulclsr 10352 . . . . 5 ((𝑥R𝑤R) → (𝑥 ·R 𝑤) ∈ R)
21 addclsr 10351 . . . . 5 (((𝑦 ·R 𝑧) ∈ R ∧ (𝑥 ·R 𝑤) ∈ R) → ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R)
2219, 20, 21syl2anr 596 . . . 4 (((𝑥R𝑤R) ∧ (𝑦R𝑧R)) → ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R)
2322an42s 657 . . 3 (((𝑥R𝑦R) ∧ (𝑧R𝑤R)) → ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R)
2418, 23jca 512 . 2 (((𝑥R𝑦R) ∧ (𝑧R𝑤R)) → (((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) ∈ R ∧ ((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) ∈ R))
25 mulclsr 10352 . . . . 5 ((𝑥R𝑣R) → (𝑥 ·R 𝑣) ∈ R)
26 mulclsr 10352 . . . . . 6 ((𝑦R𝑢R) → (𝑦 ·R 𝑢) ∈ R)
27 mulclsr 10352 . . . . . 6 ((-1RR ∧ (𝑦 ·R 𝑢) ∈ R) → (-1R ·R (𝑦 ·R 𝑢)) ∈ R)
2812, 26, 27sylancr 587 . . . . 5 ((𝑦R𝑢R) → (-1R ·R (𝑦 ·R 𝑢)) ∈ R)
29 addclsr 10351 . . . . 5 (((𝑥 ·R 𝑣) ∈ R ∧ (-1R ·R (𝑦 ·R 𝑢)) ∈ R) → ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))) ∈ R)
3025, 28, 29syl2an 595 . . . 4 (((𝑥R𝑣R) ∧ (𝑦R𝑢R)) → ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))) ∈ R)
3130an4s 656 . . 3 (((𝑥R𝑦R) ∧ (𝑣R𝑢R)) → ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))) ∈ R)
32 mulclsr 10352 . . . . 5 ((𝑦R𝑣R) → (𝑦 ·R 𝑣) ∈ R)
33 mulclsr 10352 . . . . 5 ((𝑥R𝑢R) → (𝑥 ·R 𝑢) ∈ R)
34 addclsr 10351 . . . . 5 (((𝑦 ·R 𝑣) ∈ R ∧ (𝑥 ·R 𝑢) ∈ R) → ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)) ∈ R)
3532, 33, 34syl2anr 596 . . . 4 (((𝑥R𝑢R) ∧ (𝑦R𝑣R)) → ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)) ∈ R)
3635an42s 657 . . 3 (((𝑥R𝑦R) ∧ (𝑣R𝑢R)) → ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)) ∈ R)
3731, 36jca 512 . 2 (((𝑥R𝑦R) ∧ (𝑣R𝑢R)) → (((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))) ∈ R ∧ ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)) ∈ R))
38 distrsr 10359 . . . 4 (𝑥 ·R (𝑧 +R 𝑣)) = ((𝑥 ·R 𝑧) +R (𝑥 ·R 𝑣))
39 distrsr 10359 . . . . . 6 (𝑦 ·R (𝑤 +R 𝑢)) = ((𝑦 ·R 𝑤) +R (𝑦 ·R 𝑢))
4039oveq2i 7027 . . . . 5 (-1R ·R (𝑦 ·R (𝑤 +R 𝑢))) = (-1R ·R ((𝑦 ·R 𝑤) +R (𝑦 ·R 𝑢)))
41 distrsr 10359 . . . . 5 (-1R ·R ((𝑦 ·R 𝑤) +R (𝑦 ·R 𝑢))) = ((-1R ·R (𝑦 ·R 𝑤)) +R (-1R ·R (𝑦 ·R 𝑢)))
4240, 41eqtri 2819 . . . 4 (-1R ·R (𝑦 ·R (𝑤 +R 𝑢))) = ((-1R ·R (𝑦 ·R 𝑤)) +R (-1R ·R (𝑦 ·R 𝑢)))
4338, 42oveq12i 7028 . . 3 ((𝑥 ·R (𝑧 +R 𝑣)) +R (-1R ·R (𝑦 ·R (𝑤 +R 𝑢)))) = (((𝑥 ·R 𝑧) +R (𝑥 ·R 𝑣)) +R ((-1R ·R (𝑦 ·R 𝑤)) +R (-1R ·R (𝑦 ·R 𝑢))))
44 ovex 7048 . . . 4 (𝑥 ·R 𝑧) ∈ V
45 ovex 7048 . . . 4 (𝑥 ·R 𝑣) ∈ V
46 ovex 7048 . . . 4 (-1R ·R (𝑦 ·R 𝑤)) ∈ V
47 addcomsr 10355 . . . 4 (𝑓 +R 𝑔) = (𝑔 +R 𝑓)
48 addasssr 10356 . . . 4 ((𝑓 +R 𝑔) +R ) = (𝑓 +R (𝑔 +R ))
49 ovex 7048 . . . 4 (-1R ·R (𝑦 ·R 𝑢)) ∈ V
5044, 45, 46, 47, 48, 49caov4 7235 . . 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 2819 . 2 ((𝑥 ·R (𝑧 +R 𝑣)) +R (-1R ·R (𝑦 ·R (𝑤 +R 𝑢)))) = (((𝑥 ·R 𝑧) +R (-1R ·R (𝑦 ·R 𝑤))) +R ((𝑥 ·R 𝑣) +R (-1R ·R (𝑦 ·R 𝑢))))
52 distrsr 10359 . . . 4 (𝑦 ·R (𝑧 +R 𝑣)) = ((𝑦 ·R 𝑧) +R (𝑦 ·R 𝑣))
53 distrsr 10359 . . . 4 (𝑥 ·R (𝑤 +R 𝑢)) = ((𝑥 ·R 𝑤) +R (𝑥 ·R 𝑢))
5452, 53oveq12i 7028 . . 3 ((𝑦 ·R (𝑧 +R 𝑣)) +R (𝑥 ·R (𝑤 +R 𝑢))) = (((𝑦 ·R 𝑧) +R (𝑦 ·R 𝑣)) +R ((𝑥 ·R 𝑤) +R (𝑥 ·R 𝑢)))
55 ovex 7048 . . . 4 (𝑦 ·R 𝑧) ∈ V
56 ovex 7048 . . . 4 (𝑦 ·R 𝑣) ∈ V
57 ovex 7048 . . . 4 (𝑥 ·R 𝑤) ∈ V
58 ovex 7048 . . . 4 (𝑥 ·R 𝑢) ∈ V
5955, 56, 57, 47, 48, 58caov4 7235 . . 3 (((𝑦 ·R 𝑧) +R (𝑦 ·R 𝑣)) +R ((𝑥 ·R 𝑤) +R (𝑥 ·R 𝑢))) = (((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) +R ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)))
6054, 59eqtri 2819 . 2 ((𝑦 ·R (𝑧 +R 𝑣)) +R (𝑥 ·R (𝑤 +R 𝑢))) = (((𝑦 ·R 𝑧) +R (𝑥 ·R 𝑤)) +R ((𝑦 ·R 𝑣) +R (𝑥 ·R 𝑢)))
611, 2, 3, 4, 5, 6, 10, 24, 37, 51, 60ecovdi 8255 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1080   = wceq 1522  wcel 2081   E cep 5352  ccnv 5442  (class class class)co 7016  Rcnr 10133  -1Rcm1r 10136   +R cplr 10137   ·R cmr 10138  cc 10381   + caddc 10386   · cmul 10388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-inf2 8950
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rmo 3113  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-int 4783  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-1o 7953  df-oadd 7957  df-omul 7958  df-er 8139  df-ec 8141  df-qs 8145  df-ni 10140  df-pli 10141  df-mi 10142  df-lti 10143  df-plpq 10176  df-mpq 10177  df-ltpq 10178  df-enq 10179  df-nq 10180  df-erq 10181  df-plq 10182  df-mq 10183  df-1nq 10184  df-rq 10185  df-ltnq 10186  df-np 10249  df-1p 10250  df-plp 10251  df-mp 10252  df-ltp 10253  df-enr 10323  df-nr 10324  df-plr 10325  df-mr 10326  df-m1r 10330  df-c 10389  df-add 10394  df-mul 10395
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator