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 ˙ = + 𝑓 M
Assertion mgmplusf M Mgm ˙ : B × B B

Proof

Step Hyp Ref Expression
1 mgmplusf.1 B = Base M
2 mgmplusf.2 ˙ = + 𝑓 M
3 eqid + M = + M
4 1 3 mgmcl M Mgm x B y B x + M y B
5 4 3expb M Mgm x B y B x + M y B
6 5 ralrimivva M Mgm x B y B x + M y B
7 1 3 2 plusffval ˙ = x B , y B x + M y
8 7 fmpo x B y B x + M y B ˙ : B × B B
9 6 8 sylib M Mgm ˙ : B × B B