This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )