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 𝐶 ) ) )