Theorem mgmplusfreseq

Description: If the empty set is not contained in the base set of a magma, the restriction of the addition operation to (the Cartesian square of) the base set is the functionalization of it. (Contributed by AV, 28-Jan-2020)

	Ref	Expression
Hypotheses	plusfreseq.1	$$⊢B={\mathrm{Base}}_M$$
	plusfreseq.2	$$⊢\underset{\dot{}}{+}={+}_M$$
	plusfreseq.3	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(M\right)$$
Assertion	mgmplusfreseq	$$⊢\left(M\in \mathrm{Mgm}\wedge \varnothing \notin B\right)\to {\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}=\underset{\dot{}}{⨣}$$

Proof

Step	Hyp	Ref	Expression
1		plusfreseq.1	$$⊢B={\mathrm{Base}}_M$$
2		plusfreseq.2	$$⊢\underset{\dot{}}{+}={+}_M$$
3		plusfreseq.3	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(M\right)$$
4	1 3	mgmplusf	$$⊢M\in \mathrm{Mgm}\to \underset{\dot{}}{⨣}:B\times B⟶B$$
5		frn	$$⊢\underset{\dot{}}{⨣}:B\times B⟶B\to \mathrm{ran}\underset{\dot{}}{⨣}\subseteq B$$
6		ssel	$$⊢\mathrm{ran}\underset{\dot{}}{⨣}\subseteq B\to \left(\varnothing \in \mathrm{ran}\underset{\dot{}}{⨣}\to \varnothing \in B\right)$$
7	6	nelcon3d	$$⊢\mathrm{ran}\underset{\dot{}}{⨣}\subseteq B\to \left(\varnothing \notin B\to \varnothing \notin \mathrm{ran}\underset{\dot{}}{⨣}\right)$$
8	4 5 7	3syl	$$⊢M\in \mathrm{Mgm}\to \left(\varnothing \notin B\to \varnothing \notin \mathrm{ran}\underset{\dot{}}{⨣}\right)$$
9	8	imp	$$⊢\left(M\in \mathrm{Mgm}\wedge \varnothing \notin B\right)\to \varnothing \notin \mathrm{ran}\underset{\dot{}}{⨣}$$
10	1 2 3	plusfreseq	$$⊢\varnothing \notin \mathrm{ran}\underset{\dot{}}{⨣}\to {\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}=\underset{\dot{}}{⨣}$$
11	9 10	syl	$$⊢\left(M\in \mathrm{Mgm}\wedge \varnothing \notin B\right)\to {\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}=\underset{\dot{}}{⨣}$$