Metamath Proof Explorer

Theorem adddir

Description: Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004)

Ref Expression
Assertion adddir ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B ⁢ C = A ⁢ C + B ⁢ C

Proof

Step Hyp Ref Expression
1 adddi ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ → C ⁢ A + B = C ⁢ A + C ⁢ B
2 1 3coml ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ A + B = C ⁢ A + C ⁢ B
3 addcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ
4 mulcom ⊢ A + B ∈ ℂ ∧ C ∈ ℂ → A + B ⁢ C = C ⁢ A + B
5 3 4 stoic3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B ⁢ C = C ⁢ A + B
6 mulcom ⊢ A ∈ ℂ ∧ C ∈ ℂ → A ⁢ C = C ⁢ A
7 6 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ C = C ⁢ A
8 mulcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
9 8 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
10 7 9 oveq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ C + B ⁢ C = C ⁢ A + C ⁢ B
11 2 5 10 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A + B ⁢ C = A ⁢ C + B ⁢ C