Theorem xrsinvgval

Description: The inversion operation in 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 an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017)

	Ref	Expression
Assertion	xrsinvgval	|- ( B e. RR* -> ( ( invg ` RR*s ) ` B ) = -e B )

Proof

Step	Hyp	Ref	Expression
1		xrsbas	|- RR* = ( Base ` RR*s )
2		xrsadd	|- +e = ( +g ` RR*s )
3		xrs0	|- 0 = ( 0g ` RR*s )
4		eqid	|- ( invg ` RR*s ) = ( invg ` RR*s )
5	1 2 3 4	grpinvval	|- ( B e. RR* -> ( ( invg ` RR*s ) ` B ) = ( iota_ x e. RR* ( x +e B ) = 0 ) )
6		xnegcl	|- ( B e. RR* -> -e B e. RR* )
7		xaddeq0	|- ( ( x e. RR* /\ B e. RR* ) -> ( ( x +e B ) = 0 <-> x = -e B ) )
8	7	ancoms	|- ( ( B e. RR* /\ x e. RR* ) -> ( ( x +e B ) = 0 <-> x = -e B ) )
9	6 8	riota5	|- ( B e. RR* -> ( iota_ x e. RR* ( x +e B ) = 0 ) = -e B )
10	5 9	eqtrd	|- ( B e. RR* -> ( ( invg ` RR*s ) ` B ) = -e B )