Metamath Proof Explorer

Theorem subadds

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

Ref Expression
Assertion subadds 
|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A -s B ) = C <-> ( B +s C ) = A ) )

Proof

Step Hyp Ref Expression
1 subsval 
 |-  ( ( A e. No /\ B e. No ) -> ( A -s B ) = ( A +s ( -us ` B ) ) )
2 1 3adant3 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A -s B ) = ( A +s ( -us ` B ) ) )
3 2 eqeq1d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A -s B ) = C <-> ( A +s ( -us ` B ) ) = C ) )
4 simpl 
 |-  ( ( B e. No /\ C e. No ) -> B e. No )
5 simpr 
 |-  ( ( B e. No /\ C e. No ) -> C e. No )
6 negscl 
 |-  ( B e. No -> ( -us ` B ) e. No )
7 6 adantr 
 |-  ( ( B e. No /\ C e. No ) -> ( -us ` B ) e. No )
8 4 5 7 adds32d 
 |-  ( ( B e. No /\ C e. No ) -> ( ( B +s C ) +s ( -us ` B ) ) = ( ( B +s ( -us ` B ) ) +s C ) )
9 negsid 
 |-  ( B e. No -> ( B +s ( -us ` B ) ) = 0s )
10 9 adantr 
 |-  ( ( B e. No /\ C e. No ) -> ( B +s ( -us ` B ) ) = 0s )
11 10 oveq1d 
 |-  ( ( B e. No /\ C e. No ) -> ( ( B +s ( -us ` B ) ) +s C ) = ( 0s +s C ) )
12 addslid 
 |-  ( C e. No -> ( 0s +s C ) = C )
13 12 adantl 
 |-  ( ( B e. No /\ C e. No ) -> ( 0s +s C ) = C )
14 8 11 13 3eqtrd 
 |-  ( ( B e. No /\ C e. No ) -> ( ( B +s C ) +s ( -us ` B ) ) = C )
15 14 3adant1 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( B +s C ) +s ( -us ` B ) ) = C )
16 15 eqeq1d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( ( B +s C ) +s ( -us ` B ) ) = ( A +s ( -us ` B ) ) <-> C = ( A +s ( -us ` B ) ) ) )
17 eqcom 
 |-  ( C = ( A +s ( -us ` B ) ) <-> ( A +s ( -us ` B ) ) = C )
18 16 17 bitrdi 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( ( B +s C ) +s ( -us ` B ) ) = ( A +s ( -us ` B ) ) <-> ( A +s ( -us ` B ) ) = C ) )
19 addscl 
 |-  ( ( B e. No /\ C e. No ) -> ( B +s C ) e. No )
20 19 3adant1 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( B +s C ) e. No )
21 simp1 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> A e. No )
22 simp2 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> B e. No )
23 22 negscld 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( -us ` B ) e. No )
24 20 21 23 addscan2d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( ( B +s C ) +s ( -us ` B ) ) = ( A +s ( -us ` B ) ) <-> ( B +s C ) = A ) )
25 3 18 24 3bitr2d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A -s B ) = C <-> ( B +s C ) = A ) )