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	⊢ ( 𝐵 ∈ ℝ* → ( ( invg ‘ ℝ*𝑠 ) ‘ 𝐵 ) = -e 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
2		xrsadd	⊢ +e = ( +g ‘ ℝ*𝑠 )
3		xrs0	⊢ 0 = ( 0g ‘ ℝ*𝑠 )
4		eqid	⊢ ( invg ‘ ℝ*𝑠 ) = ( invg ‘ ℝ*𝑠 )
5	1 2 3 4	grpinvval	⊢ ( 𝐵 ∈ ℝ* → ( ( invg ‘ ℝ*𝑠 ) ‘ 𝐵 ) = ( ℩ 𝑥 ∈ ℝ* ( 𝑥 +e 𝐵 ) = 0 ) )
6		xnegcl	⊢ ( 𝐵 ∈ ℝ* → -e 𝐵 ∈ ℝ* )
7		xaddeq0	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝑥 +e 𝐵 ) = 0 ↔ 𝑥 = -e 𝐵 ) )
8	7	ancoms	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( ( 𝑥 +e 𝐵 ) = 0 ↔ 𝑥 = -e 𝐵 ) )
9	6 8	riota5	⊢ ( 𝐵 ∈ ℝ* → ( ℩ 𝑥 ∈ ℝ* ( 𝑥 +e 𝐵 ) = 0 ) = -e 𝐵 )
10	5 9	eqtrd	⊢ ( 𝐵 ∈ ℝ* → ( ( invg ‘ ℝ*𝑠 ) ‘ 𝐵 ) = -e 𝐵 )