Theorem plusfreseq

Description: If the empty set is not contained in the range of the group addition function of an extensible structure (not necessarily 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	plusfreseq	$$⊢\varnothing \notin \mathrm{ran}\underset{\dot{}}{⨣}\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	plusffn	$$⊢\underset{\dot{}}{⨣}Fn\left(B\times B\right)$$
5		fnfun	$$⊢\underset{\dot{}}{⨣}Fn\left(B\times B\right)\to \mathrm{Fun}\underset{\dot{}}{⨣}$$
6	4 5	ax-mp	$$⊢\mathrm{Fun}\underset{\dot{}}{⨣}$$
7	6	a1i	$$⊢\varnothing \notin \mathrm{ran}\underset{\dot{}}{⨣}\to \mathrm{Fun}\underset{\dot{}}{⨣}$$
8		id	$$⊢\varnothing \notin \mathrm{ran}\underset{\dot{}}{⨣}\to \varnothing \notin \mathrm{ran}\underset{\dot{}}{⨣}$$
9	1 2 3	plusfval	$$⊢\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{⨣}y=x\underset{\dot{}}{+}y$$
10	9	eqcomd	$$⊢\left(x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y=x\underset{\dot{}}{⨣}y$$
11	10	rgen2	$$⊢\forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=x\underset{\dot{}}{⨣}y$$
12	11	a1i	$$⊢\varnothing \notin \mathrm{ran}\underset{\dot{}}{⨣}\to \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=x\underset{\dot{}}{⨣}y$$
13		fveq2	$$⊢p=⟨x,y⟩\to \underset{\dot{}}{+}\left(p\right)=\underset{\dot{}}{+}\left(⟨x,y⟩\right)$$
14		df-ov	$$⊢x\underset{\dot{}}{+}y=\underset{\dot{}}{+}\left(⟨x,y⟩\right)$$
15	13 14	eqtr4di	$$⊢p=⟨x,y⟩\to \underset{\dot{}}{+}\left(p\right)=x\underset{\dot{}}{+}y$$
16		fveq2	$$⊢p=⟨x,y⟩\to \underset{\dot{}}{⨣}\left(p\right)=\underset{\dot{}}{⨣}\left(⟨x,y⟩\right)$$
17		df-ov	$$⊢x\underset{\dot{}}{⨣}y=\underset{\dot{}}{⨣}\left(⟨x,y⟩\right)$$
18	16 17	eqtr4di	$$⊢p=⟨x,y⟩\to \underset{\dot{}}{⨣}\left(p\right)=x\underset{\dot{}}{⨣}y$$
19	15 18	eqeq12d	$$⊢p=⟨x,y⟩\to \left(\underset{\dot{}}{+}\left(p\right)=\underset{\dot{}}{⨣}\left(p\right)\leftrightarrow x\underset{\dot{}}{+}y=x\underset{\dot{}}{⨣}y\right)$$
20	19	ralxp	$$⊢\forall p\in \left(B\times B\right)\underset{\dot{}}{+}\left(p\right)=\underset{\dot{}}{⨣}\left(p\right)\leftrightarrow \forall x\in B\forall y\in Bx\underset{\dot{}}{+}y=x\underset{\dot{}}{⨣}y$$
21	12 20	sylibr	$$⊢\varnothing \notin \mathrm{ran}\underset{\dot{}}{⨣}\to \forall p\in \left(B\times B\right)\underset{\dot{}}{+}\left(p\right)=\underset{\dot{}}{⨣}\left(p\right)$$
22		fndm	$$⊢\underset{\dot{}}{⨣}Fn\left(B\times B\right)\to \mathrm{dom}\underset{\dot{}}{⨣}=B\times B$$
23	22	eqcomd	$$⊢\underset{\dot{}}{⨣}Fn\left(B\times B\right)\to B\times B=\mathrm{dom}\underset{\dot{}}{⨣}$$
24	4 23	ax-mp	$$⊢B\times B=\mathrm{dom}\underset{\dot{}}{⨣}$$
25	24	fveqressseq	$$⊢\left(\mathrm{Fun}\underset{\dot{}}{⨣}\wedge \varnothing \notin \mathrm{ran}\underset{\dot{}}{⨣}\wedge \forall p\in \left(B\times B\right)\underset{\dot{}}{+}\left(p\right)=\underset{\dot{}}{⨣}\left(p\right)\right)\to {\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}=\underset{\dot{}}{⨣}$$
26	7 8 21 25	syl3anc	$$⊢\varnothing \notin \mathrm{ran}\underset{\dot{}}{⨣}\to {\underset{\dot{}}{+}\upharpoonright }_{\left(B\times B\right)}=\underset{\dot{}}{⨣}$$