Step | Hyp | Ref
| Expression |
1 | | df-nsg 17592 |
. . . 4
⊢ NrmSGrp =
(𝑔 ∈ Grp ↦
{𝑠 ∈
(SubGrp‘𝑔) ∣
[(Base‘𝑔) /
𝑏][(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)}) |
2 | 1 | dmmptss 5631 |
. . 3
⊢ dom
NrmSGrp ⊆ Grp |
3 | | elfvdm 6220 |
. . 3
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝐺 ∈ dom NrmSGrp) |
4 | 2, 3 | sseldi 3601 |
. 2
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝐺 ∈ Grp) |
5 | | subgrcl 17599 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
6 | 5 | adantr 481 |
. 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)) → 𝐺 ∈ Grp) |
7 | | fveq2 6191 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (SubGrp‘𝑔) = (SubGrp‘𝐺)) |
8 | | fvexd 6203 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Base‘𝑔) ∈ V) |
9 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
10 | | isnsg.1 |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
11 | 9, 10 | syl6eqr 2674 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑋) |
12 | | fvexd 6203 |
. . . . . . . 8
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → (+g‘𝑔) ∈ V) |
13 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → 𝑔 = 𝐺) |
14 | 13 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → (+g‘𝑔) = (+g‘𝐺)) |
15 | | isnsg.2 |
. . . . . . . . 9
⊢ + =
(+g‘𝐺) |
16 | 14, 15 | syl6eqr 2674 |
. . . . . . . 8
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → (+g‘𝑔) = + ) |
17 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → 𝑏 = 𝑋) |
18 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → 𝑝 = + ) |
19 | 18 | oveqd 6667 |
. . . . . . . . . . . 12
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (𝑥𝑝𝑦) = (𝑥 + 𝑦)) |
20 | 19 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑥 + 𝑦) ∈ 𝑠)) |
21 | 18 | oveqd 6667 |
. . . . . . . . . . . 12
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (𝑦𝑝𝑥) = (𝑦 + 𝑥)) |
22 | 21 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → ((𝑦𝑝𝑥) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)) |
23 | 20, 22 | bibi12d 335 |
. . . . . . . . . 10
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
24 | 17, 23 | raleqbidv 3152 |
. . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
25 | 17, 24 | raleqbidv 3152 |
. . . . . . . 8
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
26 | 12, 16, 25 | sbcied2 3473 |
. . . . . . 7
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → ([(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
27 | 8, 11, 26 | sbcied2 3473 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
28 | 7, 27 | rabeqbidv 3195 |
. . . . 5
⊢ (𝑔 = 𝐺 → {𝑠 ∈ (SubGrp‘𝑔) ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)} = {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)}) |
29 | | fvex 6201 |
. . . . . 6
⊢
(SubGrp‘𝐺)
∈ V |
30 | 29 | rabex 4813 |
. . . . 5
⊢ {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)} ∈ V |
31 | 28, 1, 30 | fvmpt 6282 |
. . . 4
⊢ (𝐺 ∈ Grp →
(NrmSGrp‘𝐺) = {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)}) |
32 | 31 | eleq2d 2687 |
. . 3
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (NrmSGrp‘𝐺) ↔ 𝑆 ∈ {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)})) |
33 | | eleq2 2690 |
. . . . . 6
⊢ (𝑠 = 𝑆 → ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑥 + 𝑦) ∈ 𝑆)) |
34 | | eleq2 2690 |
. . . . . 6
⊢ (𝑠 = 𝑆 → ((𝑦 + 𝑥) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑆)) |
35 | 33, 34 | bibi12d 335 |
. . . . 5
⊢ (𝑠 = 𝑆 → (((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠) ↔ ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) |
36 | 35 | 2ralbidv 2989 |
. . . 4
⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) |
37 | 36 | elrab 3363 |
. . 3
⊢ (𝑆 ∈ {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)} ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) |
38 | 32, 37 | syl6bb 276 |
. 2
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)))) |
39 | 4, 6, 38 | pm5.21nii 368 |
1
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) |