Theorem mulnegs1d

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	⊢ ( 𝜑 → 𝐴 ∈ No )
	mulnegs1d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	mulnegs1d	⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) ·s 𝐵 ) = ( -us ‘ ( 𝐴 ·s 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulnegs1d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		mulnegs1d.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3	1	negsidd	⊢ ( 𝜑 → ( 𝐴 +s ( -us ‘ 𝐴 ) ) = 0s )
4	3	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 +s ( -us ‘ 𝐴 ) ) ·s 𝐵 ) = ( 0s ·s 𝐵 ) )
5	1	negscld	⊢ ( 𝜑 → ( -us ‘ 𝐴 ) ∈ No )
6	1 5 2	addsdird	⊢ ( 𝜑 → ( ( 𝐴 +s ( -us ‘ 𝐴 ) ) ·s 𝐵 ) = ( ( 𝐴 ·s 𝐵 ) +s ( ( -us ‘ 𝐴 ) ·s 𝐵 ) ) )
7		muls02	⊢ ( 𝐵 ∈ No → ( 0s ·s 𝐵 ) = 0s )
8	2 7	syl	⊢ ( 𝜑 → ( 0s ·s 𝐵 ) = 0s )
9	4 6 8	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) +s ( ( -us ‘ 𝐴 ) ·s 𝐵 ) ) = 0s )
10	1 2	mulscld	⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) ∈ No )
11	10	negsidd	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) +s ( -us ‘ ( 𝐴 ·s 𝐵 ) ) ) = 0s )
12	9 11	eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) +s ( ( -us ‘ 𝐴 ) ·s 𝐵 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( -us ‘ ( 𝐴 ·s 𝐵 ) ) ) )
13	5 2	mulscld	⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) ·s 𝐵 ) ∈ No )
14	10	negscld	⊢ ( 𝜑 → ( -us ‘ ( 𝐴 ·s 𝐵 ) ) ∈ No )
15	13 14 10	addscan1d	⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝐵 ) +s ( ( -us ‘ 𝐴 ) ·s 𝐵 ) ) = ( ( 𝐴 ·s 𝐵 ) +s ( -us ‘ ( 𝐴 ·s 𝐵 ) ) ) ↔ ( ( -us ‘ 𝐴 ) ·s 𝐵 ) = ( -us ‘ ( 𝐴 ·s 𝐵 ) ) ) )
16	12 15	mpbid	⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) ·s 𝐵 ) = ( -us ‘ ( 𝐴 ·s 𝐵 ) ) )