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 ) ) )