Theorem xrsmgm

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

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

Proof

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