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