This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑅 )