Metamath Proof Explorer

Theorem negs0s

Description: Negative surreal zero is surreal zero. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Assertion negs0s 
|- ( -us ` 0s ) = 0s

Proof

Step Hyp Ref Expression
1 right0s 
 |-  ( _R ` 0s ) = (/)
2 1 imaeq2i 
 |-  ( -us " ( _R ` 0s ) ) = ( -us " (/) )
3 ima0 
 |-  ( -us " (/) ) = (/)
4 2 3 eqtri 
 |-  ( -us " ( _R ` 0s ) ) = (/)
5 left0s 
 |-  ( _L ` 0s ) = (/)
6 5 imaeq2i 
 |-  ( -us " ( _L ` 0s ) ) = ( -us " (/) )
7 6 3 eqtri 
 |-  ( -us " ( _L ` 0s ) ) = (/)
8 4 7 oveq12i 
 |-  ( ( -us " ( _R ` 0s ) ) |s ( -us " ( _L ` 0s ) ) ) = ( (/) |s (/) )
9 0sno 
 |-  0s e. No
10 negsval 
 |-  ( 0s e. No -> ( -us ` 0s ) = ( ( -us " ( _R ` 0s ) ) |s ( -us " ( _L ` 0s ) ) ) )
11 9 10 ax-mp 
 |-  ( -us ` 0s ) = ( ( -us " ( _R ` 0s ) ) |s ( -us " ( _L ` 0s ) ) )
12 df-0s 
 |-  0s = ( (/) |s (/) )
13 8 11 12 3eqtr4i 
 |-  ( -us ` 0s ) = 0s