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