Theorem xrsmgm

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

	Ref	Expression
Assertion	xrsmgm	|- RR*s e. Mgm

Proof

Step	Hyp	Ref	Expression
1		xaddcl	|- ( ( x e. RR* /\ y e. RR* ) -> ( x +e y ) e. RR* )
2	1	rgen2	|- A. x e. RR* A. y e. RR* ( x +e y ) e. RR*
3		0xr	|- 0 e. RR*
4		xrsbas	|- RR* = ( Base ` RR*s )
5		xrsadd	|- +e = ( +g ` RR*s )
6	4 5	ismgmn0	|- ( 0 e. RR* -> ( RR*s e. Mgm <-> A. x e. RR* A. y e. RR* ( x +e y ) e. RR* ) )
7	3 6	ax-mp	|- ( RR*s e. Mgm <-> A. x e. RR* A. y e. RR* ( x +e y ) e. RR* )
8	2 7	mpbir	|- RR*s e. Mgm