This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( Base ` G )
resgrpplusfrn.h 
|- H = ( G |`s S )
resgrpplusfrn.o 
|- F = ( +f ` H )
Assertion resgrpplusfrn 
|- ( ( H e. Grp /\ S C_ B ) -> S = ran F )

Proof

Step Hyp Ref Expression
1 resgrpplusfrn.b 
 |-  B = ( Base ` G )
2 resgrpplusfrn.h 
 |-  H = ( G |`s S )
3 resgrpplusfrn.o 
 |-  F = ( +f ` H )
4 eqid 
 |-  ( Base ` H ) = ( Base ` H )
5 4 3 grpplusfo 
 |-  ( H e. Grp -> F : ( ( Base ` H ) X. ( Base ` H ) ) -onto-> ( Base ` H ) )
6 5 adantr 
 |-  ( ( H e. Grp /\ S C_ B ) -> F : ( ( Base ` H ) X. ( Base ` H ) ) -onto-> ( Base ` H ) )
7 eqidd 
 |-  ( ( H e. Grp /\ S C_ B ) -> F = F )
8 2 1 ressbas2 
 |-  ( S C_ B -> S = ( Base ` H ) )
9 8 adantl 
 |-  ( ( H e. Grp /\ S C_ B ) -> S = ( Base ` H ) )
10 9 sqxpeqd 
 |-  ( ( H e. Grp /\ S C_ B ) -> ( S X. S ) = ( ( Base ` H ) X. ( Base ` H ) ) )
11 7 10 9 foeq123d 
 |-  ( ( H e. Grp /\ S C_ B ) -> ( F : ( S X. S ) -onto-> S <-> F : ( ( Base ` H ) X. ( Base ` H ) ) -onto-> ( Base ` H ) ) )
12 6 11 mpbird 
 |-  ( ( H e. Grp /\ S C_ B ) -> F : ( S X. S ) -onto-> S )
13 forn 
 |-  ( F : ( S X. S ) -onto-> S -> ran F = S )
14 13 eqcomd 
 |-  ( F : ( S X. S ) -onto-> S -> S = ran F )
15 12 14 syl 
 |-  ( ( H e. Grp /\ S C_ B ) -> S = ran F )