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 R GrpIso S A B A SubGrp R F A SubGrp S

Proof

Step Hyp Ref Expression
1 subgim.b B = Base R
2 gimghm F R GrpIso S F R GrpHom S
3 2 adantr F R GrpIso S A B F R GrpHom S
4 ghmima F R GrpHom S A SubGrp R F A SubGrp S
5 3 4 sylan F R GrpIso S A B A SubGrp R F A SubGrp S
6 eqid Base S = Base S
7 1 6 gimf1o F 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 R GrpIso S F : B 1-1 Base S
10 f1imacnv F : B 1-1 Base S A B F -1 F A = A
11 9 10 sylan F R GrpIso S A B F -1 F A = A
12 11 adantr F R GrpIso S A B F A SubGrp S F -1 F A = A
13 ghmpreima F R GrpHom S F A SubGrp S F -1 F A SubGrp R
14 3 13 sylan F R GrpIso S A B F A SubGrp S F -1 F A SubGrp R
15 12 14 eqeltrrd F R GrpIso S A B F A SubGrp S A SubGrp R
16 5 15 impbida F R GrpIso S A B A SubGrp R F A SubGrp S