Metamath Proof Explorer


Theorem negs0s

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

Ref Expression
Assertion negs0s Could not format assertion : No typesetting found for |- ( -us ` 0s ) = 0s with typecode |-

Proof

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