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

Proof

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