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