Theorem xmulneg2

Description: Extended real version of mulneg2 . (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xmulneg2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ·e -𝑒 𝐵 ) = -𝑒 ( 𝐴 ·e 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		xmulneg1	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( -𝑒 𝐵 ·e 𝐴 ) = -𝑒 ( 𝐵 ·e 𝐴 ) )
2	1	ancoms	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( -𝑒 𝐵 ·e 𝐴 ) = -𝑒 ( 𝐵 ·e 𝐴 ) )
3		xnegcl	⊢ ( 𝐵 ∈ ℝ* → -𝑒 𝐵 ∈ ℝ* )
4		xmulcom	⊢ ( ( 𝐴 ∈ ℝ* ∧ -𝑒 𝐵 ∈ ℝ* ) → ( 𝐴 ·e -𝑒 𝐵 ) = ( -𝑒 𝐵 ·e 𝐴 ) )
5	3 4	sylan2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ·e -𝑒 𝐵 ) = ( -𝑒 𝐵 ·e 𝐴 ) )
6		xmulcom	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ·e 𝐵 ) = ( 𝐵 ·e 𝐴 ) )
7		xnegeq	⊢ ( ( 𝐴 ·e 𝐵 ) = ( 𝐵 ·e 𝐴 ) → -𝑒 ( 𝐴 ·e 𝐵 ) = -𝑒 ( 𝐵 ·e 𝐴 ) )
8	6 7	syl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → -𝑒 ( 𝐴 ·e 𝐵 ) = -𝑒 ( 𝐵 ·e 𝐴 ) )
9	2 5 8	3eqtr4d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ·e -𝑒 𝐵 ) = -𝑒 ( 𝐴 ·e 𝐵 ) )