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 ∈ ℝ * → inv g ⁡ ℝ 𝑠 * ⁡ B = − B

Proof

Step Hyp Ref Expression
1 xrsbas ⊢ ℝ * = Base ℝ 𝑠 *
2 xrsadd ⊢ + 𝑒 = + ℝ 𝑠 *
3 xrs0 ⊢ 0 = 0 ℝ 𝑠 *
4 eqid ⊢ inv g ⁡ ℝ 𝑠 * = inv g ⁡ ℝ 𝑠 *
5 1 2 3 4 grpinvval ⊢ B ∈ ℝ * → inv g ⁡ ℝ 𝑠 * ⁡ B = ι x ∈ ℝ * | x + 𝑒 B = 0
6 xnegcl ⊢ B ∈ ℝ * → − B ∈ ℝ *
7 xaddeq0 ⊢ x ∈ ℝ * ∧ B ∈ ℝ * → x + 𝑒 B = 0 ↔ x = − B
8 7 ancoms ⊢ B ∈ ℝ * ∧ x ∈ ℝ * → x + 𝑒 B = 0 ↔ x = − B
9 6 8 riota5 ⊢ B ∈ ℝ * → ι x ∈ ℝ * | x + 𝑒 B = 0 = − B
10 5 9 eqtrd ⊢ B ∈ ℝ * → inv g ⁡ ℝ 𝑠 * ⁡ B = − B