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\in {ℝ}^{*}\to {inv}_g\left({ℝ}_{𝑠}^{*}\right)\left(B\right)=-B$$

Proof

Step	Hyp	Ref	Expression
1		xrsbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
2		xrsadd	$$⊢{+}_{𝑒}={+}_{{ℝ}_{𝑠}^{*}}$$
3		xrs0	$$⊢0=0_{{ℝ}_{𝑠}^{*}}$$
4		eqid	$$⊢{inv}_g\left({ℝ}_{𝑠}^{*}\right)={inv}_g\left({ℝ}_{𝑠}^{*}\right)$$
5	1 2 3 4	grpinvval	$$⊢B\in {ℝ}^{*}\to {inv}_g\left({ℝ}_{𝑠}^{*}\right)\left(B\right)=\left(\iota x\in {ℝ}^{*}|x{+}_{𝑒}B=0\right)$$
6		xnegcl	$$⊢B\in {ℝ}^{*}\to -B\in {ℝ}^{*}$$
7		xaddeq0	$$⊢\left(x\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(x{+}_{𝑒}B=0\leftrightarrow x=-B\right)$$
8	7	ancoms	$$⊢\left(B\in {ℝ}^{*}\wedge x\in {ℝ}^{*}\right)\to \left(x{+}_{𝑒}B=0\leftrightarrow x=-B\right)$$
9	6 8	riota5	$$⊢B\in {ℝ}^{*}\to \left(\iota x\in {ℝ}^{*}|x{+}_{𝑒}B=0\right)=-B$$
10	5 9	eqtrd	$$⊢B\in {ℝ}^{*}\to {inv}_g\left({ℝ}_{𝑠}^{*}\right)\left(B\right)=-B$$