Theorem xrs0

Description: The zero of 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 a zero. (Contributed by Thierry Arnoux, 13-Jun-2017)

	Ref	Expression
Assertion	xrs0	$$⊢0=0_{{ℝ}_{𝑠}^{*}}$$

Proof

Step	Hyp	Ref	Expression
1		xrsbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
2	1	a1i	$$⊢\top \to {ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
3		xrsadd	$$⊢{+}_{𝑒}={+}_{{ℝ}_{𝑠}^{*}}$$
4	3	a1i	$$⊢\top \to {+}_{𝑒}={+}_{{ℝ}_{𝑠}^{*}}$$
5		0xr	$$⊢0\in {ℝ}^{*}$$
6	5	a1i	$$⊢\top \to 0\in {ℝ}^{*}$$
7		xaddid2	$$⊢x\in {ℝ}^{*}\to 0{+}_{𝑒}x=x$$
8	7	adantl	$$⊢\left(\top \wedge x\in {ℝ}^{*}\right)\to 0{+}_{𝑒}x=x$$
9		xaddid1	$$⊢x\in {ℝ}^{*}\to x{+}_{𝑒}0=x$$
10	9	adantl	$$⊢\left(\top \wedge x\in {ℝ}^{*}\right)\to x{+}_{𝑒}0=x$$
11	2 4 6 8 10	grpidd	$$⊢\top \to 0=0_{{ℝ}_{𝑠}^{*}}$$
12	11	mptru	$$⊢0=0_{{ℝ}_{𝑠}^{*}}$$