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 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B + C = A ⁢ B + A ⁢ C

Proof

Step Hyp Ref Expression
1 dfcnqs ⊢ ℂ = 𝑹 × 𝑹 / E -1
2 addcnsrec ⊢ z ∈ 𝑹 ∧ w ∈ 𝑹 ∧ v ∈ 𝑹 ∧ u ∈ 𝑹 → z w E -1 + v u E -1 = z + 𝑹 v w + 𝑹 u E -1
3 mulcnsrec ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ z + 𝑹 v ∈ 𝑹 ∧ w + 𝑹 u ∈ 𝑹 → x y E -1 ⁢ z + 𝑹 v w + 𝑹 u E -1 = x ⋅ 𝑹 z + 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 u y ⋅ 𝑹 z + 𝑹 v + 𝑹 x ⋅ 𝑹 w + 𝑹 u E -1
4 mulcnsrec ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ z ∈ 𝑹 ∧ w ∈ 𝑹 → x y E -1 ⁢ z w E -1 = x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w E -1
5 mulcnsrec ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ v ∈ 𝑹 ∧ u ∈ 𝑹 → x y E -1 ⁢ v u E -1 = x ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u y ⋅ 𝑹 v + 𝑹 x ⋅ 𝑹 u E -1
6 addcnsrec ⊢ x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w ∈ 𝑹 ∧ y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w ∈ 𝑹 ∧ x ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u ∈ 𝑹 ∧ y ⋅ 𝑹 v + 𝑹 x ⋅ 𝑹 u ∈ 𝑹 → x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w E -1 + x ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u y ⋅ 𝑹 v + 𝑹 x ⋅ 𝑹 u E -1 = x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 x ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w + 𝑹 y ⋅ 𝑹 v + 𝑹 x ⋅ 𝑹 u E -1
7 addclsr ⊢ z ∈ 𝑹 ∧ v ∈ 𝑹 → z + 𝑹 v ∈ 𝑹
8 addclsr ⊢ w ∈ 𝑹 ∧ u ∈ 𝑹 → w + 𝑹 u ∈ 𝑹
9 7 8 anim12i ⊢ z ∈ 𝑹 ∧ v ∈ 𝑹 ∧ w ∈ 𝑹 ∧ u ∈ 𝑹 → z + 𝑹 v ∈ 𝑹 ∧ w + 𝑹 u ∈ 𝑹
10 9 an4s ⊢ z ∈ 𝑹 ∧ w ∈ 𝑹 ∧ v ∈ 𝑹 ∧ u ∈ 𝑹 → z + 𝑹 v ∈ 𝑹 ∧ w + 𝑹 u ∈ 𝑹
11 mulclsr ⊢ x ∈ 𝑹 ∧ z ∈ 𝑹 → x ⋅ 𝑹 z ∈ 𝑹
12 m1r ⊢ -1 𝑹 ∈ 𝑹
13 mulclsr ⊢ y ∈ 𝑹 ∧ w ∈ 𝑹 → y ⋅ 𝑹 w ∈ 𝑹
14 mulclsr ⊢ -1 𝑹 ∈ 𝑹 ∧ y ⋅ 𝑹 w ∈ 𝑹 → -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w ∈ 𝑹
15 12 13 14 sylancr ⊢ y ∈ 𝑹 ∧ w ∈ 𝑹 → -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w ∈ 𝑹
16 addclsr ⊢ x ⋅ 𝑹 z ∈ 𝑹 ∧ -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w ∈ 𝑹 → x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w ∈ 𝑹
17 11 15 16 syl2an ⊢ x ∈ 𝑹 ∧ z ∈ 𝑹 ∧ y ∈ 𝑹 ∧ w ∈ 𝑹 → x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w ∈ 𝑹
18 17 an4s ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ z ∈ 𝑹 ∧ w ∈ 𝑹 → x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w ∈ 𝑹
19 mulclsr ⊢ y ∈ 𝑹 ∧ z ∈ 𝑹 → y ⋅ 𝑹 z ∈ 𝑹
20 mulclsr ⊢ x ∈ 𝑹 ∧ w ∈ 𝑹 → x ⋅ 𝑹 w ∈ 𝑹
21 addclsr ⊢ y ⋅ 𝑹 z ∈ 𝑹 ∧ x ⋅ 𝑹 w ∈ 𝑹 → y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w ∈ 𝑹
22 19 20 21 syl2anr ⊢ x ∈ 𝑹 ∧ w ∈ 𝑹 ∧ y ∈ 𝑹 ∧ z ∈ 𝑹 → y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w ∈ 𝑹
23 22 an42s ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ z ∈ 𝑹 ∧ w ∈ 𝑹 → y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w ∈ 𝑹
24 18 23 jca ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ z ∈ 𝑹 ∧ w ∈ 𝑹 → x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w ∈ 𝑹 ∧ y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w ∈ 𝑹
25 mulclsr ⊢ x ∈ 𝑹 ∧ v ∈ 𝑹 → x ⋅ 𝑹 v ∈ 𝑹
26 mulclsr ⊢ y ∈ 𝑹 ∧ u ∈ 𝑹 → y ⋅ 𝑹 u ∈ 𝑹
27 mulclsr ⊢ -1 𝑹 ∈ 𝑹 ∧ y ⋅ 𝑹 u ∈ 𝑹 → -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u ∈ 𝑹
28 12 26 27 sylancr ⊢ y ∈ 𝑹 ∧ u ∈ 𝑹 → -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u ∈ 𝑹
29 addclsr ⊢ x ⋅ 𝑹 v ∈ 𝑹 ∧ -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u ∈ 𝑹 → x ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u ∈ 𝑹
30 25 28 29 syl2an ⊢ x ∈ 𝑹 ∧ v ∈ 𝑹 ∧ y ∈ 𝑹 ∧ u ∈ 𝑹 → x ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u ∈ 𝑹
31 30 an4s ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ v ∈ 𝑹 ∧ u ∈ 𝑹 → x ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u ∈ 𝑹
32 mulclsr ⊢ y ∈ 𝑹 ∧ v ∈ 𝑹 → y ⋅ 𝑹 v ∈ 𝑹
33 mulclsr ⊢ x ∈ 𝑹 ∧ u ∈ 𝑹 → x ⋅ 𝑹 u ∈ 𝑹
34 addclsr ⊢ y ⋅ 𝑹 v ∈ 𝑹 ∧ x ⋅ 𝑹 u ∈ 𝑹 → y ⋅ 𝑹 v + 𝑹 x ⋅ 𝑹 u ∈ 𝑹
35 32 33 34 syl2anr ⊢ x ∈ 𝑹 ∧ u ∈ 𝑹 ∧ y ∈ 𝑹 ∧ v ∈ 𝑹 → y ⋅ 𝑹 v + 𝑹 x ⋅ 𝑹 u ∈ 𝑹
36 35 an42s ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ v ∈ 𝑹 ∧ u ∈ 𝑹 → y ⋅ 𝑹 v + 𝑹 x ⋅ 𝑹 u ∈ 𝑹
37 31 36 jca ⊢ x ∈ 𝑹 ∧ y ∈ 𝑹 ∧ v ∈ 𝑹 ∧ u ∈ 𝑹 → x ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u ∈ 𝑹 ∧ y ⋅ 𝑹 v + 𝑹 x ⋅ 𝑹 u ∈ 𝑹
38 distrsr ⊢ x ⋅ 𝑹 z + 𝑹 v = x ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 v
39 distrsr ⊢ y ⋅ 𝑹 w + 𝑹 u = y ⋅ 𝑹 w + 𝑹 y ⋅ 𝑹 u
40 39 oveq2i ⊢ -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 u = -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 y ⋅ 𝑹 u
41 distrsr ⊢ -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 y ⋅ 𝑹 u = -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u
42 40 41 eqtri ⊢ -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 u = -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u
43 38 42 oveq12i ⊢ x ⋅ 𝑹 z + 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 u = x ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u
44 ovex ⊢ x ⋅ 𝑹 z ∈ V
45 ovex ⊢ x ⋅ 𝑹 v ∈ V
46 ovex ⊢ -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w ∈ V
47 addcomsr ⊢ f + 𝑹 g = g + 𝑹 f
48 addasssr ⊢ f + 𝑹 g + 𝑹 h = f + 𝑹 g + 𝑹 h
49 ovex ⊢ -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u ∈ V
50 44 45 46 47 48 49 caov4 ⊢ x ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u = x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 x ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u
51 43 50 eqtri ⊢ x ⋅ 𝑹 z + 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 u = x ⋅ 𝑹 z + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 w + 𝑹 x ⋅ 𝑹 v + 𝑹 -1 𝑹 ⋅ 𝑹 y ⋅ 𝑹 u
52 distrsr ⊢ y ⋅ 𝑹 z + 𝑹 v = y ⋅ 𝑹 z + 𝑹 y ⋅ 𝑹 v
53 distrsr ⊢ x ⋅ 𝑹 w + 𝑹 u = x ⋅ 𝑹 w + 𝑹 x ⋅ 𝑹 u
54 52 53 oveq12i ⊢ y ⋅ 𝑹 z + 𝑹 v + 𝑹 x ⋅ 𝑹 w + 𝑹 u = y ⋅ 𝑹 z + 𝑹 y ⋅ 𝑹 v + 𝑹 x ⋅ 𝑹 w + 𝑹 x ⋅ 𝑹 u
55 ovex ⊢ y ⋅ 𝑹 z ∈ V
56 ovex ⊢ y ⋅ 𝑹 v ∈ V
57 ovex ⊢ x ⋅ 𝑹 w ∈ V
58 ovex ⊢ x ⋅ 𝑹 u ∈ V
59 55 56 57 47 48 58 caov4 ⊢ y ⋅ 𝑹 z + 𝑹 y ⋅ 𝑹 v + 𝑹 x ⋅ 𝑹 w + 𝑹 x ⋅ 𝑹 u = y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w + 𝑹 y ⋅ 𝑹 v + 𝑹 x ⋅ 𝑹 u
60 54 59 eqtri ⊢ y ⋅ 𝑹 z + 𝑹 v + 𝑹 x ⋅ 𝑹 w + 𝑹 u = y ⋅ 𝑹 z + 𝑹 x ⋅ 𝑹 w + 𝑹 y ⋅ 𝑹 v + 𝑹 x ⋅ 𝑹 u
61 1 2 3 4 5 6 10 24 37 51 60 ecovdi ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B + C = A ⁢ B + A ⁢ C