Database
BASIC ALGEBRAIC STRUCTURES
Groups
Isomorphisms of groups
subggim
Next ⟩
gimcnv
Metamath Proof Explorer
Ascii
Unicode
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