| Step | Hyp | Ref
| Expression |
| 1 | | subgngp.h |
. . . 4
⊢ 𝐻 = (𝐺 ↾s 𝐴) |
| 2 | 1 | subggrp 19147 |
. . 3
⊢ (𝐴 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) |
| 3 | 2 | adantl 481 |
. 2
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Grp) |
| 4 | | ngpms 24613 |
. . . 4
⊢ (𝐺 ∈ NrmGrp → 𝐺 ∈ MetSp) |
| 5 | | ressms 24539 |
. . . 4
⊢ ((𝐺 ∈ MetSp ∧ 𝐴 ∈ (SubGrp‘𝐺)) → (𝐺 ↾s 𝐴) ∈ MetSp) |
| 6 | 4, 5 | sylan 580 |
. . 3
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) → (𝐺 ↾s 𝐴) ∈ MetSp) |
| 7 | 1, 6 | eqeltrid 2845 |
. 2
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ MetSp) |
| 8 | | simplr 769 |
. . . . . 6
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → 𝐴 ∈ (SubGrp‘𝐺)) |
| 9 | | simprl 771 |
. . . . . . 7
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → 𝑥 ∈ (Base‘𝐻)) |
| 10 | 1 | subgbas 19148 |
. . . . . . . 8
⊢ (𝐴 ∈ (SubGrp‘𝐺) → 𝐴 = (Base‘𝐻)) |
| 11 | 10 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → 𝐴 = (Base‘𝐻)) |
| 12 | 9, 11 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → 𝑥 ∈ 𝐴) |
| 13 | | simprr 773 |
. . . . . . 7
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → 𝑦 ∈ (Base‘𝐻)) |
| 14 | 13, 11 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → 𝑦 ∈ 𝐴) |
| 15 | | eqid 2737 |
. . . . . . 7
⊢
(-g‘𝐺) = (-g‘𝐺) |
| 16 | | eqid 2737 |
. . . . . . 7
⊢
(-g‘𝐻) = (-g‘𝐻) |
| 17 | 15, 1, 16 | subgsub 19156 |
. . . . . 6
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥(-g‘𝐺)𝑦) = (𝑥(-g‘𝐻)𝑦)) |
| 18 | 8, 12, 14, 17 | syl3anc 1373 |
. . . . 5
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → (𝑥(-g‘𝐺)𝑦) = (𝑥(-g‘𝐻)𝑦)) |
| 19 | 18 | fveq2d 6910 |
. . . 4
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦)) = ((norm‘𝐺)‘(𝑥(-g‘𝐻)𝑦))) |
| 20 | | eqid 2737 |
. . . . . . . 8
⊢
(dist‘𝐺) =
(dist‘𝐺) |
| 21 | 1, 20 | ressds 17454 |
. . . . . . 7
⊢ (𝐴 ∈ (SubGrp‘𝐺) → (dist‘𝐺) = (dist‘𝐻)) |
| 22 | 21 | ad2antlr 727 |
. . . . . 6
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → (dist‘𝐺) = (dist‘𝐻)) |
| 23 | 22 | oveqd 7448 |
. . . . 5
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → (𝑥(dist‘𝐺)𝑦) = (𝑥(dist‘𝐻)𝑦)) |
| 24 | | simpll 767 |
. . . . . 6
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → 𝐺 ∈ NrmGrp) |
| 25 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 26 | 25 | subgss 19145 |
. . . . . . . 8
⊢ (𝐴 ∈ (SubGrp‘𝐺) → 𝐴 ⊆ (Base‘𝐺)) |
| 27 | 26 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → 𝐴 ⊆ (Base‘𝐺)) |
| 28 | 27, 12 | sseldd 3984 |
. . . . . 6
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → 𝑥 ∈ (Base‘𝐺)) |
| 29 | 27, 14 | sseldd 3984 |
. . . . . 6
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → 𝑦 ∈ (Base‘𝐺)) |
| 30 | | eqid 2737 |
. . . . . . 7
⊢
(norm‘𝐺) =
(norm‘𝐺) |
| 31 | 30, 25, 15, 20 | ngpds 24617 |
. . . . . 6
⊢ ((𝐺 ∈ NrmGrp ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(dist‘𝐺)𝑦) = ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦))) |
| 32 | 24, 28, 29, 31 | syl3anc 1373 |
. . . . 5
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → (𝑥(dist‘𝐺)𝑦) = ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦))) |
| 33 | 23, 32 | eqtr3d 2779 |
. . . 4
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → (𝑥(dist‘𝐻)𝑦) = ((norm‘𝐺)‘(𝑥(-g‘𝐺)𝑦))) |
| 34 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝐻) =
(Base‘𝐻) |
| 35 | 34, 16 | grpsubcl 19038 |
. . . . . . . 8
⊢ ((𝐻 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻)) → (𝑥(-g‘𝐻)𝑦) ∈ (Base‘𝐻)) |
| 36 | 35 | 3expb 1121 |
. . . . . . 7
⊢ ((𝐻 ∈ Grp ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → (𝑥(-g‘𝐻)𝑦) ∈ (Base‘𝐻)) |
| 37 | 3, 36 | sylan 580 |
. . . . . 6
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → (𝑥(-g‘𝐻)𝑦) ∈ (Base‘𝐻)) |
| 38 | 37, 11 | eleqtrrd 2844 |
. . . . 5
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → (𝑥(-g‘𝐻)𝑦) ∈ 𝐴) |
| 39 | | eqid 2737 |
. . . . . 6
⊢
(norm‘𝐻) =
(norm‘𝐻) |
| 40 | 1, 30, 39 | subgnm2 24647 |
. . . . 5
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ (𝑥(-g‘𝐻)𝑦) ∈ 𝐴) → ((norm‘𝐻)‘(𝑥(-g‘𝐻)𝑦)) = ((norm‘𝐺)‘(𝑥(-g‘𝐻)𝑦))) |
| 41 | 8, 38, 40 | syl2anc 584 |
. . . 4
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → ((norm‘𝐻)‘(𝑥(-g‘𝐻)𝑦)) = ((norm‘𝐺)‘(𝑥(-g‘𝐻)𝑦))) |
| 42 | 19, 33, 41 | 3eqtr4d 2787 |
. . 3
⊢ (((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) ∧ (𝑥 ∈ (Base‘𝐻) ∧ 𝑦 ∈ (Base‘𝐻))) → (𝑥(dist‘𝐻)𝑦) = ((norm‘𝐻)‘(𝑥(-g‘𝐻)𝑦))) |
| 43 | 42 | ralrimivva 3202 |
. 2
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) → ∀𝑥 ∈ (Base‘𝐻)∀𝑦 ∈ (Base‘𝐻)(𝑥(dist‘𝐻)𝑦) = ((norm‘𝐻)‘(𝑥(-g‘𝐻)𝑦))) |
| 44 | | eqid 2737 |
. . 3
⊢
(dist‘𝐻) =
(dist‘𝐻) |
| 45 | 39, 16, 44, 34 | isngp3 24611 |
. 2
⊢ (𝐻 ∈ NrmGrp ↔ (𝐻 ∈ Grp ∧ 𝐻 ∈ MetSp ∧
∀𝑥 ∈
(Base‘𝐻)∀𝑦 ∈ (Base‘𝐻)(𝑥(dist‘𝐻)𝑦) = ((norm‘𝐻)‘(𝑥(-g‘𝐻)𝑦)))) |
| 46 | 3, 7, 43, 45 | syl3anbrc 1344 |
1
⊢ ((𝐺 ∈ NrmGrp ∧ 𝐴 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ NrmGrp) |