Theorem xrs0

Description: The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass and df-xrs ), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017)

	Ref	Expression
Assertion	xrs0	|- 0 = ( 0g ` RR*s )

Proof

Step	Hyp	Ref	Expression
1		xrsbas	|- RR* = ( Base ` RR*s )
2	1	a1i	|- ( T. -> RR* = ( Base ` RR*s ) )
3		xrsadd	|- +e = ( +g ` RR*s )
4	3	a1i	|- ( T. -> +e = ( +g ` RR*s ) )
5		0xr	|- 0 e. RR*
6	5	a1i	|- ( T. -> 0 e. RR* )
7		xaddid2	|- ( x e. RR* -> ( 0 +e x ) = x )
8	7	adantl	|- ( ( T. /\ x e. RR* ) -> ( 0 +e x ) = x )
9		xaddid1	|- ( x e. RR* -> ( x +e 0 ) = x )
10	9	adantl	|- ( ( T. /\ x e. RR* ) -> ( x +e 0 ) = x )
11	2 4 6 8 10	grpidd	|- ( T. -> 0 = ( 0g ` RR*s ) )
12	11	mptru	|- 0 = ( 0g ` RR*s )