Step | Hyp | Ref
| Expression |
1 | | subgngp.h |
. . . 4
β’ π» = (πΊ βΎs π΄) |
2 | 1 | subggrp 18939 |
. . 3
β’ (π΄ β (SubGrpβπΊ) β π» β Grp) |
3 | 2 | adantl 483 |
. 2
β’ ((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β π» β Grp) |
4 | | ngpms 23979 |
. . . 4
β’ (πΊ β NrmGrp β πΊ β MetSp) |
5 | | ressms 23905 |
. . . 4
β’ ((πΊ β MetSp β§ π΄ β (SubGrpβπΊ)) β (πΊ βΎs π΄) β MetSp) |
6 | 4, 5 | sylan 581 |
. . 3
β’ ((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β (πΊ βΎs π΄) β MetSp) |
7 | 1, 6 | eqeltrid 2838 |
. 2
β’ ((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β π» β MetSp) |
8 | | simplr 768 |
. . . . . 6
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β π΄ β (SubGrpβπΊ)) |
9 | | simprl 770 |
. . . . . . 7
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β π₯ β (Baseβπ»)) |
10 | 1 | subgbas 18940 |
. . . . . . . 8
β’ (π΄ β (SubGrpβπΊ) β π΄ = (Baseβπ»)) |
11 | 10 | ad2antlr 726 |
. . . . . . 7
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β π΄ = (Baseβπ»)) |
12 | 9, 11 | eleqtrrd 2837 |
. . . . . 6
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β π₯ β π΄) |
13 | | simprr 772 |
. . . . . . 7
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β π¦ β (Baseβπ»)) |
14 | 13, 11 | eleqtrrd 2837 |
. . . . . 6
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β π¦ β π΄) |
15 | | eqid 2733 |
. . . . . . 7
β’
(-gβπΊ) = (-gβπΊ) |
16 | | eqid 2733 |
. . . . . . 7
β’
(-gβπ») = (-gβπ») |
17 | 15, 1, 16 | subgsub 18948 |
. . . . . 6
β’ ((π΄ β (SubGrpβπΊ) β§ π₯ β π΄ β§ π¦ β π΄) β (π₯(-gβπΊ)π¦) = (π₯(-gβπ»)π¦)) |
18 | 8, 12, 14, 17 | syl3anc 1372 |
. . . . 5
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β (π₯(-gβπΊ)π¦) = (π₯(-gβπ»)π¦)) |
19 | 18 | fveq2d 6850 |
. . . 4
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β ((normβπΊ)β(π₯(-gβπΊ)π¦)) = ((normβπΊ)β(π₯(-gβπ»)π¦))) |
20 | | eqid 2733 |
. . . . . . . 8
β’
(distβπΊ) =
(distβπΊ) |
21 | 1, 20 | ressds 17299 |
. . . . . . 7
β’ (π΄ β (SubGrpβπΊ) β (distβπΊ) = (distβπ»)) |
22 | 21 | ad2antlr 726 |
. . . . . 6
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β (distβπΊ) = (distβπ»)) |
23 | 22 | oveqd 7378 |
. . . . 5
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β (π₯(distβπΊ)π¦) = (π₯(distβπ»)π¦)) |
24 | | simpll 766 |
. . . . . 6
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β πΊ β NrmGrp) |
25 | | eqid 2733 |
. . . . . . . . 9
β’
(BaseβπΊ) =
(BaseβπΊ) |
26 | 25 | subgss 18937 |
. . . . . . . 8
β’ (π΄ β (SubGrpβπΊ) β π΄ β (BaseβπΊ)) |
27 | 26 | ad2antlr 726 |
. . . . . . 7
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β π΄ β (BaseβπΊ)) |
28 | 27, 12 | sseldd 3949 |
. . . . . 6
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β π₯ β (BaseβπΊ)) |
29 | 27, 14 | sseldd 3949 |
. . . . . 6
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β π¦ β (BaseβπΊ)) |
30 | | eqid 2733 |
. . . . . . 7
β’
(normβπΊ) =
(normβπΊ) |
31 | 30, 25, 15, 20 | ngpds 23983 |
. . . . . 6
β’ ((πΊ β NrmGrp β§ π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ)) β (π₯(distβπΊ)π¦) = ((normβπΊ)β(π₯(-gβπΊ)π¦))) |
32 | 24, 28, 29, 31 | syl3anc 1372 |
. . . . 5
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β (π₯(distβπΊ)π¦) = ((normβπΊ)β(π₯(-gβπΊ)π¦))) |
33 | 23, 32 | eqtr3d 2775 |
. . . 4
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β (π₯(distβπ»)π¦) = ((normβπΊ)β(π₯(-gβπΊ)π¦))) |
34 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ») =
(Baseβπ») |
35 | 34, 16 | grpsubcl 18835 |
. . . . . . . 8
β’ ((π» β Grp β§ π₯ β (Baseβπ») β§ π¦ β (Baseβπ»)) β (π₯(-gβπ»)π¦) β (Baseβπ»)) |
36 | 35 | 3expb 1121 |
. . . . . . 7
β’ ((π» β Grp β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β (π₯(-gβπ»)π¦) β (Baseβπ»)) |
37 | 3, 36 | sylan 581 |
. . . . . 6
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β (π₯(-gβπ»)π¦) β (Baseβπ»)) |
38 | 37, 11 | eleqtrrd 2837 |
. . . . 5
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β (π₯(-gβπ»)π¦) β π΄) |
39 | | eqid 2733 |
. . . . . 6
β’
(normβπ») =
(normβπ») |
40 | 1, 30, 39 | subgnm2 24013 |
. . . . 5
β’ ((π΄ β (SubGrpβπΊ) β§ (π₯(-gβπ»)π¦) β π΄) β ((normβπ»)β(π₯(-gβπ»)π¦)) = ((normβπΊ)β(π₯(-gβπ»)π¦))) |
41 | 8, 38, 40 | syl2anc 585 |
. . . 4
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β ((normβπ»)β(π₯(-gβπ»)π¦)) = ((normβπΊ)β(π₯(-gβπ»)π¦))) |
42 | 19, 33, 41 | 3eqtr4d 2783 |
. . 3
β’ (((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β§ (π₯ β (Baseβπ») β§ π¦ β (Baseβπ»))) β (π₯(distβπ»)π¦) = ((normβπ»)β(π₯(-gβπ»)π¦))) |
43 | 42 | ralrimivva 3194 |
. 2
β’ ((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β βπ₯ β (Baseβπ»)βπ¦ β (Baseβπ»)(π₯(distβπ»)π¦) = ((normβπ»)β(π₯(-gβπ»)π¦))) |
44 | | eqid 2733 |
. . 3
β’
(distβπ») =
(distβπ») |
45 | 39, 16, 44, 34 | isngp3 23977 |
. 2
β’ (π» β NrmGrp β (π» β Grp β§ π» β MetSp β§
βπ₯ β
(Baseβπ»)βπ¦ β (Baseβπ»)(π₯(distβπ»)π¦) = ((normβπ»)β(π₯(-gβπ»)π¦)))) |
46 | 3, 7, 43, 45 | syl3anbrc 1344 |
1
β’ ((πΊ β NrmGrp β§ π΄ β (SubGrpβπΊ)) β π» β NrmGrp) |