Theorem xrs10

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

	Ref	Expression
Hypothesis	xrs1mnd.1	⊢ 𝑅 = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
Assertion	xrs10	⊢ 0 = ( 0g ‘ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		xrs1mnd.1	⊢ 𝑅 = ( ℝ*𝑠 ↾s ( ℝ* ∖ { -∞ } ) )
2		difss	⊢ ( ℝ* ∖ { -∞ } ) ⊆ ℝ*
3		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
4	1 3	ressbas2	⊢ ( ( ℝ* ∖ { -∞ } ) ⊆ ℝ* → ( ℝ* ∖ { -∞ } ) = ( Base ‘ 𝑅 ) )
5	2 4	ax-mp	⊢ ( ℝ* ∖ { -∞ } ) = ( Base ‘ 𝑅 )
6		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
7		xrex	⊢ ℝ* ∈ V
8	7	difexi	⊢ ( ℝ* ∖ { -∞ } ) ∈ V
9		xrsadd	⊢ +𝑒 = ( +g ‘ ℝ*𝑠 )
10	1 9	ressplusg	⊢ ( ( ℝ* ∖ { -∞ } ) ∈ V → +𝑒 = ( +g ‘ 𝑅 ) )
11	8 10	ax-mp	⊢ +𝑒 = ( +g ‘ 𝑅 )
12		0re	⊢ 0 ∈ ℝ
13		rexr	⊢ ( 0 ∈ ℝ → 0 ∈ ℝ* )
14		renemnf	⊢ ( 0 ∈ ℝ → 0 ≠ -∞ )
15		eldifsn	⊢ ( 0 ∈ ( ℝ* ∖ { -∞ } ) ↔ ( 0 ∈ ℝ* ∧ 0 ≠ -∞ ) )
16	13 14 15	sylanbrc	⊢ ( 0 ∈ ℝ → 0 ∈ ( ℝ* ∖ { -∞ } ) )
17	12 16	mp1i	⊢ ( ⊤ → 0 ∈ ( ℝ* ∖ { -∞ } ) )
18		eldifi	⊢ ( 𝑥 ∈ ( ℝ* ∖ { -∞ } ) → 𝑥 ∈ ℝ* )
19	18	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ) → 𝑥 ∈ ℝ* )
20		xaddlid	⊢ ( 𝑥 ∈ ℝ* → ( 0 +𝑒 𝑥 ) = 𝑥 )
21	19 20	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ) → ( 0 +𝑒 𝑥 ) = 𝑥 )
22	19	xaddridd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( ℝ* ∖ { -∞ } ) ) → ( 𝑥 +𝑒 0 ) = 𝑥 )
23	5 6 11 17 21 22	ismgmid2	⊢ ( ⊤ → 0 = ( 0g ‘ 𝑅 ) )
24	23	mptru	⊢ 0 = ( 0g ‘ 𝑅 )