Theorem mul2negsd

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

	Ref	Expression
Hypotheses	mulnegs1d.1	$$⊢\phi \to A\in \mathrm{No}$$
	mulnegs1d.2	$$⊢\phi \to B\in \mathrm{No}$$
Assertion	mul2negsd	Could not format assertion : No typesetting found for |- ( ph -> ( ( -us ` A ) x.s ( -us ` B ) ) = ( A x.s B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mulnegs1d.1	$$⊢\phi \to A\in \mathrm{No}$$
2		mulnegs1d.2	$$⊢\phi \to B\in \mathrm{No}$$
3	2	negscld	Could not format ( ph -> ( -us ` B ) e. No ) : No typesetting found for |- ( ph -> ( -us ` B ) e. No ) with typecode |-
4	1 3	mulnegs1d	Could not format ( ph -> ( ( -us ` A ) x.s ( -us ` B ) ) = ( -us ` ( A x.s ( -us ` B ) ) ) ) : No typesetting found for |- ( ph -> ( ( -us ` A ) x.s ( -us ` B ) ) = ( -us ` ( A x.s ( -us ` B ) ) ) ) with typecode |-
5	1 2	mulnegs2d	Could not format ( ph -> ( A x.s ( -us ` B ) ) = ( -us ` ( A x.s B ) ) ) : No typesetting found for |- ( ph -> ( A x.s ( -us ` B ) ) = ( -us ` ( A x.s B ) ) ) with typecode |-
6	5	fveq2d	Could not format ( ph -> ( -us ` ( A x.s ( -us ` B ) ) ) = ( -us ` ( -us ` ( A x.s B ) ) ) ) : No typesetting found for |- ( ph -> ( -us ` ( A x.s ( -us ` B ) ) ) = ( -us ` ( -us ` ( A x.s B ) ) ) ) with typecode |-
7	1 2	mulscld	Could not format ( ph -> ( A x.s B ) e. No ) : No typesetting found for |- ( ph -> ( A x.s B ) e. No ) with typecode |-
8		negnegs	Could not format ( ( A x.s B ) e. No -> ( -us ` ( -us ` ( A x.s B ) ) ) = ( A x.s B ) ) : No typesetting found for |- ( ( A x.s B ) e. No -> ( -us ` ( -us ` ( A x.s B ) ) ) = ( A x.s B ) ) with typecode |-
9	7 8	syl	Could not format ( ph -> ( -us ` ( -us ` ( A x.s B ) ) ) = ( A x.s B ) ) : No typesetting found for |- ( ph -> ( -us ` ( -us ` ( A x.s B ) ) ) = ( A x.s B ) ) with typecode |-
10	4 6 9	3eqtrd	Could not format ( ph -> ( ( -us ` A ) x.s ( -us ` B ) ) = ( A x.s B ) ) : No typesetting found for |- ( ph -> ( ( -us ` A ) x.s ( -us ` B ) ) = ( A x.s B ) ) with typecode |-