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={\mathrm{Base}}_M$$
	mgmplusf.2	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(M\right)$$
Assertion	mgmplusf	$$⊢M\in \mathrm{Mgm}\to \underset{\dot{}}{⨣}:B\times B⟶B$$

Proof

Step	Hyp	Ref	Expression
1		mgmplusf.1	$$⊢B={\mathrm{Base}}_M$$
2		mgmplusf.2	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(M\right)$$
3		eqid	$$⊢{+}_M={+}_M$$
4	1 3	mgmcl	$$⊢\left(M\in \mathrm{Mgm}\wedge x\in B\wedge y\in B\right)\to x{+}_{M}y\in B$$
5	4	3expb	$$⊢\left(M\in \mathrm{Mgm}\wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{M}y\in B$$
6	5	ralrimivva	$$⊢M\in \mathrm{Mgm}\to \forall x\in B\forall y\in Bx{+}_{M}y\in B$$
7	1 3 2	plusffval	$$⊢\underset{\dot{}}{⨣}=\left(x\in B,y\in B⟼x{+}_{M}y\right)$$
8	7	fmpo	$$⊢\forall x\in B\forall y\in Bx{+}_{M}y\in B\leftrightarrow \underset{\dot{}}{⨣}:B\times B⟶B$$
9	6 8	sylib	$$⊢M\in \mathrm{Mgm}\to \underset{\dot{}}{⨣}:B\times B⟶B$$