Metamath Proof Explorer

Theorem ltsubsubsbd

Description: Equivalence for the surreal less-than relationship between differences. (Contributed by Scott Fenton, 6-Feb-2025)

Ref Expression
Hypotheses ltsubsubsbd.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
ltsubsubsbd.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
ltsubsubsbd.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
ltsubsubsbd.4 ⊢ ( 𝜑 → 𝐷 ∈ No )
Assertion ltsubsubsbd ( 𝜑 → ( ( 𝐴 -s 𝐶 ) <s ( 𝐵 -s 𝐷 ) ↔ ( 𝐴 -s 𝐵 ) <s ( 𝐶 -s 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 ltsubsubsbd.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 ltsubsubsbd.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
3 ltsubsubsbd.3 ⊢ ( 𝜑 → 𝐶 ∈ No )
4 ltsubsubsbd.4 ⊢ ( 𝜑 → 𝐷 ∈ No )
5 npcans ⊢ ( ( 𝐴 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐴 -s 𝐶 ) +s 𝐶 ) = 𝐴 )
6 1 3 5 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 -s 𝐶 ) +s 𝐶 ) = 𝐴 )
7 npcans ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐴 -s 𝐵 ) +s 𝐵 ) = 𝐴 )
8 1 2 7 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 -s 𝐵 ) +s 𝐵 ) = 𝐴 )
9 6 8 eqtr4d ⊢ ( 𝜑 → ( ( 𝐴 -s 𝐶 ) +s 𝐶 ) = ( ( 𝐴 -s 𝐵 ) +s 𝐵 ) )
10 2 3 addscomd ⊢ ( 𝜑 → ( 𝐵 +s 𝐶 ) = ( 𝐶 +s 𝐵 ) )
11 10 oveq1d ⊢ ( 𝜑 → ( ( 𝐵 +s 𝐶 ) +s ( -us ‘ 𝐷 ) ) = ( ( 𝐶 +s 𝐵 ) +s ( -us ‘ 𝐷 ) ) )
12 2 4 subsvald ⊢ ( 𝜑 → ( 𝐵 -s 𝐷 ) = ( 𝐵 +s ( -us ‘ 𝐷 ) ) )
13 12 oveq1d ⊢ ( 𝜑 → ( ( 𝐵 -s 𝐷 ) +s 𝐶 ) = ( ( 𝐵 +s ( -us ‘ 𝐷 ) ) +s 𝐶 ) )
14 4 negscld ⊢ ( 𝜑 → ( -us ‘ 𝐷 ) ∈ No )
15 2 14 3 adds32d ⊢ ( 𝜑 → ( ( 𝐵 +s ( -us ‘ 𝐷 ) ) +s 𝐶 ) = ( ( 𝐵 +s 𝐶 ) +s ( -us ‘ 𝐷 ) ) )
16 13 15 eqtrd ⊢ ( 𝜑 → ( ( 𝐵 -s 𝐷 ) +s 𝐶 ) = ( ( 𝐵 +s 𝐶 ) +s ( -us ‘ 𝐷 ) ) )
17 3 4 subsvald ⊢ ( 𝜑 → ( 𝐶 -s 𝐷 ) = ( 𝐶 +s ( -us ‘ 𝐷 ) ) )
18 17 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 -s 𝐷 ) +s 𝐵 ) = ( ( 𝐶 +s ( -us ‘ 𝐷 ) ) +s 𝐵 ) )
19 3 14 2 adds32d ⊢ ( 𝜑 → ( ( 𝐶 +s ( -us ‘ 𝐷 ) ) +s 𝐵 ) = ( ( 𝐶 +s 𝐵 ) +s ( -us ‘ 𝐷 ) ) )
20 18 19 eqtrd ⊢ ( 𝜑 → ( ( 𝐶 -s 𝐷 ) +s 𝐵 ) = ( ( 𝐶 +s 𝐵 ) +s ( -us ‘ 𝐷 ) ) )
21 11 16 20 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐵 -s 𝐷 ) +s 𝐶 ) = ( ( 𝐶 -s 𝐷 ) +s 𝐵 ) )
22 9 21 breq12d ⊢ ( 𝜑 → ( ( ( 𝐴 -s 𝐶 ) +s 𝐶 ) <s ( ( 𝐵 -s 𝐷 ) +s 𝐶 ) ↔ ( ( 𝐴 -s 𝐵 ) +s 𝐵 ) <s ( ( 𝐶 -s 𝐷 ) +s 𝐵 ) ) )
23 1 3 subscld ⊢ ( 𝜑 → ( 𝐴 -s 𝐶 ) ∈ No )
24 2 4 subscld ⊢ ( 𝜑 → ( 𝐵 -s 𝐷 ) ∈ No )
25 23 24 3 ltadds1d ⊢ ( 𝜑 → ( ( 𝐴 -s 𝐶 ) <s ( 𝐵 -s 𝐷 ) ↔ ( ( 𝐴 -s 𝐶 ) +s 𝐶 ) <s ( ( 𝐵 -s 𝐷 ) +s 𝐶 ) ) )
26 1 2 subscld ⊢ ( 𝜑 → ( 𝐴 -s 𝐵 ) ∈ No )
27 3 4 subscld ⊢ ( 𝜑 → ( 𝐶 -s 𝐷 ) ∈ No )
28 26 27 2 ltadds1d ⊢ ( 𝜑 → ( ( 𝐴 -s 𝐵 ) <s ( 𝐶 -s 𝐷 ) ↔ ( ( 𝐴 -s 𝐵 ) +s 𝐵 ) <s ( ( 𝐶 -s 𝐷 ) +s 𝐵 ) ) )
29 22 25 28 3bitr4d ⊢ ( 𝜑 → ( ( 𝐴 -s 𝐶 ) <s ( 𝐵 -s 𝐷 ) ↔ ( 𝐴 -s 𝐵 ) <s ( 𝐶 -s 𝐷 ) ) )