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 )