Theorem mulnegs2d

Description: Product with negative is negative of product. Part of theorem 7 of Conway p. 19. (Contributed by Scott Fenton, 10-Mar-2025)

	Ref	Expression
Hypotheses	mulnegs1d.1	|- ( ph -> A e. No )
	mulnegs1d.2	|- ( ph -> B e. No )
Assertion	mulnegs2d	|- ( ph -> ( A x.s ( -us ` B ) ) = ( -us ` ( A x.s B ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulnegs1d.1	|- ( ph -> A e. No )
2		mulnegs1d.2	|- ( ph -> B e. No )
3	2 1	mulnegs1d	|- ( ph -> ( ( -us ` B ) x.s A ) = ( -us ` ( B x.s A ) ) )
4	2	negscld	|- ( ph -> ( -us ` B ) e. No )
5	1 4	mulscomd	|- ( ph -> ( A x.s ( -us ` B ) ) = ( ( -us ` B ) x.s A ) )
6	1 2	mulscomd	|- ( ph -> ( A x.s B ) = ( B x.s A ) )
7	6	fveq2d	|- ( ph -> ( -us ` ( A x.s B ) ) = ( -us ` ( B x.s A ) ) )
8	3 5 7	3eqtr4d	|- ( ph -> ( A x.s ( -us ` B ) ) = ( -us ` ( A x.s B ) ) )