Step |
Hyp |
Ref |
Expression |
1 |
|
elnmz.1 |
⊢ 𝑁 = { 𝑥 ∈ 𝑋 ∣ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 + 𝑦 ) ∈ 𝑆 ↔ ( 𝑦 + 𝑥 ) ∈ 𝑆 ) } |
2 |
|
nmzsubg.2 |
⊢ 𝑋 = ( Base ‘ 𝐺 ) |
3 |
|
nmzsubg.3 |
⊢ + = ( +g ‘ 𝐺 ) |
4 |
|
nmznsg.4 |
⊢ 𝐻 = ( 𝐺 ↾s 𝑁 ) |
5 |
|
id |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) |
6 |
1 2 3
|
ssnmz |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝑁 ) |
7 |
|
subgrcl |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp ) |
8 |
1 2 3
|
nmzsubg |
⊢ ( 𝐺 ∈ Grp → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) ) |
9 |
7 8
|
syl |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) ) |
10 |
4
|
subsubg |
⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑁 ) ) ) |
11 |
9 10
|
syl |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑆 ⊆ 𝑁 ) ) ) |
12 |
5 6 11
|
mpbir2and |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐻 ) ) |
13 |
1
|
ssrab3 |
⊢ 𝑁 ⊆ 𝑋 |
14 |
13
|
sseli |
⊢ ( 𝑤 ∈ 𝑁 → 𝑤 ∈ 𝑋 ) |
15 |
1
|
nmzbi |
⊢ ( ( 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ) |
16 |
14 15
|
sylan2 |
⊢ ( ( 𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁 ) → ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ) |
17 |
16
|
rgen2 |
⊢ ∀ 𝑧 ∈ 𝑁 ∀ 𝑤 ∈ 𝑁 ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) |
18 |
4
|
subgbas |
⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 = ( Base ‘ 𝐻 ) ) |
19 |
9 18
|
syl |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 = ( Base ‘ 𝐻 ) ) |
20 |
19
|
raleqdv |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( ∀ 𝑤 ∈ 𝑁 ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ) ) |
21 |
19 20
|
raleqbidv |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( ∀ 𝑧 ∈ 𝑁 ∀ 𝑤 ∈ 𝑁 ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ) ) |
22 |
17 21
|
mpbii |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ) |
23 |
|
eqid |
⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 ) |
24 |
2
|
fvexi |
⊢ 𝑋 ∈ V |
25 |
24 13
|
ssexi |
⊢ 𝑁 ∈ V |
26 |
4 3
|
ressplusg |
⊢ ( 𝑁 ∈ V → + = ( +g ‘ 𝐻 ) ) |
27 |
25 26
|
ax-mp |
⊢ + = ( +g ‘ 𝐻 ) |
28 |
23 27
|
isnsg |
⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐻 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐻 ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ∀ 𝑤 ∈ ( Base ‘ 𝐻 ) ( ( 𝑧 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝑧 ) ∈ 𝑆 ) ) ) |
29 |
12 22 28
|
sylanbrc |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ∈ ( NrmSGrp ‘ 𝐻 ) ) |