Step | Hyp | Ref
| Expression |
1 | | nsgsubg 19032 |
. . 3
β’ (π β (NrmSGrpβπΊ) β π β (SubGrpβπΊ)) |
2 | | subgntr.h |
. . . 4
β’ π½ = (TopOpenβπΊ) |
3 | 2 | clssubg 23604 |
. . 3
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β ((clsβπ½)βπ) β (SubGrpβπΊ)) |
4 | 1, 3 | sylan2 593 |
. 2
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β ((clsβπ½)βπ) β (SubGrpβπΊ)) |
5 | | df-ima 5688 |
. . . . . . 7
β’ ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β ((clsβπ½)βπ)) = ran ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) βΎ ((clsβπ½)βπ)) |
6 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(BaseβπΊ) =
(BaseβπΊ) |
7 | 2, 6 | tgptopon 23577 |
. . . . . . . . . . . . 13
β’ (πΊ β TopGrp β π½ β
(TopOnβ(BaseβπΊ))) |
8 | 7 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β π½ β (TopOnβ(BaseβπΊ))) |
9 | | topontop 22406 |
. . . . . . . . . . . 12
β’ (π½ β
(TopOnβ(BaseβπΊ)) β π½ β Top) |
10 | 8, 9 | syl 17 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β π½ β Top) |
11 | 1 | ad2antlr 725 |
. . . . . . . . . . . . 13
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β π β (SubGrpβπΊ)) |
12 | 6 | subgss 19001 |
. . . . . . . . . . . . 13
β’ (π β (SubGrpβπΊ) β π β (BaseβπΊ)) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . 12
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β π β (BaseβπΊ)) |
14 | | toponuni 22407 |
. . . . . . . . . . . . 13
β’ (π½ β
(TopOnβ(BaseβπΊ)) β (BaseβπΊ) = βͺ π½) |
15 | 8, 14 | syl 17 |
. . . . . . . . . . . 12
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β (BaseβπΊ) = βͺ π½) |
16 | 13, 15 | sseqtrd 4021 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β π β βͺ π½) |
17 | | eqid 2732 |
. . . . . . . . . . . 12
β’ βͺ π½ =
βͺ π½ |
18 | 17 | clsss3 22554 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β βͺ π½)
β ((clsβπ½)βπ) β βͺ π½) |
19 | 10, 16, 18 | syl2anc 584 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ((clsβπ½)βπ) β βͺ π½) |
20 | 19, 15 | sseqtrrd 4022 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ((clsβπ½)βπ) β (BaseβπΊ)) |
21 | 20 | resmptd 6038 |
. . . . . . . 8
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) βΎ ((clsβπ½)βπ)) = (π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯))) |
22 | 21 | rneqd 5935 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ran ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) βΎ ((clsβπ½)βπ)) = ran (π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯))) |
23 | 5, 22 | eqtrid 2784 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β ((clsβπ½)βπ)) = ran (π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯))) |
24 | | eqid 2732 |
. . . . . . . . . 10
β’
(+gβπΊ) = (+gβπΊ) |
25 | | tgptmd 23574 |
. . . . . . . . . . 11
β’ (πΊ β TopGrp β πΊ β TopMnd) |
26 | 25 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β πΊ β TopMnd) |
27 | | simpr 485 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β π₯ β (BaseβπΊ)) |
28 | 8, 8, 27 | cnmptc 23157 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β (π¦ β (BaseβπΊ) β¦ π₯) β (π½ Cn π½)) |
29 | 8 | cnmptid 23156 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β (π¦ β (BaseβπΊ) β¦ π¦) β (π½ Cn π½)) |
30 | 2, 24, 26, 8, 28, 29 | cnmpt1plusg 23582 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β (π¦ β (BaseβπΊ) β¦ (π₯(+gβπΊ)π¦)) β (π½ Cn π½)) |
31 | | eqid 2732 |
. . . . . . . . . . 11
β’
(-gβπΊ) = (-gβπΊ) |
32 | 2, 31 | tgpsubcn 23585 |
. . . . . . . . . 10
β’ (πΊ β TopGrp β
(-gβπΊ)
β ((π½
Γt π½) Cn
π½)) |
33 | 32 | ad2antrr 724 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β (-gβπΊ) β ((π½ Γt π½) Cn π½)) |
34 | 8, 30, 28, 33 | cnmpt12f 23161 |
. . . . . . . 8
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β (π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β (π½ Cn π½)) |
35 | 17 | cnclsi 22767 |
. . . . . . . 8
β’ (((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β (π½ Cn π½) β§ π β βͺ π½) β ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β ((clsβπ½)βπ)) β ((clsβπ½)β((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β π))) |
36 | 34, 16, 35 | syl2anc 584 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β ((clsβπ½)βπ)) β ((clsβπ½)β((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β π))) |
37 | | df-ima 5688 |
. . . . . . . . . 10
β’ ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β π) = ran ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) βΎ π) |
38 | 13 | resmptd 6038 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) βΎ π) = (π¦ β π β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯))) |
39 | 38 | rneqd 5935 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ran ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) βΎ π) = ran (π¦ β π β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯))) |
40 | 37, 39 | eqtrid 2784 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β π) = ran (π¦ β π β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯))) |
41 | 6, 24, 31 | nsgconj 19033 |
. . . . . . . . . . . 12
β’ ((π β (NrmSGrpβπΊ) β§ π₯ β (BaseβπΊ) β§ π¦ β π) β ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯) β π) |
42 | 41 | ad4ant234 1175 |
. . . . . . . . . . 11
β’ ((((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β§ π¦ β π) β ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯) β π) |
43 | 42 | fmpttd 7111 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β (π¦ β π β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)):πβΆπ) |
44 | 43 | frnd 6722 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ran (π¦ β π β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β π) |
45 | 40, 44 | eqsstrd 4019 |
. . . . . . . 8
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β π) β π) |
46 | 17 | clsss 22549 |
. . . . . . . 8
β’ ((π½ β Top β§ π β βͺ π½
β§ ((π¦ β
(BaseβπΊ) β¦
((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β π) β π) β ((clsβπ½)β((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β π)) β ((clsβπ½)βπ)) |
47 | 10, 16, 45, 46 | syl3anc 1371 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ((clsβπ½)β((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β π)) β ((clsβπ½)βπ)) |
48 | 36, 47 | sstrd 3991 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ((π¦ β (BaseβπΊ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β ((clsβπ½)βπ)) β ((clsβπ½)βπ)) |
49 | 23, 48 | eqsstrrd 4020 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β ran (π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β ((clsβπ½)βπ)) |
50 | | ovex 7438 |
. . . . . . 7
β’ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯) β V |
51 | | eqid 2732 |
. . . . . . 7
β’ (π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) = (π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) |
52 | 50, 51 | fnmpti 6690 |
. . . . . 6
β’ (π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) Fn ((clsβπ½)βπ) |
53 | | df-f 6544 |
. . . . . 6
β’ ((π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)):((clsβπ½)βπ)βΆ((clsβπ½)βπ) β ((π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) Fn ((clsβπ½)βπ) β§ ran (π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β ((clsβπ½)βπ))) |
54 | 52, 53 | mpbiran 707 |
. . . . 5
β’ ((π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)):((clsβπ½)βπ)βΆ((clsβπ½)βπ) β ran (π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)) β ((clsβπ½)βπ)) |
55 | 49, 54 | sylibr 233 |
. . . 4
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β (π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)):((clsβπ½)βπ)βΆ((clsβπ½)βπ)) |
56 | 51 | fmpt 7106 |
. . . 4
β’
(βπ¦ β
((clsβπ½)βπ)((π₯(+gβπΊ)π¦)(-gβπΊ)π₯) β ((clsβπ½)βπ) β (π¦ β ((clsβπ½)βπ) β¦ ((π₯(+gβπΊ)π¦)(-gβπΊ)π₯)):((clsβπ½)βπ)βΆ((clsβπ½)βπ)) |
57 | 55, 56 | sylibr 233 |
. . 3
β’ (((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β§ π₯ β (BaseβπΊ)) β βπ¦ β ((clsβπ½)βπ)((π₯(+gβπΊ)π¦)(-gβπΊ)π₯) β ((clsβπ½)βπ)) |
58 | 57 | ralrimiva 3146 |
. 2
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β βπ₯ β (BaseβπΊ)βπ¦ β ((clsβπ½)βπ)((π₯(+gβπΊ)π¦)(-gβπΊ)π₯) β ((clsβπ½)βπ)) |
59 | 6, 24, 31 | isnsg3 19034 |
. 2
β’
(((clsβπ½)βπ) β (NrmSGrpβπΊ) β (((clsβπ½)βπ) β (SubGrpβπΊ) β§ βπ₯ β (BaseβπΊ)βπ¦ β ((clsβπ½)βπ)((π₯(+gβπΊ)π¦)(-gβπΊ)π₯) β ((clsβπ½)βπ))) |
60 | 4, 58, 59 | sylanbrc 583 |
1
β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β ((clsβπ½)βπ) β (NrmSGrpβπΊ)) |