Theorem remulneg2d

Description: Product with negative is negative of product. (Contributed by SN, 25-Jan-2025)

	Ref	Expression
Hypotheses	remulneg2d.a	|- ( ph -> A e. RR )
	remulneg2d.b	|- ( ph -> B e. RR )
Assertion	remulneg2d	|- ( ph -> ( A x. ( 0 -R B ) ) = ( 0 -R ( A x. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		remulneg2d.a	|- ( ph -> A e. RR )
2		remulneg2d.b	|- ( ph -> B e. RR )
3		0red	|- ( ph -> 0 e. RR )
4		resubdi	|- ( ( A e. RR /\ 0 e. RR /\ B e. RR ) -> ( A x. ( 0 -R B ) ) = ( ( A x. 0 ) -R ( A x. B ) ) )
5	1 3 2 4	syl3anc	|- ( ph -> ( A x. ( 0 -R B ) ) = ( ( A x. 0 ) -R ( A x. B ) ) )
6		remul01	|- ( A e. RR -> ( A x. 0 ) = 0 )
7	1 6	syl	|- ( ph -> ( A x. 0 ) = 0 )
8	7	oveq1d	|- ( ph -> ( ( A x. 0 ) -R ( A x. B ) ) = ( 0 -R ( A x. B ) ) )
9	5 8	eqtrd	|- ( ph -> ( A x. ( 0 -R B ) ) = ( 0 -R ( A x. B ) ) )