Theorem resgrpplusfrn

Description: The underlying set of a group operation which is a restriction of a structure. (Contributed by Paul Chapman, 25-Mar-2008) (Revised by AV, 30-Aug-2021)

	Ref	Expression
Hypotheses	resgrpplusfrn.b	$$⊢B={\mathrm{Base}}_G$$
	resgrpplusfrn.h	$$⊢H=G{\upharpoonright }_{𝑠}S$$
	resgrpplusfrn.o	$$⊢F={+}_{𝑓}\left(H\right)$$
Assertion	resgrpplusfrn	$$⊢\left(H\in \mathrm{Grp}\wedge S\subseteq B\right)\to S=\mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		resgrpplusfrn.b	$$⊢B={\mathrm{Base}}_G$$
2		resgrpplusfrn.h	$$⊢H=G{\upharpoonright }_{𝑠}S$$
3		resgrpplusfrn.o	$$⊢F={+}_{𝑓}\left(H\right)$$
4		eqid	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_H$$
5	4 3	grpplusfo	$$⊢H\in \mathrm{Grp}\to F:{\mathrm{Base}}_H\times {\mathrm{Base}}_H\underset{onto}{⟶}{\mathrm{Base}}_H$$
6	5	adantr	$$⊢\left(H\in \mathrm{Grp}\wedge S\subseteq B\right)\to F:{\mathrm{Base}}_H\times {\mathrm{Base}}_H\underset{onto}{⟶}{\mathrm{Base}}_H$$
7		eqidd	$$⊢\left(H\in \mathrm{Grp}\wedge S\subseteq B\right)\to F=F$$
8	2 1	ressbas2	$$⊢S\subseteq B\to S={\mathrm{Base}}_H$$
9	8	adantl	$$⊢\left(H\in \mathrm{Grp}\wedge S\subseteq B\right)\to S={\mathrm{Base}}_H$$
10	9	sqxpeqd	$$⊢\left(H\in \mathrm{Grp}\wedge S\subseteq B\right)\to S\times S={\mathrm{Base}}_H\times {\mathrm{Base}}_H$$
11	7 10 9	foeq123d	$$⊢\left(H\in \mathrm{Grp}\wedge S\subseteq B\right)\to \left(F:S\times S\underset{onto}{⟶}S\leftrightarrow F:{\mathrm{Base}}_H\times {\mathrm{Base}}_H\underset{onto}{⟶}{\mathrm{Base}}_H\right)$$
12	6 11	mpbird	$$⊢\left(H\in \mathrm{Grp}\wedge S\subseteq B\right)\to F:S\times S\underset{onto}{⟶}S$$
13		forn	$$⊢F:S\times S\underset{onto}{⟶}S\to \mathrm{ran}F=S$$
14	13	eqcomd	$$⊢F:S\times S\underset{onto}{⟶}S\to S=\mathrm{ran}F$$
15	12 14	syl	$$⊢\left(H\in \mathrm{Grp}\wedge S\subseteq B\right)\to S=\mathrm{ran}F$$