| Step | Hyp | Ref
| Expression |
| 1 | | df-nsg 19142 |
. . 3
⊢ NrmSGrp =
(𝑔 ∈ Grp ↦
{𝑠 ∈
(SubGrp‘𝑔) ∣
[(Base‘𝑔) /
𝑏][(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)}) |
| 2 | 1 | mptrcl 7025 |
. 2
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝐺 ∈ Grp) |
| 3 | | subgrcl 19149 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
| 4 | 3 | adantr 480 |
. 2
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)) → 𝐺 ∈ Grp) |
| 5 | | fveq2 6906 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (SubGrp‘𝑔) = (SubGrp‘𝐺)) |
| 6 | | fvexd 6921 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Base‘𝑔) ∈ V) |
| 7 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
| 8 | | isnsg.1 |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
| 9 | 7, 8 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝑋) |
| 10 | | fvexd 6921 |
. . . . . . . 8
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → (+g‘𝑔) ∈ V) |
| 11 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → 𝑔 = 𝐺) |
| 12 | 11 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → (+g‘𝑔) = (+g‘𝐺)) |
| 13 | | isnsg.2 |
. . . . . . . . 9
⊢ + =
(+g‘𝐺) |
| 14 | 12, 13 | eqtr4di 2795 |
. . . . . . . 8
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → (+g‘𝑔) = + ) |
| 15 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → 𝑏 = 𝑋) |
| 16 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → 𝑝 = + ) |
| 17 | 16 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (𝑥𝑝𝑦) = (𝑥 + 𝑦)) |
| 18 | 17 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑥 + 𝑦) ∈ 𝑠)) |
| 19 | 16 | oveqd 7448 |
. . . . . . . . . . . 12
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (𝑦𝑝𝑥) = (𝑦 + 𝑥)) |
| 20 | 19 | eleq1d 2826 |
. . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → ((𝑦𝑝𝑥) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)) |
| 21 | 18, 20 | bibi12d 345 |
. . . . . . . . . 10
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
| 22 | 15, 21 | raleqbidv 3346 |
. . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
| 23 | 15, 22 | raleqbidv 3346 |
. . . . . . . 8
⊢ (((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) ∧ 𝑝 = + ) → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
| 24 | 10, 14, 23 | sbcied2 3833 |
. . . . . . 7
⊢ ((𝑔 = 𝐺 ∧ 𝑏 = 𝑋) → ([(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
| 25 | 6, 9, 24 | sbcied2 3833 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ([(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠))) |
| 26 | 5, 25 | rabeqbidv 3455 |
. . . . 5
⊢ (𝑔 = 𝐺 → {𝑠 ∈ (SubGrp‘𝑔) ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)} = {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)}) |
| 27 | | fvex 6919 |
. . . . . 6
⊢
(SubGrp‘𝐺)
∈ V |
| 28 | 27 | rabex 5339 |
. . . . 5
⊢ {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)} ∈ V |
| 29 | 26, 1, 28 | fvmpt 7016 |
. . . 4
⊢ (𝐺 ∈ Grp →
(NrmSGrp‘𝐺) = {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)}) |
| 30 | 29 | eleq2d 2827 |
. . 3
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (NrmSGrp‘𝐺) ↔ 𝑆 ∈ {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)})) |
| 31 | | eleq2 2830 |
. . . . . 6
⊢ (𝑠 = 𝑆 → ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑥 + 𝑦) ∈ 𝑆)) |
| 32 | | eleq2 2830 |
. . . . . 6
⊢ (𝑠 = 𝑆 → ((𝑦 + 𝑥) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑆)) |
| 33 | 31, 32 | bibi12d 345 |
. . . . 5
⊢ (𝑠 = 𝑆 → (((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠) ↔ ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) |
| 34 | 33 | 2ralbidv 3221 |
. . . 4
⊢ (𝑠 = 𝑆 → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) |
| 35 | 34 | elrab 3692 |
. . 3
⊢ (𝑆 ∈ {𝑠 ∈ (SubGrp‘𝐺) ∣ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)} ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) |
| 36 | 30, 35 | bitrdi 287 |
. 2
⊢ (𝐺 ∈ Grp → (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)))) |
| 37 | 2, 4, 36 | pm5.21nii 378 |
1
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆))) |