Metamath Proof Explorer

Theorem xadddi2r

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

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

Proof

Step Hyp Ref Expression
1 xadddi2 ⊢ C ∈ ℝ * ∧ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B → C ⋅ 𝑒 A + 𝑒 B = C ⋅ 𝑒 A + 𝑒 C ⋅ 𝑒 B
2 1 3coml ⊢ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B ∧ C ∈ ℝ * → C ⋅ 𝑒 A + 𝑒 B = C ⋅ 𝑒 A + 𝑒 C ⋅ 𝑒 B
3 simp1l ⊢ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B ∧ C ∈ ℝ * → A ∈ ℝ *
4 simp2l ⊢ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B ∧ C ∈ ℝ * → B ∈ ℝ *
5 xaddcl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A + 𝑒 B ∈ ℝ *
6 3 4 5 syl2anc ⊢ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B ∧ C ∈ ℝ * → A + 𝑒 B ∈ ℝ *
7 simp3 ⊢ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B ∧ C ∈ ℝ * → C ∈ ℝ *
8 xmulcom ⊢ A + 𝑒 B ∈ ℝ * ∧ C ∈ ℝ * → A + 𝑒 B ⋅ 𝑒 C = C ⋅ 𝑒 A + 𝑒 B
9 6 7 8 syl2anc ⊢ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B ∧ C ∈ ℝ * → A + 𝑒 B ⋅ 𝑒 C = C ⋅ 𝑒 A + 𝑒 B
10 xmulcom ⊢ A ∈ ℝ * ∧ C ∈ ℝ * → A ⋅ 𝑒 C = C ⋅ 𝑒 A
11 3 7 10 syl2anc ⊢ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B ∧ C ∈ ℝ * → A ⋅ 𝑒 C = C ⋅ 𝑒 A
12 xmulcom ⊢ B ∈ ℝ * ∧ C ∈ ℝ * → B ⋅ 𝑒 C = C ⋅ 𝑒 B
13 4 7 12 syl2anc ⊢ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B ∧ C ∈ ℝ * → B ⋅ 𝑒 C = C ⋅ 𝑒 B
14 11 13 oveq12d ⊢ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B ∧ C ∈ ℝ * → A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C = C ⋅ 𝑒 A + 𝑒 C ⋅ 𝑒 B
15 2 9 14 3eqtr4d ⊢ A ∈ ℝ * ∧ 0 ≤ A ∧ B ∈ ℝ * ∧ 0 ≤ B ∧ C ∈ ℝ * → A + 𝑒 B ⋅ 𝑒 C = A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C