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