Metamath Proof Explorer

Theorem addslid

Description: Surreal addition to zero is identity. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Assertion addslid 
|- ( A e. No -> ( 0s +s A ) = A )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. No -> A e. No )
2 0sno 
 |-  0s e. No
3 2 a1i 
 |-  ( A e. No -> 0s e. No )
4 1 3 addscomd 
 |-  ( A e. No -> ( A +s 0s ) = ( 0s +s A ) )
5 addsrid 
 |-  ( A e. No -> ( A +s 0s ) = A )
6 4 5 eqtr3d 
 |-  ( A e. No -> ( 0s +s A ) = A )