Theorem xrs10

Description: The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypothesis	xrs1mnd.1	|- R = ( RR*s |`s ( RR* \ { -oo } ) )
Assertion	xrs10	|- 0 = ( 0g ` R )

Proof

Step	Hyp	Ref	Expression
1		xrs1mnd.1	|- R = ( RR*s |`s ( RR* \ { -oo } ) )
2		difss	|- ( RR* \ { -oo } ) C_ RR*
3		xrsbas	|- RR* = ( Base ` RR*s )
4	1 3	ressbas2	|- ( ( RR* \ { -oo } ) C_ RR* -> ( RR* \ { -oo } ) = ( Base ` R ) )
5	2 4	ax-mp	|- ( RR* \ { -oo } ) = ( Base ` R )
6		eqid	|- ( 0g ` R ) = ( 0g ` R )
7		xrex	|- RR* e. _V
8	7	difexi	|- ( RR* \ { -oo } ) e. _V
9		xrsadd	|- +e = ( +g ` RR*s )
10	1 9	ressplusg	|- ( ( RR* \ { -oo } ) e. _V -> +e = ( +g ` R ) )
11	8 10	ax-mp	|- +e = ( +g ` R )
12		0re	|- 0 e. RR
13		rexr	|- ( 0 e. RR -> 0 e. RR* )
14		renemnf	|- ( 0 e. RR -> 0 =/= -oo )
15		eldifsn	|- ( 0 e. ( RR* \ { -oo } ) <-> ( 0 e. RR* /\ 0 =/= -oo ) )
16	13 14 15	sylanbrc	|- ( 0 e. RR -> 0 e. ( RR* \ { -oo } ) )
17	12 16	mp1i	|- ( T. -> 0 e. ( RR* \ { -oo } ) )
18		eldifi	|- ( x e. ( RR* \ { -oo } ) -> x e. RR* )
19	18	adantl	|- ( ( T. /\ x e. ( RR* \ { -oo } ) ) -> x e. RR* )
20		xaddlid	|- ( x e. RR* -> ( 0 +e x ) = x )
21	19 20	syl	|- ( ( T. /\ x e. ( RR* \ { -oo } ) ) -> ( 0 +e x ) = x )
22	19	xaddridd	|- ( ( T. /\ x e. ( RR* \ { -oo } ) ) -> ( x +e 0 ) = x )
23	5 6 11 17 21 22	ismgmid2	|- ( T. -> 0 = ( 0g ` R ) )
24	23	mptru	|- 0 = ( 0g ` R )