Theorem xrsmgm

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

	Ref	Expression
Assertion	xrsmgm	⊢ ℝ*𝑠 ∈ Mgm

Proof

Step	Hyp	Ref	Expression
1		xaddcl	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 +𝑒 𝑦 ) ∈ ℝ* )
2	1	rgen2	⊢ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* ( 𝑥 +𝑒 𝑦 ) ∈ ℝ*
3		0xr	⊢ 0 ∈ ℝ*
4		xrsbas	⊢ ℝ* = ( Base ‘ ℝ*𝑠 )
5		xrsadd	⊢ +𝑒 = ( +g ‘ ℝ*𝑠 )
6	4 5	ismgmn0	⊢ ( 0 ∈ ℝ* → ( ℝ*𝑠 ∈ Mgm ↔ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* ( 𝑥 +𝑒 𝑦 ) ∈ ℝ* ) )
7	3 6	ax-mp	⊢ ( ℝ*𝑠 ∈ Mgm ↔ ∀ 𝑥 ∈ ℝ* ∀ 𝑦 ∈ ℝ* ( 𝑥 +𝑒 𝑦 ) ∈ ℝ* )
8	2 7	mpbir	⊢ ℝ*𝑠 ∈ Mgm