Theorem mul2negsd

Description: Surreal product of two negatives. (Contributed by Scott Fenton, 15-Mar-2025)

	Ref	Expression
Hypotheses	mulnegs1d.1	|- ( ph -> A e. No )
	mulnegs1d.2	|- ( ph -> B e. No )
Assertion	mul2negsd	|- ( ph -> ( ( -us ` A ) x.s ( -us ` B ) ) = ( 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	negscld	|- ( ph -> ( -us ` B ) e. No )
4	1 3	mulnegs1d	|- ( ph -> ( ( -us ` A ) x.s ( -us ` B ) ) = ( -us ` ( A x.s ( -us ` B ) ) ) )
5	1 2	mulnegs2d	|- ( ph -> ( A x.s ( -us ` B ) ) = ( -us ` ( A x.s B ) ) )
6	5	fveq2d	|- ( ph -> ( -us ` ( A x.s ( -us ` B ) ) ) = ( -us ` ( -us ` ( A x.s B ) ) ) )
7	1 2	mulscld	|- ( ph -> ( A x.s B ) e. No )
8		negnegs	|- ( ( A x.s B ) e. No -> ( -us ` ( -us ` ( A x.s B ) ) ) = ( A x.s B ) )
9	7 8	syl	|- ( ph -> ( -us ` ( -us ` ( A x.s B ) ) ) = ( A x.s B ) )
10	4 6 9	3eqtrd	|- ( ph -> ( ( -us ` A ) x.s ( -us ` B ) ) = ( A x.s B ) )