Database
BASIC ALGEBRAIC STRUCTURES
Groups
Subgroups and Quotient groups
nsgbi
Next ⟩
nsgsubg
Metamath Proof Explorer
Ascii
Unicode
Theorem
nsgbi
Description:
Defining property of a normal subgroup.
(Contributed by
Mario Carneiro
, 18-Jan-2015)
Ref
Expression
Hypotheses
isnsg.1
⊢
X
=
Base
G
isnsg.2
⊢
+
˙
=
+
G
Assertion
nsgbi
⊢
S
∈
NrmSGrp
⁡
G
∧
A
∈
X
∧
B
∈
X
→
A
+
˙
B
∈
S
↔
B
+
˙
A
∈
S
Proof
Step
Hyp
Ref
Expression
1
isnsg.1
⊢
X
=
Base
G
2
isnsg.2
⊢
+
˙
=
+
G
3
1
2
isnsg
⊢
S
∈
NrmSGrp
⁡
G
↔
S
∈
SubGrp
⁡
G
∧
∀
x
∈
X
∀
y
∈
X
x
+
˙
y
∈
S
↔
y
+
˙
x
∈
S
4
3
simprbi
⊢
S
∈
NrmSGrp
⁡
G
→
∀
x
∈
X
∀
y
∈
X
x
+
˙
y
∈
S
↔
y
+
˙
x
∈
S
5
oveq1
⊢
x
=
A
→
x
+
˙
y
=
A
+
˙
y
6
5
eleq1d
⊢
x
=
A
→
x
+
˙
y
∈
S
↔
A
+
˙
y
∈
S
7
oveq2
⊢
x
=
A
→
y
+
˙
x
=
y
+
˙
A
8
7
eleq1d
⊢
x
=
A
→
y
+
˙
x
∈
S
↔
y
+
˙
A
∈
S
9
6
8
bibi12d
⊢
x
=
A
→
x
+
˙
y
∈
S
↔
y
+
˙
x
∈
S
↔
A
+
˙
y
∈
S
↔
y
+
˙
A
∈
S
10
oveq2
⊢
y
=
B
→
A
+
˙
y
=
A
+
˙
B
11
10
eleq1d
⊢
y
=
B
→
A
+
˙
y
∈
S
↔
A
+
˙
B
∈
S
12
oveq1
⊢
y
=
B
→
y
+
˙
A
=
B
+
˙
A
13
12
eleq1d
⊢
y
=
B
→
y
+
˙
A
∈
S
↔
B
+
˙
A
∈
S
14
11
13
bibi12d
⊢
y
=
B
→
A
+
˙
y
∈
S
↔
y
+
˙
A
∈
S
↔
A
+
˙
B
∈
S
↔
B
+
˙
A
∈
S
15
9
14
rspc2v
⊢
A
∈
X
∧
B
∈
X
→
∀
x
∈
X
∀
y
∈
X
x
+
˙
y
∈
S
↔
y
+
˙
x
∈
S
→
A
+
˙
B
∈
S
↔
B
+
˙
A
∈
S
16
4
15
syl5com
⊢
S
∈
NrmSGrp
⁡
G
→
A
∈
X
∧
B
∈
X
→
A
+
˙
B
∈
S
↔
B
+
˙
A
∈
S
17
16
3impib
⊢
S
∈
NrmSGrp
⁡
G
∧
A
∈
X
∧
B
∈
X
→
A
+
˙
B
∈
S
↔
B
+
˙
A
∈
S