Metamath Proof Explorer

Theorem negsdi

Description: Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025)

Ref Expression
Assertion negsdi ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( -us ‘ ( 𝐴 +s 𝐵 ) ) = ( ( -us ‘ 𝐴 ) +s ( -us ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 addscl ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) ∈ No )
2 1 negsidd ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 +s 𝐵 ) +s ( -us ‘ ( 𝐴 +s 𝐵 ) ) ) = 0s )
3 negsid ⊢ ( 𝐴 ∈ No → ( 𝐴 +s ( -us ‘ 𝐴 ) ) = 0s )
4 negsid ⊢ ( 𝐵 ∈ No → ( 𝐵 +s ( -us ‘ 𝐵 ) ) = 0s )
5 3 4 oveqan12d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 +s ( -us ‘ 𝐴 ) ) +s ( 𝐵 +s ( -us ‘ 𝐵 ) ) ) = ( 0s +s 0s ) )
6 0no ⊢ 0s ∈ No
7 addslid ⊢ ( 0s ∈ No → ( 0s +s 0s ) = 0s )
8 6 7 ax-mp ⊢ ( 0s +s 0s ) = 0s
9 5 8 eqtr2di ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 0s = ( ( 𝐴 +s ( -us ‘ 𝐴 ) ) +s ( 𝐵 +s ( -us ‘ 𝐵 ) ) ) )
10 simpl ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐴 ∈ No )
11 10 negscld ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( -us ‘ 𝐴 ) ∈ No )
12 simpr ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐵 ∈ No )
13 12 negscld ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( -us ‘ 𝐵 ) ∈ No )
14 10 11 12 13 adds4d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 +s ( -us ‘ 𝐴 ) ) +s ( 𝐵 +s ( -us ‘ 𝐵 ) ) ) = ( ( 𝐴 +s 𝐵 ) +s ( ( -us ‘ 𝐴 ) +s ( -us ‘ 𝐵 ) ) ) )
15 2 9 14 3eqtrd ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 +s 𝐵 ) +s ( -us ‘ ( 𝐴 +s 𝐵 ) ) ) = ( ( 𝐴 +s 𝐵 ) +s ( ( -us ‘ 𝐴 ) +s ( -us ‘ 𝐵 ) ) ) )
16 1 negscld ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( -us ‘ ( 𝐴 +s 𝐵 ) ) ∈ No )
17 negscl ⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) ∈ No )
18 negscl ⊢ ( 𝐵 ∈ No → ( -us ‘ 𝐵 ) ∈ No )
19 addscl ⊢ ( ( ( -us ‘ 𝐴 ) ∈ No ∧ ( -us ‘ 𝐵 ) ∈ No ) → ( ( -us ‘ 𝐴 ) +s ( -us ‘ 𝐵 ) ) ∈ No )
20 17 18 19 syl2an ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( -us ‘ 𝐴 ) +s ( -us ‘ 𝐵 ) ) ∈ No )
21 16 20 1 addscan1d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( ( 𝐴 +s 𝐵 ) +s ( -us ‘ ( 𝐴 +s 𝐵 ) ) ) = ( ( 𝐴 +s 𝐵 ) +s ( ( -us ‘ 𝐴 ) +s ( -us ‘ 𝐵 ) ) ) ↔ ( -us ‘ ( 𝐴 +s 𝐵 ) ) = ( ( -us ‘ 𝐴 ) +s ( -us ‘ 𝐵 ) ) ) )
22 15 21 mpbid ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( -us ‘ ( 𝐴 +s 𝐵 ) ) = ( ( -us ‘ 𝐴 ) +s ( -us ‘ 𝐵 ) ) )