Metamath Proof Explorer

Theorem no2times

Description: Version of 2times for surreal numbers. (Contributed by Scott Fenton, 23-Jul-2025)

Ref Expression
Assertion no2times 
|- ( A e. No -> ( 2s x.s A ) = ( A +s A ) )

Proof

Step Hyp Ref Expression
1 1p1e2s 
 |-  ( 1s +s 1s ) = 2s
2 1 oveq1i 
 |-  ( ( 1s +s 1s ) x.s A ) = ( 2s x.s A )
3 2 eqcomi 
 |-  ( 2s x.s A ) = ( ( 1s +s 1s ) x.s A )
4 1sno 
 |-  1s e. No
5 4 a1i 
 |-  ( A e. No -> 1s e. No )
6 id 
 |-  ( A e. No -> A e. No )
7 5 5 6 addsdird 
 |-  ( A e. No -> ( ( 1s +s 1s ) x.s A ) = ( ( 1s x.s A ) +s ( 1s x.s A ) ) )
8 mulslid 
 |-  ( A e. No -> ( 1s x.s A ) = A )
9 8 8 oveq12d 
 |-  ( A e. No -> ( ( 1s x.s A ) +s ( 1s x.s A ) ) = ( A +s A ) )
10 7 9 eqtrd 
 |-  ( A e. No -> ( ( 1s +s 1s ) x.s A ) = ( A +s A ) )
11 3 10 eqtrid 
 |-  ( A e. No -> ( 2s x.s A ) = ( A +s A ) )