Theorem subsdid

Description: Distribution of surreal multiplication over subtraction. (Contributed by Scott Fenton, 9-Mar-2025)

	Ref	Expression
Hypotheses	addsdid.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	addsdid.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	addsdid.3	⊢ ( 𝜑 → 𝐶 ∈ No )
Assertion	subsdid	⊢ ( 𝜑 → ( 𝐴 ·s ( 𝐵 -s 𝐶 ) ) = ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		addsdid.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		addsdid.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		addsdid.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4	2 3	subscld	⊢ ( 𝜑 → ( 𝐵 -s 𝐶 ) ∈ No )
5	1 3 4	addsdid	⊢ ( 𝜑 → ( 𝐴 ·s ( 𝐶 +s ( 𝐵 -s 𝐶 ) ) ) = ( ( 𝐴 ·s 𝐶 ) +s ( 𝐴 ·s ( 𝐵 -s 𝐶 ) ) ) )
6		pncan3s	⊢ ( ( 𝐶 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐶 +s ( 𝐵 -s 𝐶 ) ) = 𝐵 )
7	3 2 6	syl2anc	⊢ ( 𝜑 → ( 𝐶 +s ( 𝐵 -s 𝐶 ) ) = 𝐵 )
8	7	oveq2d	⊢ ( 𝜑 → ( 𝐴 ·s ( 𝐶 +s ( 𝐵 -s 𝐶 ) ) ) = ( 𝐴 ·s 𝐵 ) )
9	5 8	eqtr3d	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐶 ) +s ( 𝐴 ·s ( 𝐵 -s 𝐶 ) ) ) = ( 𝐴 ·s 𝐵 ) )
10	1 2	mulscld	⊢ ( 𝜑 → ( 𝐴 ·s 𝐵 ) ∈ No )
11	1 3	mulscld	⊢ ( 𝜑 → ( 𝐴 ·s 𝐶 ) ∈ No )
12	1 4	mulscld	⊢ ( 𝜑 → ( 𝐴 ·s ( 𝐵 -s 𝐶 ) ) ∈ No )
13	10 11 12	subaddsd	⊢ ( 𝜑 → ( ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 𝐶 ) ) = ( 𝐴 ·s ( 𝐵 -s 𝐶 ) ) ↔ ( ( 𝐴 ·s 𝐶 ) +s ( 𝐴 ·s ( 𝐵 -s 𝐶 ) ) ) = ( 𝐴 ·s 𝐵 ) ) )
14	9 13	mpbird	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 𝐶 ) ) = ( 𝐴 ·s ( 𝐵 -s 𝐶 ) ) )
15	14	eqcomd	⊢ ( 𝜑 → ( 𝐴 ·s ( 𝐵 -s 𝐶 ) ) = ( ( 𝐴 ·s 𝐵 ) -s ( 𝐴 ·s 𝐶 ) ) )