Metamath Proof Explorer


Theorem subggim

Description: Behavior of subgroups under isomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015)

Ref Expression
Hypothesis subgim.b
|- B = ( Base ` R )
Assertion subggim
|- ( ( F e. ( R GrpIso S ) /\ A C_ B ) -> ( A e. ( SubGrp ` R ) <-> ( F " A ) e. ( SubGrp ` S ) ) )

Proof

Step Hyp Ref Expression
1 subgim.b
 |-  B = ( Base ` R )
2 gimghm
 |-  ( F e. ( R GrpIso S ) -> F e. ( R GrpHom S ) )
3 2 adantr
 |-  ( ( F e. ( R GrpIso S ) /\ A C_ B ) -> F e. ( R GrpHom S ) )
4 ghmima
 |-  ( ( F e. ( R GrpHom S ) /\ A e. ( SubGrp ` R ) ) -> ( F " A ) e. ( SubGrp ` S ) )
5 3 4 sylan
 |-  ( ( ( F e. ( R GrpIso S ) /\ A C_ B ) /\ A e. ( SubGrp ` R ) ) -> ( F " A ) e. ( SubGrp ` S ) )
6 eqid
 |-  ( Base ` S ) = ( Base ` S )
7 1 6 gimf1o
 |-  ( F e. ( R GrpIso S ) -> F : B -1-1-onto-> ( Base ` S ) )
8 f1of1
 |-  ( F : B -1-1-onto-> ( Base ` S ) -> F : B -1-1-> ( Base ` S ) )
9 7 8 syl
 |-  ( F e. ( R GrpIso S ) -> F : B -1-1-> ( Base ` S ) )
10 f1imacnv
 |-  ( ( F : B -1-1-> ( Base ` S ) /\ A C_ B ) -> ( `' F " ( F " A ) ) = A )
11 9 10 sylan
 |-  ( ( F e. ( R GrpIso S ) /\ A C_ B ) -> ( `' F " ( F " A ) ) = A )
12 11 adantr
 |-  ( ( ( F e. ( R GrpIso S ) /\ A C_ B ) /\ ( F " A ) e. ( SubGrp ` S ) ) -> ( `' F " ( F " A ) ) = A )
13 ghmpreima
 |-  ( ( F e. ( R GrpHom S ) /\ ( F " A ) e. ( SubGrp ` S ) ) -> ( `' F " ( F " A ) ) e. ( SubGrp ` R ) )
14 3 13 sylan
 |-  ( ( ( F e. ( R GrpIso S ) /\ A C_ B ) /\ ( F " A ) e. ( SubGrp ` S ) ) -> ( `' F " ( F " A ) ) e. ( SubGrp ` R ) )
15 12 14 eqeltrrd
 |-  ( ( ( F e. ( R GrpIso S ) /\ A C_ B ) /\ ( F " A ) e. ( SubGrp ` S ) ) -> A e. ( SubGrp ` R ) )
16 5 15 impbida
 |-  ( ( F e. ( R GrpIso S ) /\ A C_ B ) -> ( A e. ( SubGrp ` R ) <-> ( F " A ) e. ( SubGrp ` S ) ) )