Theorem mul2negsd

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

	Ref	Expression
Hypotheses	mulnegs1d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	mulnegs1d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	mul2negsd	⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) ·s ( -us ‘ 𝐵 ) ) = ( 𝐴 ·s 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		mulnegs1d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		mulnegs1d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3	2	negscld	⊢ ( 𝜑 → ( -us ‘ 𝐵 ) ∈ No )
4	1 3	mulnegs1d	⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) ·s ( -us ‘ 𝐵 ) ) = ( -us ‘ ( 𝐴 ·s ( -us ‘ 𝐵 ) ) ) )
5	1 2	mulnegs2d	⊢ ( 𝜑 → ( 𝐴 ·s ( -us ‘ 𝐵 ) ) = ( -us ‘ ( 𝐴 ·s 𝐵 ) ) )
6	5	fveq2d	⊢ ( 𝜑 → ( -us ‘ ( 𝐴 ·s ( -us ‘ 𝐵 ) ) ) = ( -us ‘ ( -us ‘ ( 𝐴 ·s 𝐵 ) ) ) )
7	1 2	mulscld	⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) ∈ No )
8		negnegs	⊢ ( ( 𝐴 ·s 𝐵 ) ∈ No → ( -us ‘ ( -us ‘ ( 𝐴 ·s 𝐵 ) ) ) = ( 𝐴 ·s 𝐵 ) )
9	7 8	syl	⊢ ( 𝜑 → ( -us ‘ ( -us ‘ ( 𝐴 ·s 𝐵 ) ) ) = ( 𝐴 ·s 𝐵 ) )
10	4 6 9	3eqtrd	⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) ·s ( -us ‘ 𝐵 ) ) = ( 𝐴 ·s 𝐵 ) )