This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )