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	$⊢ ℝ^{} = {Base}_{ℝ_{𝑠}^{}}$
2	1	a1i	$⊢ ⊤ \to ℝ^{} = {Base}_{ℝ_{𝑠}^{}}$
3		xrsadd	$⊢ +_{𝑒} = +_{ℝ_{𝑠}^{*}}$
4	3	a1i	$⊢ ⊤ \to +_{𝑒} = +_{ℝ_{𝑠}^{*}}$
5		0xr	$⊢ 0 \in ℝ^{*}$
6	5	a1i	$⊢ ⊤ \to 0 \in ℝ^{*}$
7		xaddlid	$⊢ x \in ℝ^{*} \to 0 +_{𝑒} x = x$
8	7	adantl	$⊢ (⊤ \land x \in ℝ^{*}) \to 0 +_{𝑒} x = x$
9		xaddrid	$⊢ x \in ℝ^{*} \to x +_{𝑒} 0 = x$
10	9	adantl	$⊢ (⊤ \land x \in ℝ^{*}) \to x +_{𝑒} 0 = x$
11	2 4 6 8 10	grpidd	$⊢ ⊤ \to 0 = 0_{ℝ_{𝑠}^{*}}$
12	11	mptru	$⊢ 0 = 0_{ℝ_{𝑠}^{*}}$

Metamath Proof Explorer

Theorem xrs0

Proof