Step | Hyp | Ref
| Expression |
1 | | df-nsg 17415 |
. . . 4
⊢ NrmSGrp =
(𝑔 ∈ Grp ↦
{𝑠 ∈
(SubGrp‘𝑔) ∣
[(Base‘𝑔) /
𝑏][(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)}) |
2 | 1 | dmmptss 5548 |
. . 3
⊢ dom
NrmSGrp ⊆ Grp |
3 | | elfvdm 6130 |
. . 3
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝐺 ∈ dom NrmSGrp) |
4 | 2, 3 | sseldi 3566 |
. 2
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝐺 ∈ Grp) |
5 | | subgrcl 17422 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
6 | 5 | adantr 480 |
. 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)) → 𝐺 ∈ Grp) |
7 | | fveq2 6103 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (SubGrp‘𝑔) = (SubGrp‘𝐺)) |
8 | | fvex 6113 |
. . . . . . . 8
⊢
(Base‘𝑔)
∈ V |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Base‘𝑔) ∈ V) |
10 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
11 | | isnsg.1 |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
12 | 10, 11 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑋) |
13 | | fvex 6113 |
. . . . . . . . 9
⊢
(+g‘𝑔) ∈ V |
14 | 13 | a1i 11 |
. . . . . . . 8
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → (+g‘𝑔) ∈ V) |
15 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → 𝑔 = 𝐺) |
16 | 15 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → (+g‘𝑔) = (+g‘𝐺)) |
17 | | isnsg.2 |
. . . . . . . . 9
⊢ + =
(+g‘𝐺) |
18 | 16, 17 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → (+g‘𝑔) = + ) |
19 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → 𝑏 = 𝑋) |
20 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → 𝑝 = + ) |
21 | 20 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (𝑥𝑝𝑦) = (𝑥 + 𝑦)) |
22 | 21 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑥 + 𝑦) ∈ 𝑠)) |
23 | 20 | oveqd 6566 |
. . . . . . . . . . . 12
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (𝑦𝑝𝑥) = (𝑦 + 𝑥)) |
24 | 23 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → ((𝑦𝑝𝑥) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)) |
25 | 22, 24 | bibi12d 334 |
. . . . . . . . . 10
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
26 | 19, 25 | raleqbidv 3129 |
. . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
27 | 19, 26 | raleqbidv 3129 |
. . . . . . . 8
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
28 | 14, 18, 27 | sbcied2 3440 |
. . . . . . 7
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → ([(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
29 | 9, 12, 28 | sbcied2 3440 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
30 | 7, 29 | rabeqbidv 3168 |
. . . . 5
⊢ (𝑔 = 𝐺 → {𝑠 ∈ (SubGrp‘𝑔) ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)} = {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)}) |
31 | | fvex 6113 |
. . . . . 6
⊢
(SubGrp‘𝐺)
∈ V |
32 | 31 | rabex 4740 |
. . . . 5
⊢ {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)} ∈ V |
33 | 30, 1, 32 | fvmpt 6191 |
. . . 4
⊢ (𝐺 ∈ Grp →
(NrmSGrp‘𝐺) = {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)}) |
34 | 33 | eleq2d 2673 |
. . 3
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (NrmSGrp‘𝐺) ↔ 𝑆 ∈ {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)})) |
35 | | eleq2 2677 |
. . . . . 6
⊢ (𝑠 = 𝑆 → ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑥 + 𝑦) ∈ 𝑆)) |
36 | | eleq2 2677 |
. . . . . 6
⊢ (𝑠 = 𝑆 → ((𝑦 + 𝑥) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑆)) |
37 | 35, 36 | bibi12d 334 |
. . . . 5
⊢ (𝑠 = 𝑆 → (((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠) ↔ ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) |
38 | 37 | 2ralbidv 2972 |
. . . 4
⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) |
39 | 38 | elrab 3331 |
. . 3
⊢ (𝑆 ∈ {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)} ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) |
40 | 34, 39 | syl6bb 275 |
. 2
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)))) |
41 | 4, 6, 40 | pm5.21nii 367 |
1
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) |