Theorem mgmn0plusgplusf

Description: The group addition function of a magma is the restriction of its group operation to its base set if the base set does not contain the empty set. (Contributed by AV, 16-Aug-2026)

	Ref	Expression
Hypotheses	mgmn0plusgf.b	$$⊢B={\mathrm{Base}}_G$$
	mgmn0plusgf.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	mgmn0plusgf.g	$$⊢\phi \to G\in \mathrm{Mgm}$$
	mgmn0plusgf.0	$$⊢\phi \to \varnothing \notin B$$
	mgmn0plusgplusf.p	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
Assertion	mgmn0plusgplusf	$$⊢\phi \to \underset{\dot{}}{⨣}={\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}$$

Proof

Step	Hyp	Ref	Expression
1		mgmn0plusgf.b	$$⊢B={\mathrm{Base}}_G$$
2		mgmn0plusgf.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		mgmn0plusgf.g	$$⊢\phi \to G\in \mathrm{Mgm}$$
4		mgmn0plusgf.0	$$⊢\phi \to \varnothing \notin B$$
5		mgmn0plusgplusf.p	$$⊢\underset{\dot{}}{⨣}={+}_{𝑓}\left(G\right)$$
6	1 5	mgmplusf	$$⊢G\in \mathrm{Mgm}\to \underset{\dot{}}{⨣}:B\times B⟶B$$
7	3 6	syl	$$⊢\phi \to \underset{\dot{}}{⨣}:B\times B⟶B$$
8	7	ffnd	$$⊢\phi \to \underset{\dot{}}{⨣}Fn\left(B\times B\right)$$
9		eqid	$$⊢{\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}={\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}$$
10	1 2 3 4 9	mgmn0plusgf	$$⊢\phi \to \left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right):B\times B⟶B$$
11	10	ffnd	$$⊢\phi \to \left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)Fn\left(B\times B\right)$$
12		elxp	$$⊢z\in \left(B\times B\right)\leftrightarrow \exists x\exists y\left(z=⟨x,y⟩\wedge \left(x\in B\wedge y\in B\right)\right)$$
13		df-ov	$$⊢x\underset{\dot{}}{+}y=\underset{\dot{}}{+}\left(⟨x,y⟩\right)$$
14	1 2 5	plusfval	$$⊢\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{⨣}y=x\underset{\dot{}}{+}y$$
15	14	ad2antlr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge z=⟨x,y⟩\right)\to x\underset{\dot{}}{⨣}y=x\underset{\dot{}}{+}y$$
16		opelxpi	$$⊢\left(x\in B\wedge y\in B\right)\to ⟨x,y⟩\in \left(B\times B\right)$$
17	16	ad2antlr	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge z=⟨x,y⟩\right)\to ⟨x,y⟩\in \left(B\times B\right)$$
18	17	fvresd	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge z=⟨x,y⟩\right)\to \left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(⟨x,y⟩\right)=\underset{\dot{}}{+}\left(⟨x,y⟩\right)$$
19	13 15 18	3eqtr4a	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge z=⟨x,y⟩\right)\to x\underset{\dot{}}{⨣}y=\left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(⟨x,y⟩\right)$$
20		fveq2	$$⊢z=⟨x,y⟩\to \underset{\dot{}}{⨣}\left(z\right)=\underset{\dot{}}{⨣}\left(⟨x,y⟩\right)$$
21		df-ov	$$⊢x\underset{\dot{}}{⨣}y=\underset{\dot{}}{⨣}\left(⟨x,y⟩\right)$$
22	20 21	eqtr4di	$$⊢z=⟨x,y⟩\to \underset{\dot{}}{⨣}\left(z\right)=x\underset{\dot{}}{⨣}y$$
23		fveq2	$$⊢z=⟨x,y⟩\to \left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(z\right)=\left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(⟨x,y⟩\right)$$
24	22 23	eqeq12d	$$⊢z=⟨x,y⟩\to \left(\underset{\dot{}}{⨣}\left(z\right)=\left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(z\right)\leftrightarrow x\underset{\dot{}}{⨣}y=\left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(⟨x,y⟩\right)\right)$$
25	24	adantl	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge z=⟨x,y⟩\right)\to \left(\underset{\dot{}}{⨣}\left(z\right)=\left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(z\right)\leftrightarrow x\underset{\dot{}}{⨣}y=\left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(⟨x,y⟩\right)\right)$$
26	19 25	mpbird	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\wedge z=⟨x,y⟩\right)\to \underset{\dot{}}{⨣}\left(z\right)=\left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(z\right)$$
27	26	exp31	$$⊢\phi \to \left(\left(x\in B\wedge y\in B\right)\to \left(z=⟨x,y⟩\to \underset{\dot{}}{⨣}\left(z\right)=\left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(z\right)\right)\right)$$
28	27	impcomd	$$⊢\phi \to \left(\left(z=⟨x,y⟩\wedge \left(x\in B\wedge y\in B\right)\right)\to \underset{\dot{}}{⨣}\left(z\right)=\left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(z\right)\right)$$
29	28	exlimdvv	$$⊢\phi \to \left(\exists x\exists y\left(z=⟨x,y⟩\wedge \left(x\in B\wedge y\in B\right)\right)\to \underset{\dot{}}{⨣}\left(z\right)=\left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(z\right)\right)$$
30	12 29	biimtrid	$$⊢\phi \to \left(z\in \left(B\times B\right)\to \underset{\dot{}}{⨣}\left(z\right)=\left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(z\right)\right)$$
31	30	imp	$$⊢\left(\phi \wedge z\in \left(B\times B\right)\right)\to \underset{\dot{}}{⨣}\left(z\right)=\left({\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}\right)\left(z\right)$$
32	8 11 31	eqfnfvd	$$⊢\phi \to \underset{\dot{}}{⨣}={\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}$$