This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐶 ·e ( 𝐴 +𝑒 𝐵 ) ) = ( ( 𝐶 ·e 𝐴 ) +𝑒 ( 𝐶 ·e 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 xrge0adddir ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) )
2 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
3 simp1 ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐴 ∈ ( 0 [,] +∞ ) )
4 2 3 sselid ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐴 ∈ ℝ* )
5 simp2 ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐵 ∈ ( 0 [,] +∞ ) )
6 2 5 sselid ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐵 ∈ ℝ* )
7 4 6 xaddcld ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐴 +𝑒 𝐵 ) ∈ ℝ* )
8 simp3 ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
9 2 8 sselid ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → 𝐶 ∈ ℝ* )
10 xmulcom ⊢ ( ( ( 𝐴 +𝑒 𝐵 ) ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( 𝐶 ·e ( 𝐴 +𝑒 𝐵 ) ) )
11 7 9 10 syl2anc ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( 𝐶 ·e ( 𝐴 +𝑒 𝐵 ) ) )
12 xmulcom ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐴 ·e 𝐶 ) = ( 𝐶 ·e 𝐴 ) )
13 4 9 12 syl2anc ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐴 ·e 𝐶 ) = ( 𝐶 ·e 𝐴 ) )
14 xmulcom ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐵 ·e 𝐶 ) = ( 𝐶 ·e 𝐵 ) )
15 6 9 14 syl2anc ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐵 ·e 𝐶 ) = ( 𝐶 ·e 𝐵 ) )
16 13 15 oveq12d ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) = ( ( 𝐶 ·e 𝐴 ) +𝑒 ( 𝐶 ·e 𝐵 ) ) )
17 1 11 16 3eqtr3d ⊢ ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ∧ 𝐶 ∈ ( 0 [,] +∞ ) ) → ( 𝐶 ·e ( 𝐴 +𝑒 𝐵 ) ) = ( ( 𝐶 ·e 𝐴 ) +𝑒 ( 𝐶 ·e 𝐵 ) ) )