Metamath Proof Explorer

Theorem mulslid

Description: Surreal one is a left identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion mulslid 
|- ( A e. No -> ( 1s x.s A ) = A )

Proof

Step Hyp Ref Expression
1 1sno 
 |-  1s e. No
2 mulscom 
 |-  ( ( 1s e. No /\ A e. No ) -> ( 1s x.s A ) = ( A x.s 1s ) )
3 1 2 mpan 
 |-  ( A e. No -> ( 1s x.s A ) = ( A x.s 1s ) )
4 mulsrid 
 |-  ( A e. No -> ( A x.s 1s ) = A )
5 3 4 eqtrd 
 |-  ( A e. No -> ( 1s x.s A ) = A )