Metamath Proof Explorer

Theorem xadddir

Description: Commuted version of xadddi . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xadddir ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ→A+𝑒B⋅𝑒C=A⋅𝑒C+𝑒B⋅𝑒C

Proof

Step Hyp Ref Expression
1 xadddi ⊢C∈ℝ∧A∈ℝ*∧B∈ℝ*→C⋅𝑒A+𝑒B=C⋅𝑒A+𝑒C⋅𝑒B
2 1 3coml ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ→C⋅𝑒A+𝑒B=C⋅𝑒A+𝑒C⋅𝑒B
3 xaddcl ⊢A∈ℝ*∧B∈ℝ*→A+𝑒B∈ℝ*
4 3 3adant3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ→A+𝑒B∈ℝ*
5 rexr ⊢C∈ℝ→C∈ℝ*
6 5 3ad2ant3 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ→C∈ℝ*
7 xmulcom ⊢A+𝑒B∈ℝ*∧C∈ℝ*→A+𝑒B⋅𝑒C=C⋅𝑒A+𝑒B
8 4 6 7 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ→A+𝑒B⋅𝑒C=C⋅𝑒A+𝑒B
9 simp1 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ→A∈ℝ*
10 xmulcom ⊢A∈ℝ*∧C∈ℝ*→A⋅𝑒C=C⋅𝑒A
11 9 6 10 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ→A⋅𝑒C=C⋅𝑒A
12 simp2 ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ→B∈ℝ*
13 xmulcom ⊢B∈ℝ*∧C∈ℝ*→B⋅𝑒C=C⋅𝑒B
14 12 6 13 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ→B⋅𝑒C=C⋅𝑒B
15 11 14 oveq12d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ→A⋅𝑒C+𝑒B⋅𝑒C=C⋅𝑒A+𝑒C⋅𝑒B
16 2 8 15 3eqtr4d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ→A+𝑒B⋅𝑒C=A⋅𝑒C+𝑒B⋅𝑒C