Theorem xrs10

Description: The zero of the extended real number monoid. (Contributed by Mario Carneiro, 21-Aug-2015)

	Ref	Expression
Hypothesis	xrs1mnd.1	$$⊢R={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)$$
Assertion	xrs10	$$⊢0=0_R$$

Proof

Step	Hyp	Ref	Expression
1		xrs1mnd.1	$$⊢R={ℝ}_{𝑠}^{*}{\upharpoonright }_{𝑠}\left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)$$
2		difss	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}$$
3		xrsbas	$$⊢{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$$
4	1 3	ressbas2	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\subseteq {ℝ}^{*}\to {ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}={\mathrm{Base}}_R$$
5	2 4	ax-mp	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}={\mathrm{Base}}_R$$
6		eqid	$$⊢0_R=0_R$$
7		xrex	$$⊢{ℝ}^{*}\in \mathrm{V}$$
8	7	difexi	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\in \mathrm{V}$$
9		xrsadd	$$⊢{+}_{𝑒}={+}_{{ℝ}_{𝑠}^{*}}$$
10	1 9	ressplusg	$$⊢{ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\in \mathrm{V}\to {+}_{𝑒}={+}_R$$
11	8 10	ax-mp	$$⊢{+}_{𝑒}={+}_R$$
12		0re	$$⊢0\in ℝ$$
13		rexr	$$⊢0\in ℝ\to 0\in {ℝ}^{*}$$
14		renemnf	$$⊢0\in ℝ\to 0\ne \mathrm{-\infty }$$
15		eldifsn	$$⊢0\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\leftrightarrow \left(0\in {ℝ}^{*}\wedge 0\ne \mathrm{-\infty }\right)$$
16	13 14 15	sylanbrc	$$⊢0\in ℝ\to 0\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)$$
17	12 16	mp1i	$$⊢\top \to 0\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)$$
18		eldifi	$$⊢x\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\to x\in {ℝ}^{*}$$
19	18	adantl	$$⊢\left(\top \wedge x\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)\to x\in {ℝ}^{*}$$
20		xaddid2	$$⊢x\in {ℝ}^{*}\to 0{+}_{𝑒}x=x$$
21	19 20	syl	$$⊢\left(\top \wedge x\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)\to 0{+}_{𝑒}x=x$$
22	19	xaddid1d	$$⊢\left(\top \wedge x\in \left({ℝ}^{*}\setminus \left\{\mathrm{-\infty }\right\}\right)\right)\to x{+}_{𝑒}0=x$$
23	5 6 11 17 21 22	ismgmid2	$$⊢\top \to 0=0_R$$
24	23	mptru	$$⊢0=0_R$$