Metamath Proof Explorer

Theorem xrge0adddi

Description: Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018)

Ref Expression
Assertion xrge0adddi ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → C ⋅ 𝑒 A + 𝑒 B = C ⋅ 𝑒 A + 𝑒 C ⋅ 𝑒 B

Proof

Step Hyp Ref Expression
1 xrge0adddir ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → A + 𝑒 B ⋅ 𝑒 C = A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C
2 iccssxr ⊢ 0 +∞ ⊆ ℝ *
3 simp1 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → A ∈ 0 +∞
4 2 3 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → A ∈ ℝ *
5 simp2 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → B ∈ 0 +∞
6 2 5 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → B ∈ ℝ *
7 4 6 xaddcld ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → A + 𝑒 B ∈ ℝ *
8 simp3 ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → C ∈ 0 +∞
9 2 8 sselid ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → C ∈ ℝ *
10 xmulcom ⊢ A + 𝑒 B ∈ ℝ * ∧ C ∈ ℝ * → A + 𝑒 B ⋅ 𝑒 C = C ⋅ 𝑒 A + 𝑒 B
11 7 9 10 syl2anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → A + 𝑒 B ⋅ 𝑒 C = C ⋅ 𝑒 A + 𝑒 B
12 xmulcom ⊢ A ∈ ℝ * ∧ C ∈ ℝ * → A ⋅ 𝑒 C = C ⋅ 𝑒 A
13 4 9 12 syl2anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → A ⋅ 𝑒 C = C ⋅ 𝑒 A
14 xmulcom ⊢ B ∈ ℝ * ∧ C ∈ ℝ * → B ⋅ 𝑒 C = C ⋅ 𝑒 B
15 6 9 14 syl2anc ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → B ⋅ 𝑒 C = C ⋅ 𝑒 B
16 13 15 oveq12d ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → A ⋅ 𝑒 C + 𝑒 B ⋅ 𝑒 C = C ⋅ 𝑒 A + 𝑒 C ⋅ 𝑒 B
17 1 11 16 3eqtr3d ⊢ A ∈ 0 +∞ ∧ B ∈ 0 +∞ ∧ C ∈ 0 +∞ → C ⋅ 𝑒 A + 𝑒 B = C ⋅ 𝑒 A + 𝑒 C ⋅ 𝑒 B