Metamath Proof Explorer

Theorem subadds

Description: Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion subadds ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐴 -s 𝐵 ) = 𝐶 ↔ ( 𝐵 +s 𝐶 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 subsval ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 -s 𝐵 ) = ( 𝐴 +s ( -us ‘ 𝐵 ) ) )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 𝐴 -s 𝐵 ) = ( 𝐴 +s ( -us ‘ 𝐵 ) ) )
3 2 eqeq1d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐴 -s 𝐵 ) = 𝐶 ↔ ( 𝐴 +s ( -us ‘ 𝐵 ) ) = 𝐶 ) )
4 simpl ⊢ ( ( 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝐵 ∈ No )
5 simpr ⊢ ( ( 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝐶 ∈ No )
6 negscl ⊢ ( 𝐵 ∈ No → ( -us ‘ 𝐵 ) ∈ No )
7 6 adantr ⊢ ( ( 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( -us ‘ 𝐵 ) ∈ No )
8 4 5 7 adds32d ⊢ ( ( 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐵 +s 𝐶 ) +s ( -us ‘ 𝐵 ) ) = ( ( 𝐵 +s ( -us ‘ 𝐵 ) ) +s 𝐶 ) )
9 negsid ⊢ ( 𝐵 ∈ No → ( 𝐵 +s ( -us ‘ 𝐵 ) ) = 0s )
10 9 adantr ⊢ ( ( 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 𝐵 +s ( -us ‘ 𝐵 ) ) = 0s )
11 10 oveq1d ⊢ ( ( 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐵 +s ( -us ‘ 𝐵 ) ) +s 𝐶 ) = ( 0s +s 𝐶 ) )
12 addslid ⊢ ( 𝐶 ∈ No → ( 0s +s 𝐶 ) = 𝐶 )
13 12 adantl ⊢ ( ( 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 0s +s 𝐶 ) = 𝐶 )
14 8 11 13 3eqtrd ⊢ ( ( 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐵 +s 𝐶 ) +s ( -us ‘ 𝐵 ) ) = 𝐶 )
15 14 3adant1 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐵 +s 𝐶 ) +s ( -us ‘ 𝐵 ) ) = 𝐶 )
16 15 eqeq1d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( ( 𝐵 +s 𝐶 ) +s ( -us ‘ 𝐵 ) ) = ( 𝐴 +s ( -us ‘ 𝐵 ) ) ↔ 𝐶 = ( 𝐴 +s ( -us ‘ 𝐵 ) ) ) )
17 eqcom ⊢ ( 𝐶 = ( 𝐴 +s ( -us ‘ 𝐵 ) ) ↔ ( 𝐴 +s ( -us ‘ 𝐵 ) ) = 𝐶 )
18 16 17 bitrdi ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( ( 𝐵 +s 𝐶 ) +s ( -us ‘ 𝐵 ) ) = ( 𝐴 +s ( -us ‘ 𝐵 ) ) ↔ ( 𝐴 +s ( -us ‘ 𝐵 ) ) = 𝐶 ) )
19 addscl ⊢ ( ( 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 𝐵 +s 𝐶 ) ∈ No )
20 19 3adant1 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( 𝐵 +s 𝐶 ) ∈ No )
21 simp1 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝐴 ∈ No )
22 simp2 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝐵 ∈ No )
23 22 negscld ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( -us ‘ 𝐵 ) ∈ No )
24 20 21 23 addscan2d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( ( 𝐵 +s 𝐶 ) +s ( -us ‘ 𝐵 ) ) = ( 𝐴 +s ( -us ‘ 𝐵 ) ) ↔ ( 𝐵 +s 𝐶 ) = 𝐴 ) )
25 3 18 24 3bitr2d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐴 -s 𝐵 ) = 𝐶 ↔ ( 𝐵 +s 𝐶 ) = 𝐴 ) )