This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subggim

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

Ref Expression
Hypothesis subgim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion subggim ( ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ↔ ( 𝐹 “ 𝐴 ) ∈ ( SubGrp ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 subgim.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 gimghm ⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
3 2 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝐴 ⊆ 𝐵 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
4 ghmima ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝐹 “ 𝐴 ) ∈ ( SubGrp ‘ 𝑆 ) )
5 3 4 sylan ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝐹 “ 𝐴 ) ∈ ( SubGrp ‘ 𝑆 ) )
6 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
7 1 6 gimf1o ⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝐹 : 𝐵 –1-1-onto→ ( Base ‘ 𝑆 ) )
8 f1of1 ⊢ ( 𝐹 : 𝐵 –1-1-onto→ ( Base ‘ 𝑆 ) → 𝐹 : 𝐵 –1-1→ ( Base ‘ 𝑆 ) )
9 7 8 syl ⊢ ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝐹 : 𝐵 –1-1→ ( Base ‘ 𝑆 ) )
10 f1imacnv ⊢ ( ( 𝐹 : 𝐵 –1-1→ ( Base ‘ 𝑆 ) ∧ 𝐴 ⊆ 𝐵 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) = 𝐴 )
11 9 10 sylan ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝐴 ⊆ 𝐵 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) = 𝐴 )
12 11 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝐹 “ 𝐴 ) ∈ ( SubGrp ‘ 𝑆 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) = 𝐴 )
13 ghmpreima ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( 𝐹 “ 𝐴 ) ∈ ( SubGrp ‘ 𝑆 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) ∈ ( SubGrp ‘ 𝑅 ) )
14 3 13 sylan ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝐹 “ 𝐴 ) ∈ ( SubGrp ‘ 𝑆 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝐴 ) ) ∈ ( SubGrp ‘ 𝑅 ) )
15 12 14 eqeltrrd ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝐴 ⊆ 𝐵 ) ∧ ( 𝐹 “ 𝐴 ) ∈ ( SubGrp ‘ 𝑆 ) ) → 𝐴 ∈ ( SubGrp ‘ 𝑅 ) )
16 5 15 impbida ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) ↔ ( 𝐹 “ 𝐴 ) ∈ ( SubGrp ‘ 𝑆 ) ) )