Metamath Proof Explorer

Theorem axdistr

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 be used later. Instead, use adddi . (Contributed by NM, 2-Sep-1995) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dfcnqs ⊢ ℂ = ( ( R × R ) / ◡ E )
2 addcnsrec ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ◡ E + [ ⟨ 𝑣 , 𝑢 ⟩ ] ◡ E ) = [ ⟨ ( 𝑧 +R 𝑣 ) , ( 𝑤 +R 𝑢 ) ⟩ ] ◡ E )
3 mulcnsrec ⊢ ( ( ( 𝑥 ∈ 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 ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ E · [ ⟨ 𝑧 , 𝑤 ⟩ ] ◡ E ) = [ ⟨ ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) , ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ⟩ ] ◡ E )
5 mulcnsrec ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ E · [ ⟨ 𝑣 , 𝑢 ⟩ ] ◡ E ) = [ ⟨ ( ( 𝑥 ·R 𝑣 ) +R ( -1R ·R ( 𝑦 ·R 𝑢 ) ) ) , ( ( 𝑦 ·R 𝑣 ) +R ( 𝑥 ·R 𝑢 ) ) ⟩ ] ◡ E )
6 addcnsrec ⊢ ( ( ( ( ( 𝑥 ·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 ⊢ ( ( 𝑧 ∈ R ∧ 𝑣 ∈ R ) → ( 𝑧 +R 𝑣 ) ∈ R )
8 addclsr ⊢ ( ( 𝑤 ∈ R ∧ 𝑢 ∈ R ) → ( 𝑤 +R 𝑢 ) ∈ R )
9 7 8 anim12i ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑣 ∈ R ) ∧ ( 𝑤 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑧 +R 𝑣 ) ∈ R ∧ ( 𝑤 +R 𝑢 ) ∈ R ) )
10 9 an4s ⊢ ( ( ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑧 +R 𝑣 ) ∈ R ∧ ( 𝑤 +R 𝑢 ) ∈ R ) )
11 mulclsr ⊢ ( ( 𝑥 ∈ R ∧ 𝑧 ∈ R ) → ( 𝑥 ·R 𝑧 ) ∈ R )
12 m1r ⊢ -1R ∈ R
13 mulclsr ⊢ ( ( 𝑦 ∈ R ∧ 𝑤 ∈ R ) → ( 𝑦 ·R 𝑤 ) ∈ R )
14 mulclsr ⊢ ( ( -1R ∈ R ∧ ( 𝑦 ·R 𝑤 ) ∈ R ) → ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ∈ R )
15 12 13 14 sylancr ⊢ ( ( 𝑦 ∈ R ∧ 𝑤 ∈ R ) → ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ∈ R )
16 addclsr ⊢ ( ( ( 𝑥 ·R 𝑧 ) ∈ R ∧ ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ∈ R ) → ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ∈ R )
17 11 15 16 syl2an ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑧 ∈ R ) ∧ ( 𝑦 ∈ R ∧ 𝑤 ∈ R ) ) → ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ∈ R )
18 17 an4s ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ) → ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ∈ R )
19 mulclsr ⊢ ( ( 𝑦 ∈ R ∧ 𝑧 ∈ R ) → ( 𝑦 ·R 𝑧 ) ∈ R )
20 mulclsr ⊢ ( ( 𝑥 ∈ R ∧ 𝑤 ∈ R ) → ( 𝑥 ·R 𝑤 ) ∈ R )
21 addclsr ⊢ ( ( ( 𝑦 ·R 𝑧 ) ∈ R ∧ ( 𝑥 ·R 𝑤 ) ∈ R ) → ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ∈ R )
22 19 20 21 syl2anr ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑤 ∈ R ) ∧ ( 𝑦 ∈ R ∧ 𝑧 ∈ R ) ) → ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ∈ R )
23 22 an42s ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ) → ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ∈ R )
24 18 23 jca ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑧 ∈ R ∧ 𝑤 ∈ R ) ) → ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) ∈ R ∧ ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) ∈ R ) )
25 mulclsr ⊢ ( ( 𝑥 ∈ R ∧ 𝑣 ∈ R ) → ( 𝑥 ·R 𝑣 ) ∈ R )
26 mulclsr ⊢ ( ( 𝑦 ∈ R ∧ 𝑢 ∈ R ) → ( 𝑦 ·R 𝑢 ) ∈ R )
27 mulclsr ⊢ ( ( -1R ∈ R ∧ ( 𝑦 ·R 𝑢 ) ∈ R ) → ( -1R ·R ( 𝑦 ·R 𝑢 ) ) ∈ R )
28 12 26 27 sylancr ⊢ ( ( 𝑦 ∈ R ∧ 𝑢 ∈ R ) → ( -1R ·R ( 𝑦 ·R 𝑢 ) ) ∈ R )
29 addclsr ⊢ ( ( ( 𝑥 ·R 𝑣 ) ∈ R ∧ ( -1R ·R ( 𝑦 ·R 𝑢 ) ) ∈ R ) → ( ( 𝑥 ·R 𝑣 ) +R ( -1R ·R ( 𝑦 ·R 𝑢 ) ) ) ∈ R )
30 25 28 29 syl2an ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑣 ∈ R ) ∧ ( 𝑦 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑥 ·R 𝑣 ) +R ( -1R ·R ( 𝑦 ·R 𝑢 ) ) ) ∈ R )
31 30 an4s ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑥 ·R 𝑣 ) +R ( -1R ·R ( 𝑦 ·R 𝑢 ) ) ) ∈ R )
32 mulclsr ⊢ ( ( 𝑦 ∈ R ∧ 𝑣 ∈ R ) → ( 𝑦 ·R 𝑣 ) ∈ R )
33 mulclsr ⊢ ( ( 𝑥 ∈ R ∧ 𝑢 ∈ R ) → ( 𝑥 ·R 𝑢 ) ∈ R )
34 addclsr ⊢ ( ( ( 𝑦 ·R 𝑣 ) ∈ R ∧ ( 𝑥 ·R 𝑢 ) ∈ R ) → ( ( 𝑦 ·R 𝑣 ) +R ( 𝑥 ·R 𝑢 ) ) ∈ R )
35 32 33 34 syl2anr ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑢 ∈ R ) ∧ ( 𝑦 ∈ R ∧ 𝑣 ∈ R ) ) → ( ( 𝑦 ·R 𝑣 ) +R ( 𝑥 ·R 𝑢 ) ) ∈ R )
36 35 an42s ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( 𝑦 ·R 𝑣 ) +R ( 𝑥 ·R 𝑢 ) ) ∈ R )
37 31 36 jca ⊢ ( ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ( 𝑣 ∈ R ∧ 𝑢 ∈ R ) ) → ( ( ( 𝑥 ·R 𝑣 ) +R ( -1R ·R ( 𝑦 ·R 𝑢 ) ) ) ∈ R ∧ ( ( 𝑦 ·R 𝑣 ) +R ( 𝑥 ·R 𝑢 ) ) ∈ R ) )
38 distrsr ⊢ ( 𝑥 ·R ( 𝑧 +R 𝑣 ) ) = ( ( 𝑥 ·R 𝑧 ) +R ( 𝑥 ·R 𝑣 ) )
39 distrsr ⊢ ( 𝑦 ·R ( 𝑤 +R 𝑢 ) ) = ( ( 𝑦 ·R 𝑤 ) +R ( 𝑦 ·R 𝑢 ) )
40 39 oveq2i ⊢ ( -1R ·R ( 𝑦 ·R ( 𝑤 +R 𝑢 ) ) ) = ( -1R ·R ( ( 𝑦 ·R 𝑤 ) +R ( 𝑦 ·R 𝑢 ) ) )
41 distrsr ⊢ ( -1R ·R ( ( 𝑦 ·R 𝑤 ) +R ( 𝑦 ·R 𝑢 ) ) ) = ( ( -1R ·R ( 𝑦 ·R 𝑤 ) ) +R ( -1R ·R ( 𝑦 ·R 𝑢 ) ) )
42 40 41 eqtri ⊢ ( -1R ·R ( 𝑦 ·R ( 𝑤 +R 𝑢 ) ) ) = ( ( -1R ·R ( 𝑦 ·R 𝑤 ) ) +R ( -1R ·R ( 𝑦 ·R 𝑢 ) ) )
43 38 42 oveq12i ⊢ ( ( 𝑥 ·R ( 𝑧 +R 𝑣 ) ) +R ( -1R ·R ( 𝑦 ·R ( 𝑤 +R 𝑢 ) ) ) ) = ( ( ( 𝑥 ·R 𝑧 ) +R ( 𝑥 ·R 𝑣 ) ) +R ( ( -1R ·R ( 𝑦 ·R 𝑤 ) ) +R ( -1R ·R ( 𝑦 ·R 𝑢 ) ) ) )
44 ovex ⊢ ( 𝑥 ·R 𝑧 ) ∈ V
45 ovex ⊢ ( 𝑥 ·R 𝑣 ) ∈ V
46 ovex ⊢ ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ∈ V
47 addcomsr ⊢ ( 𝑓 +R 𝑔 ) = ( 𝑔 +R 𝑓 )
48 addasssr ⊢ ( ( 𝑓 +R 𝑔 ) +R ℎ ) = ( 𝑓 +R ( 𝑔 +R ℎ ) )
49 ovex ⊢ ( -1R ·R ( 𝑦 ·R 𝑢 ) ) ∈ V
50 44 45 46 47 48 49 caov4 ⊢ ( ( ( 𝑥 ·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 ⊢ ( ( 𝑥 ·R ( 𝑧 +R 𝑣 ) ) +R ( -1R ·R ( 𝑦 ·R ( 𝑤 +R 𝑢 ) ) ) ) = ( ( ( 𝑥 ·R 𝑧 ) +R ( -1R ·R ( 𝑦 ·R 𝑤 ) ) ) +R ( ( 𝑥 ·R 𝑣 ) +R ( -1R ·R ( 𝑦 ·R 𝑢 ) ) ) )
52 distrsr ⊢ ( 𝑦 ·R ( 𝑧 +R 𝑣 ) ) = ( ( 𝑦 ·R 𝑧 ) +R ( 𝑦 ·R 𝑣 ) )
53 distrsr ⊢ ( 𝑥 ·R ( 𝑤 +R 𝑢 ) ) = ( ( 𝑥 ·R 𝑤 ) +R ( 𝑥 ·R 𝑢 ) )
54 52 53 oveq12i ⊢ ( ( 𝑦 ·R ( 𝑧 +R 𝑣 ) ) +R ( 𝑥 ·R ( 𝑤 +R 𝑢 ) ) ) = ( ( ( 𝑦 ·R 𝑧 ) +R ( 𝑦 ·R 𝑣 ) ) +R ( ( 𝑥 ·R 𝑤 ) +R ( 𝑥 ·R 𝑢 ) ) )
55 ovex ⊢ ( 𝑦 ·R 𝑧 ) ∈ V
56 ovex ⊢ ( 𝑦 ·R 𝑣 ) ∈ V
57 ovex ⊢ ( 𝑥 ·R 𝑤 ) ∈ V
58 ovex ⊢ ( 𝑥 ·R 𝑢 ) ∈ V
59 55 56 57 47 48 58 caov4 ⊢ ( ( ( 𝑦 ·R 𝑧 ) +R ( 𝑦 ·R 𝑣 ) ) +R ( ( 𝑥 ·R 𝑤 ) +R ( 𝑥 ·R 𝑢 ) ) ) = ( ( ( 𝑦 ·R 𝑧 ) +R ( 𝑥 ·R 𝑤 ) ) +R ( ( 𝑦 ·R 𝑣 ) +R ( 𝑥 ·R 𝑢 ) ) )
60 54 59 eqtri ⊢ ( ( 𝑦 ·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 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )