xrsmgm

Description: The "additive group" of the extended reals is a magma. (Contributed by AV, 30-Jan-2020)

		Ref	Expression
	Assertion	xrsmgm	$⊢ ℝ_{𝑠}^{*} \in Mgm$

Step	Hyp	Ref	Expression
1		xaddcl	$⊢ (x \in ℝ^{} \land y \in ℝ^{}) \to x +_{𝑒} y \in ℝ^{*}$
2	1	rgen2	$⊢ \forall x \in ℝ^{} \forall y \in ℝ^{} x +_{𝑒} y \in ℝ^{*}$
3		0xr	$⊢ 0 \in ℝ^{*}$
4		xrsbas	$⊢ ℝ^{} = {Base}_{ℝ_{𝑠}^{}}$
5		xrsadd	$⊢ +_{𝑒} = +_{ℝ_{𝑠}^{*}}$
6	4 5	ismgmn0	$⊢ 0 \in ℝ^{} \to (ℝ_{𝑠}^{} \in Mgm \leftrightarrow \forall x \in ℝ^{} \forall y \in ℝ^{} x +_{𝑒} y \in ℝ^{*})$
7	3 6	ax-mp	$⊢ ℝ_{𝑠}^{} \in Mgm \leftrightarrow \forall x \in ℝ^{} \forall y \in ℝ^{} x +_{𝑒} y \in ℝ^{}$
8	2 7	mpbir	$⊢ ℝ_{𝑠}^{*} \in Mgm$

Metamath Proof Explorer