Metamath Proof Explorer

Theorem xrsstr

Description: The extended real structure is a structure. (Contributed by Mario Carneiro, 21-Aug-2015)

		Ref	Expression
	Assertion	xrsstr	\|- RR*s Struct <. 1 , ; 1 2 >.

Proof

Step	Hyp	Ref	Expression
1		df-xrs	\|- RRs = ( { <. ( Base ` ndx ) , RR >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , e >. } u. { <. ( TopSet ` ndx ) , ( ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR , y e. RR* \|-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. } )
2	1	odrngstr	\|- RR*s Struct <. 1 , ; 1 2 >.

Step

Hyp

Ref

Expression

df-xrs

 |-  RR*s = ( { <. ( Base ` ndx ) , RR* >. , <. ( +g ` ndx ) , +e >. , <. ( .r ` ndx ) , *e >. } u. { <. ( TopSet ` ndx ) , ( ordTop ` <_ ) >. , <. ( le ` ndx ) , <_ >. , <. ( dist ` ndx ) , ( x e. RR* , y e. RR* |-> if ( x <_ y , ( y +e -e x ) , ( x +e -e y ) ) ) >. } )

odrngstr

 |-  RR*s Struct <. 1 , ; 1 2 >.