Theorem divsdird

Description: Distribution of surreal division over addition. (Contributed by Scott Fenton, 13-Aug-2025)

	Ref	Expression
Hypotheses	divsdird.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	divsdird.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	divsdird.3	⊢ ( 𝜑 → 𝐶 ∈ No )
	divsdird.4	⊢ ( 𝜑 → 𝐶 ≠ 0s )
Assertion	divsdird	⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) /su 𝐶 ) = ( ( 𝐴 /su 𝐶 ) +s ( 𝐵 /su 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		divsdird.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		divsdird.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		divsdird.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4		divsdird.4	⊢ ( 𝜑 → 𝐶 ≠ 0s )
5		1no	⊢ 1s ∈ No
6	5	a1i	⊢ ( 𝜑 → 1s ∈ No )
7	6 3 4	divscld	⊢ ( 𝜑 → ( 1s /su 𝐶 ) ∈ No )
8	1 2 7	addsdird	⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) ·s ( 1s /su 𝐶 ) ) = ( ( 𝐴 ·s ( 1s /su 𝐶 ) ) +s ( 𝐵 ·s ( 1s /su 𝐶 ) ) ) )
9	1 2	addscld	⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) ∈ No )
10	9 3 4	divsrecd	⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) /su 𝐶 ) = ( ( 𝐴 +s 𝐵 ) ·s ( 1s /su 𝐶 ) ) )
11	1 3 4	divsrecd	⊢ ( 𝜑 → ( 𝐴 /su 𝐶 ) = ( 𝐴 ·s ( 1s /su 𝐶 ) ) )
12	2 3 4	divsrecd	⊢ ( 𝜑 → ( 𝐵 /su 𝐶 ) = ( 𝐵 ·s ( 1s /su 𝐶 ) ) )
13	11 12	oveq12d	⊢ ( 𝜑 → ( ( 𝐴 /su 𝐶 ) +s ( 𝐵 /su 𝐶 ) ) = ( ( 𝐴 ·s ( 1s /su 𝐶 ) ) +s ( 𝐵 ·s ( 1s /su 𝐶 ) ) ) )
14	8 10 13	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 +s 𝐵 ) /su 𝐶 ) = ( ( 𝐴 /su 𝐶 ) +s ( 𝐵 /su 𝐶 ) ) )