Metamath Proof Explorer


Theorem xadddir

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

Ref Expression
Assertion xadddir ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 xadddi ( ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐶 ·e ( 𝐴 +𝑒 𝐵 ) ) = ( ( 𝐶 ·e 𝐴 ) +𝑒 ( 𝐶 ·e 𝐵 ) ) )
2 1 3coml ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( 𝐶 ·e ( 𝐴 +𝑒 𝐵 ) ) = ( ( 𝐶 ·e 𝐴 ) +𝑒 ( 𝐶 ·e 𝐵 ) ) )
3 xaddcl ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 +𝑒 𝐵 ) ∈ ℝ* )
4 3 3adant3 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( 𝐴 +𝑒 𝐵 ) ∈ ℝ* )
5 rexr ( 𝐶 ∈ ℝ → 𝐶 ∈ ℝ* )
6 5 3ad2ant3 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ* )
7 xmulcom ( ( ( 𝐴 +𝑒 𝐵 ) ∈ ℝ*𝐶 ∈ ℝ* ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( 𝐶 ·e ( 𝐴 +𝑒 𝐵 ) ) )
8 4 6 7 syl2anc ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( 𝐶 ·e ( 𝐴 +𝑒 𝐵 ) ) )
9 simp1 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ* )
10 xmulcom ( ( 𝐴 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐴 ·e 𝐶 ) = ( 𝐶 ·e 𝐴 ) )
11 9 6 10 syl2anc ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( 𝐴 ·e 𝐶 ) = ( 𝐶 ·e 𝐴 ) )
12 simp2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ* )
13 xmulcom ( ( 𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) → ( 𝐵 ·e 𝐶 ) = ( 𝐶 ·e 𝐵 ) )
14 12 6 13 syl2anc ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( 𝐵 ·e 𝐶 ) = ( 𝐶 ·e 𝐵 ) )
15 11 14 oveq12d ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) = ( ( 𝐶 ·e 𝐴 ) +𝑒 ( 𝐶 ·e 𝐵 ) ) )
16 2 8 15 3eqtr4d ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ ) → ( ( 𝐴 +𝑒 𝐵 ) ·e 𝐶 ) = ( ( 𝐴 ·e 𝐶 ) +𝑒 ( 𝐵 ·e 𝐶 ) ) )