Metamath Proof Explorer

Theorem addscan2

Description: Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 sleadd1 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A <_s B <-> ( A +s C ) <_s ( B +s C ) ) )
2 sleadd1 
 |-  ( ( B e. No /\ A e. No /\ C e. No ) -> ( B <_s A <-> ( B +s C ) <_s ( A +s C ) ) )
3 2 3com12 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( B <_s A <-> ( B +s C ) <_s ( A +s C ) ) )
4 1 3 anbi12d 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A <_s B /\ B <_s A ) <-> ( ( A +s C ) <_s ( B +s C ) /\ ( B +s C ) <_s ( A +s C ) ) ) )
5 sletri3 
 |-  ( ( A e. No /\ B e. No ) -> ( A = B <-> ( A <_s B /\ B <_s A ) ) )
6 5 3adant3 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A = B <-> ( A <_s B /\ B <_s A ) ) )
7 addscl 
 |-  ( ( A e. No /\ C e. No ) -> ( A +s C ) e. No )
8 7 3adant2 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( A +s C ) e. No )
9 addscl 
 |-  ( ( B e. No /\ C e. No ) -> ( B +s C ) e. No )
10 9 3adant1 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( B +s C ) e. No )
11 sletri3 
 |-  ( ( ( A +s C ) e. No /\ ( B +s C ) e. No ) -> ( ( A +s C ) = ( B +s C ) <-> ( ( A +s C ) <_s ( B +s C ) /\ ( B +s C ) <_s ( A +s C ) ) ) )
12 8 10 11 syl2anc 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A +s C ) = ( B +s C ) <-> ( ( A +s C ) <_s ( B +s C ) /\ ( B +s C ) <_s ( A +s C ) ) ) )
13 4 6 12 3bitr4rd 
 |-  ( ( A e. No /\ B e. No /\ C e. No ) -> ( ( A +s C ) = ( B +s C ) <-> A = B ) )