Metamath Proof Explorer


Axiom ax-distr

Description: Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, justified by Theorem axdistr . Proofs should normally use adddi instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994)

Ref Expression
Assertion ax-distr ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 cc
2 0 1 wcel 𝐴 ∈ ℂ
3 cB 𝐵
4 3 1 wcel 𝐵 ∈ ℂ
5 cC 𝐶
6 5 1 wcel 𝐶 ∈ ℂ
7 2 4 6 w3a ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ )
8 cmul ·
9 caddc +
10 3 5 9 co ( 𝐵 + 𝐶 )
11 0 10 8 co ( 𝐴 · ( 𝐵 + 𝐶 ) )
12 0 3 8 co ( 𝐴 · 𝐵 )
13 0 5 8 co ( 𝐴 · 𝐶 )
14 12 13 9 co ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) )
15 11 14 wceq ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) )
16 7 15 wi ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐶 ) ) )