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

Metamath Proof Explorer

Theorem xadddi2r

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

		Ref	Expression
	Assertion	xadddi2r	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝐴 +_𝑒 𝐵 ) ·_e 𝐶 ) = ( ( 𝐴 ·_e 𝐶 ) +_𝑒 ( 𝐵 ·_e 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xadddi2	⊢ ( ( 𝐶 ∈ ℝ^* ∧ ( 𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ) ) → ( 𝐶 ·_e ( 𝐴 +_𝑒 𝐵 ) ) = ( ( 𝐶 ·_e 𝐴 ) +_𝑒 ( 𝐶 ·_e 𝐵 ) ) )
2	1	3coml	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ^* ) → ( 𝐶 ·_e ( 𝐴 +_𝑒 𝐵 ) ) = ( ( 𝐶 ·_e 𝐴 ) +_𝑒 ( 𝐶 ·_e 𝐵 ) ) )
3		simp1l	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ^* ) → 𝐴 ∈ ℝ^* )
4		simp2l	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ^* ) → 𝐵 ∈ ℝ^* )
5		xaddcl	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) → ( 𝐴 +_𝑒 𝐵 ) ∈ ℝ^* )
6	3 4 5	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ^* ) → ( 𝐴 +_𝑒 𝐵 ) ∈ ℝ^* )
7		simp3	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ^* ) → 𝐶 ∈ ℝ^* )
8		xmulcom	⊢ ( ( ( 𝐴 +_𝑒 𝐵 ) ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝐴 +_𝑒 𝐵 ) ·_e 𝐶 ) = ( 𝐶 ·_e ( 𝐴 +_𝑒 𝐵 ) ) )
9	6 7 8	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝐴 +_𝑒 𝐵 ) ·_e 𝐶 ) = ( 𝐶 ·_e ( 𝐴 +_𝑒 𝐵 ) ) )
10		xmulcom	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( 𝐴 ·_e 𝐶 ) = ( 𝐶 ·_e 𝐴 ) )
11	3 7 10	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ^* ) → ( 𝐴 ·_e 𝐶 ) = ( 𝐶 ·_e 𝐴 ) )
12		xmulcom	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( 𝐵 ·_e 𝐶 ) = ( 𝐶 ·_e 𝐵 ) )
13	4 7 12	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ^* ) → ( 𝐵 ·_e 𝐶 ) = ( 𝐶 ·_e 𝐵 ) )
14	11 13	oveq12d	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝐴 ·_e 𝐶 ) +_𝑒 ( 𝐵 ·_e 𝐶 ) ) = ( ( 𝐶 ·_e 𝐴 ) +_𝑒 ( 𝐶 ·_e 𝐵 ) ) )
15	2 9 14	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ^* ∧ 0 ≤ 𝐵 ) ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝐴 +_𝑒 𝐵 ) ·_e 𝐶 ) = ( ( 𝐴 ·_e 𝐶 ) +_𝑒 ( 𝐵 ·_e 𝐶 ) ) )