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 \in (R GrpIso S) \land A \subseteq B) \to (A \in SubGrp (R) \leftrightarrow F [A] \in SubGrp (S))$

Step	Hyp	Ref	Expression
1		subgim.b	$⊢ B = {Base}_{R}$
2		gimghm	$⊢ F \in (R GrpIso S) \to F \in (R GrpHom S)$
3	2	adantr	$⊢ (F \in (R GrpIso S) \land A \subseteq B) \to F \in (R GrpHom S)$
4		ghmima	$⊢ (F \in (R GrpHom S) \land A \in SubGrp (R)) \to F [A] \in SubGrp (S)$
5	3 4	sylan	$⊢ ((F \in (R GrpIso S) \land A \subseteq B) \land A \in SubGrp (R)) \to F [A] \in SubGrp (S)$
6		eqid	$⊢ {Base}_{S} = {Base}_{S}$
7	1 6	gimf1o	$⊢ F \in (R GrpIso S) \to F : B \underset{1-1 onto}{⟶} {Base}_{S}$
8		f1of1	$⊢ F : B \underset{1-1 onto}{⟶} {Base}_{S} \to F : B \underset{1-1}{⟶} {Base}_{S}$
9	7 8	syl	$⊢ F \in (R GrpIso S) \to F : B \underset{1-1}{⟶} {Base}_{S}$
10		f1imacnv	$⊢ (F : B \underset{1-1}{⟶} {Base}_{S} \land A \subseteq B) \to F^{-1} [F [A]] = A$
11	9 10	sylan	$⊢ (F \in (R GrpIso S) \land A \subseteq B) \to F^{-1} [F [A]] = A$
12	11	adantr	$⊢ ((F \in (R GrpIso S) \land A \subseteq B) \land F [A] \in SubGrp (S)) \to F^{-1} [F [A]] = A$
13		ghmpreima	$⊢ (F \in (R GrpHom S) \land F [A] \in SubGrp (S)) \to F^{-1} [F [A]] \in SubGrp (R)$
14	3 13	sylan	$⊢ ((F \in (R GrpIso S) \land A \subseteq B) \land F [A] \in SubGrp (S)) \to F^{-1} [F [A]] \in SubGrp (R)$
15	12 14	eqeltrrd	$⊢ ((F \in (R GrpIso S) \land A \subseteq B) \land F [A] \in SubGrp (S)) \to A \in SubGrp (R)$
16	5 15	impbida	$⊢ (F \in (R GrpIso S) \land A \subseteq B) \to (A \in SubGrp (R) \leftrightarrow F [A] \in SubGrp (S))$

Metamath Proof Explorer