Theorem mgmplusf

Description: The group addition function of a magma is a function into its base set. (Contributed by Mario Carneiro, 14-Aug-2015) (Revisd by AV, 28-Jan-2020.)

	Ref	Expression
Hypotheses	mgmplusf.1	|- B = ( Base ` M )
	mgmplusf.2	|- .+^ = ( +f ` M )
Assertion	mgmplusf	|- ( M e. Mgm -> .+^ : ( B X. B ) --> B )

Proof

Step	Hyp	Ref	Expression
1		mgmplusf.1	|- B = ( Base ` M )
2		mgmplusf.2	|- .+^ = ( +f ` M )
3		eqid	|- ( +g ` M ) = ( +g ` M )
4	1 3	mgmcl	|- ( ( M e. Mgm /\ x e. B /\ y e. B ) -> ( x ( +g ` M ) y ) e. B )
5	4	3expb	|- ( ( M e. Mgm /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` M ) y ) e. B )
6	5	ralrimivva	|- ( M e. Mgm -> A. x e. B A. y e. B ( x ( +g ` M ) y ) e. B )
7	1 3 2	plusffval	|- .+^ = ( x e. B , y e. B |-> ( x ( +g ` M ) y ) )
8	7	fmpo	|- ( A. x e. B A. y e. B ( x ( +g ` M ) y ) e. B <-> .+^ : ( B X. B ) --> B )
9	6 8	sylib	|- ( M e. Mgm -> .+^ : ( B X. B ) --> B )