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 = ( 0g ‘ ℝ*𝑠 )

Proof

Step	Hyp	Ref	Expression
1		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
2	1	a1i	⊢ ( ⊤ → ℝ* = ( Base ‘ ℝ*𝑠 ) )
3		xrsadd	⊢ +𝑒 = ( +g ‘ ℝ*𝑠 )
4	3	a1i	⊢ ( ⊤ → +𝑒 = ( +g ‘ ℝ*𝑠 ) )
5		0xr	⊢ 0 ∈ ℝ*
6	5	a1i	⊢ ( ⊤ → 0 ∈ ℝ* )
7		xaddid2	⊢ ( 𝑥 ∈ ℝ* → ( 0 +𝑒 𝑥 ) = 𝑥 )
8	7	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ* ) → ( 0 +𝑒 𝑥 ) = 𝑥 )
9		xaddid1	⊢ ( 𝑥 ∈ ℝ* → ( 𝑥 +𝑒 0 ) = 𝑥 )
10	9	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ* ) → ( 𝑥 +𝑒 0 ) = 𝑥 )
11	2 4 6 8 10	grpidd	⊢ ( ⊤ → 0 = ( 0g ‘ ℝ*𝑠 ) )
12	11	mptru	⊢ 0 = ( 0g ‘ ℝ*𝑠 )