Step | Hyp | Ref
| Expression |
1 | | id 19 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (SubGrp‘𝐺)) |
2 | | elnmz.1 |
. . . 4
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)} |
3 | | nmzsubg.2 |
. . . 4
⊢ 𝑋 = (Base‘𝐺) |
4 | | nmzsubg.3 |
. . . 4
⊢ + =
(+g‘𝐺) |
5 | 2, 3, 4 | ssnmz 13002 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝑁) |
6 | | subgrcl 12970 |
. . . . 5
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
7 | 2, 3, 4 | nmzsubg 13001 |
. . . . 5
⊢ (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺)) |
8 | 6, 7 | syl 14 |
. . . 4
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑁 ∈ (SubGrp‘𝐺)) |
9 | | nmznsg.4 |
. . . . 5
⊢ 𝐻 = (𝐺 ↾s 𝑁) |
10 | 9 | subsubg 12988 |
. . . 4
⊢ (𝑁 ∈ (SubGrp‘𝐺) → (𝑆 ∈ (SubGrp‘𝐻) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑆 ⊆ 𝑁))) |
11 | 8, 10 | syl 14 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝑆 ∈ (SubGrp‘𝐻) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑆 ⊆ 𝑁))) |
12 | 1, 5, 11 | mpbir2and 944 |
. 2
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (SubGrp‘𝐻)) |
13 | 2 | ssrab3 3241 |
. . . . . 6
⊢ 𝑁 ⊆ 𝑋 |
14 | 13 | sseli 3151 |
. . . . 5
⊢ (𝑤 ∈ 𝑁 → 𝑤 ∈ 𝑋) |
15 | 2 | nmzbi 13000 |
. . . . 5
⊢ ((𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑋) → ((𝑧 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝑧) ∈ 𝑆)) |
16 | 14, 15 | sylan2 286 |
. . . 4
⊢ ((𝑧 ∈ 𝑁 ∧ 𝑤 ∈ 𝑁) → ((𝑧 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝑧) ∈ 𝑆)) |
17 | 16 | rgen2 2563 |
. . 3
⊢
∀𝑧 ∈
𝑁 ∀𝑤 ∈ 𝑁 ((𝑧 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝑧) ∈ 𝑆) |
18 | 9 | subgbas 12969 |
. . . . 5
⊢ (𝑁 ∈ (SubGrp‘𝐺) → 𝑁 = (Base‘𝐻)) |
19 | 8, 18 | syl 14 |
. . . 4
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑁 = (Base‘𝐻)) |
20 | 19 | raleqdv 2678 |
. . . 4
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (∀𝑤 ∈ 𝑁 ((𝑧 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝑧) ∈ 𝑆) ↔ ∀𝑤 ∈ (Base‘𝐻)((𝑧 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝑧) ∈ 𝑆))) |
21 | 19, 20 | raleqbidv 2684 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (∀𝑧 ∈ 𝑁 ∀𝑤 ∈ 𝑁 ((𝑧 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝑧) ∈ 𝑆) ↔ ∀𝑧 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑧 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝑧) ∈ 𝑆))) |
22 | 17, 21 | mpbii 148 |
. 2
⊢ (𝑆 ∈ (SubGrp‘𝐺) → ∀𝑧 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑧 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝑧) ∈ 𝑆)) |
23 | | eqid 2177 |
. . . 4
⊢
(Base‘𝐻) =
(Base‘𝐻) |
24 | | eqid 2177 |
. . . 4
⊢
(+g‘𝐻) = (+g‘𝐻) |
25 | 23, 24 | isnsg 12993 |
. . 3
⊢ (𝑆 ∈ (NrmSGrp‘𝐻) ↔ (𝑆 ∈ (SubGrp‘𝐻) ∧ ∀𝑧 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑧(+g‘𝐻)𝑤) ∈ 𝑆 ↔ (𝑤(+g‘𝐻)𝑧) ∈ 𝑆))) |
26 | 9 | a1i 9 |
. . . . . . . . 9
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 = (𝐺 ↾s 𝑁)) |
27 | 4 | a1i 9 |
. . . . . . . . 9
⊢ (𝑆 ∈ (SubGrp‘𝐺) → + =
(+g‘𝐺)) |
28 | 26, 27, 8, 6 | ressplusgd 12579 |
. . . . . . . 8
⊢ (𝑆 ∈ (SubGrp‘𝐺) → + =
(+g‘𝐻)) |
29 | 28 | oveqd 5889 |
. . . . . . 7
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝑧 + 𝑤) = (𝑧(+g‘𝐻)𝑤)) |
30 | 29 | eleq1d 2246 |
. . . . . 6
⊢ (𝑆 ∈ (SubGrp‘𝐺) → ((𝑧 + 𝑤) ∈ 𝑆 ↔ (𝑧(+g‘𝐻)𝑤) ∈ 𝑆)) |
31 | 28 | oveqd 5889 |
. . . . . . 7
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝑤 + 𝑧) = (𝑤(+g‘𝐻)𝑧)) |
32 | 31 | eleq1d 2246 |
. . . . . 6
⊢ (𝑆 ∈ (SubGrp‘𝐺) → ((𝑤 + 𝑧) ∈ 𝑆 ↔ (𝑤(+g‘𝐻)𝑧) ∈ 𝑆)) |
33 | 30, 32 | bibi12d 235 |
. . . . 5
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (((𝑧 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝑧) ∈ 𝑆) ↔ ((𝑧(+g‘𝐻)𝑤) ∈ 𝑆 ↔ (𝑤(+g‘𝐻)𝑧) ∈ 𝑆))) |
34 | 33 | 2ralbidv 2501 |
. . . 4
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (∀𝑧 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑧 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝑧) ∈ 𝑆) ↔ ∀𝑧 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑧(+g‘𝐻)𝑤) ∈ 𝑆 ↔ (𝑤(+g‘𝐻)𝑧) ∈ 𝑆))) |
35 | 34 | anbi2d 464 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → ((𝑆 ∈ (SubGrp‘𝐻) ∧ ∀𝑧 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑧 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝑧) ∈ 𝑆)) ↔ (𝑆 ∈ (SubGrp‘𝐻) ∧ ∀𝑧 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑧(+g‘𝐻)𝑤) ∈ 𝑆 ↔ (𝑤(+g‘𝐻)𝑧) ∈ 𝑆)))) |
36 | 25, 35 | bitr4id 199 |
. 2
⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝑆 ∈ (NrmSGrp‘𝐻) ↔ (𝑆 ∈ (SubGrp‘𝐻) ∧ ∀𝑧 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑧 + 𝑤) ∈ 𝑆 ↔ (𝑤 + 𝑧) ∈ 𝑆)))) |
37 | 12, 22, 36 | mpbir2and 944 |
1
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (NrmSGrp‘𝐻)) |