# Metamath Proof Explorer

## 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}{↾}_{𝑠}{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}{↾}_{𝑠}{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}}×{\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}}×{\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}×{S}={\mathrm{Base}}_{{H}}×{\mathrm{Base}}_{{H}}$
11 7 10 9 foeq123d ${⊢}\left({H}\in \mathrm{Grp}\wedge {S}\subseteq {B}\right)\to \left({F}:{S}×{S}\underset{onto}{⟶}{S}↔{F}:{\mathrm{Base}}_{{H}}×{\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}×{S}\underset{onto}{⟶}{S}$
13 forn ${⊢}{F}:{S}×{S}\underset{onto}{⟶}{S}\to \mathrm{ran}{F}={S}$
14 13 eqcomd ${⊢}{F}:{S}×{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}$