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