Step | Hyp | Ref
| Expression |
1 | | df-ima 5650 |
. . . . . 6
β’ ((π¦ β (BaseβπΊ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β ((intβπ½)βπ)) = ran ((π¦ β (BaseβπΊ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) βΎ ((intβπ½)βπ)) |
2 | | subgntr.h |
. . . . . . . . . . . 12
β’ π½ = (TopOpenβπΊ) |
3 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(BaseβπΊ) =
(BaseβπΊ) |
4 | 2, 3 | tgptopon 23456 |
. . . . . . . . . . 11
β’ (πΊ β TopGrp β π½ β
(TopOnβ(BaseβπΊ))) |
5 | 4 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β π½ β (TopOnβ(BaseβπΊ))) |
6 | 5 | adantr 482 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β π½ β (TopOnβ(BaseβπΊ))) |
7 | | topontop 22285 |
. . . . . . . . . . . 12
β’ (π½ β
(TopOnβ(BaseβπΊ)) β π½ β Top) |
8 | 5, 7 | syl 17 |
. . . . . . . . . . 11
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β π½ β Top) |
9 | 8 | adantr 482 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β π½ β Top) |
10 | | simpl2 1193 |
. . . . . . . . . . . 12
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β π β (SubGrpβπΊ)) |
11 | 3 | subgss 18937 |
. . . . . . . . . . . 12
β’ (π β (SubGrpβπΊ) β π β (BaseβπΊ)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β π β (BaseβπΊ)) |
13 | | toponuni 22286 |
. . . . . . . . . . . 12
β’ (π½ β
(TopOnβ(BaseβπΊ)) β (BaseβπΊ) = βͺ π½) |
14 | 6, 13 | syl 17 |
. . . . . . . . . . 11
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β (BaseβπΊ) = βͺ π½) |
15 | 12, 14 | sseqtrd 3988 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β π β βͺ π½) |
16 | | eqid 2733 |
. . . . . . . . . . 11
β’ βͺ π½ =
βͺ π½ |
17 | 16 | ntropn 22423 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π β βͺ π½)
β ((intβπ½)βπ) β π½) |
18 | 9, 15, 17 | syl2anc 585 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β ((intβπ½)βπ) β π½) |
19 | | toponss 22299 |
. . . . . . . . 9
β’ ((π½ β
(TopOnβ(BaseβπΊ)) β§ ((intβπ½)βπ) β π½) β ((intβπ½)βπ) β (BaseβπΊ)) |
20 | 6, 18, 19 | syl2anc 585 |
. . . . . . . 8
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β ((intβπ½)βπ) β (BaseβπΊ)) |
21 | 20 | resmptd 5998 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β ((π¦ β (BaseβπΊ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) βΎ ((intβπ½)βπ)) = (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦))) |
22 | 21 | rneqd 5897 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β ran ((π¦ β (BaseβπΊ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) βΎ ((intβπ½)βπ)) = ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦))) |
23 | 1, 22 | eqtrid 2785 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β ((π¦ β (BaseβπΊ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β ((intβπ½)βπ)) = ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦))) |
24 | | simpl1 1192 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β πΊ β TopGrp) |
25 | | simpr 486 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β π₯ β π) |
26 | 16 | ntrss2 22431 |
. . . . . . . . . . 11
β’ ((π½ β Top β§ π β βͺ π½)
β ((intβπ½)βπ) β π) |
27 | 9, 15, 26 | syl2anc 585 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β ((intβπ½)βπ) β π) |
28 | | simpl3 1194 |
. . . . . . . . . 10
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β π΄ β ((intβπ½)βπ)) |
29 | 27, 28 | sseldd 3949 |
. . . . . . . . 9
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β π΄ β π) |
30 | | eqid 2733 |
. . . . . . . . . 10
β’
(-gβπΊ) = (-gβπΊ) |
31 | 30 | subgsubcl 18947 |
. . . . . . . . 9
β’ ((π β (SubGrpβπΊ) β§ π₯ β π β§ π΄ β π) β (π₯(-gβπΊ)π΄) β π) |
32 | 10, 25, 29, 31 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β (π₯(-gβπΊ)π΄) β π) |
33 | 12, 32 | sseldd 3949 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β (π₯(-gβπΊ)π΄) β (BaseβπΊ)) |
34 | | eqid 2733 |
. . . . . . . 8
β’ (π¦ β (BaseβπΊ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) = (π¦ β (BaseβπΊ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) |
35 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπΊ) = (+gβπΊ) |
36 | 34, 3, 35, 2 | tgplacthmeo 23477 |
. . . . . . 7
β’ ((πΊ β TopGrp β§ (π₯(-gβπΊ)π΄) β (BaseβπΊ)) β (π¦ β (BaseβπΊ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β (π½Homeoπ½)) |
37 | 24, 33, 36 | syl2anc 585 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β (π¦ β (BaseβπΊ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β (π½Homeoπ½)) |
38 | | hmeoima 23139 |
. . . . . 6
β’ (((π¦ β (BaseβπΊ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β (π½Homeoπ½) β§ ((intβπ½)βπ) β π½) β ((π¦ β (BaseβπΊ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β ((intβπ½)βπ)) β π½) |
39 | 37, 18, 38 | syl2anc 585 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β ((π¦ β (BaseβπΊ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β ((intβπ½)βπ)) β π½) |
40 | 23, 39 | eqeltrrd 2835 |
. . . 4
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β π½) |
41 | | tgpgrp 23452 |
. . . . . . 7
β’ (πΊ β TopGrp β πΊ β Grp) |
42 | 24, 41 | syl 17 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β πΊ β Grp) |
43 | 11 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β π β (BaseβπΊ)) |
44 | 43 | sselda 3948 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β π₯ β (BaseβπΊ)) |
45 | 20, 28 | sseldd 3949 |
. . . . . 6
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β π΄ β (BaseβπΊ)) |
46 | 3, 35, 30 | grpnpcan 18847 |
. . . . . 6
β’ ((πΊ β Grp β§ π₯ β (BaseβπΊ) β§ π΄ β (BaseβπΊ)) β ((π₯(-gβπΊ)π΄)(+gβπΊ)π΄) = π₯) |
47 | 42, 44, 45, 46 | syl3anc 1372 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β ((π₯(-gβπΊ)π΄)(+gβπΊ)π΄) = π₯) |
48 | | ovex 7394 |
. . . . . 6
β’ ((π₯(-gβπΊ)π΄)(+gβπΊ)π΄) β V |
49 | | eqid 2733 |
. . . . . . 7
β’ (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) = (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) |
50 | | oveq2 7369 |
. . . . . . 7
β’ (π¦ = π΄ β ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦) = ((π₯(-gβπΊ)π΄)(+gβπΊ)π΄)) |
51 | 49, 50 | elrnmpt1s 5916 |
. . . . . 6
β’ ((π΄ β ((intβπ½)βπ) β§ ((π₯(-gβπΊ)π΄)(+gβπΊ)π΄) β V) β ((π₯(-gβπΊ)π΄)(+gβπΊ)π΄) β ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦))) |
52 | 28, 48, 51 | sylancl 587 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β ((π₯(-gβπΊ)π΄)(+gβπΊ)π΄) β ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦))) |
53 | 47, 52 | eqeltrrd 2835 |
. . . 4
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β π₯ β ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦))) |
54 | 10 | adantr 482 |
. . . . . . 7
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β§ π¦ β ((intβπ½)βπ)) β π β (SubGrpβπΊ)) |
55 | 32 | adantr 482 |
. . . . . . 7
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β§ π¦ β ((intβπ½)βπ)) β (π₯(-gβπΊ)π΄) β π) |
56 | 27 | sselda 3948 |
. . . . . . 7
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β§ π¦ β ((intβπ½)βπ)) β π¦ β π) |
57 | 35 | subgcl 18946 |
. . . . . . 7
β’ ((π β (SubGrpβπΊ) β§ (π₯(-gβπΊ)π΄) β π β§ π¦ β π) β ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦) β π) |
58 | 54, 55, 56, 57 | syl3anc 1372 |
. . . . . 6
β’ ((((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β§ π¦ β ((intβπ½)βπ)) β ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦) β π) |
59 | 58 | fmpttd 7067 |
. . . . 5
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)):((intβπ½)βπ)βΆπ) |
60 | 59 | frnd 6680 |
. . . 4
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β π) |
61 | | eleq2 2823 |
. . . . . 6
β’ (π’ = ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β (π₯ β π’ β π₯ β ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)))) |
62 | | sseq1 3973 |
. . . . . 6
β’ (π’ = ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β (π’ β π β ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β π)) |
63 | 61, 62 | anbi12d 632 |
. . . . 5
β’ (π’ = ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β ((π₯ β π’ β§ π’ β π) β (π₯ β ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β§ ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β π))) |
64 | 63 | rspcev 3583 |
. . . 4
β’ ((ran
(π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β π½ β§ (π₯ β ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β§ ran (π¦ β ((intβπ½)βπ) β¦ ((π₯(-gβπΊ)π΄)(+gβπΊ)π¦)) β π)) β βπ’ β π½ (π₯ β π’ β§ π’ β π)) |
65 | 40, 53, 60, 64 | syl12anc 836 |
. . 3
β’ (((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β§ π₯ β π) β βπ’ β π½ (π₯ β π’ β§ π’ β π)) |
66 | 65 | ralrimiva 3140 |
. 2
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β βπ₯ β π βπ’ β π½ (π₯ β π’ β§ π’ β π)) |
67 | | eltop2 22348 |
. . 3
β’ (π½ β Top β (π β π½ β βπ₯ β π βπ’ β π½ (π₯ β π’ β§ π’ β π))) |
68 | 8, 67 | syl 17 |
. 2
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β (π β π½ β βπ₯ β π βπ’ β π½ (π₯ β π’ β§ π’ β π))) |
69 | 66, 68 | mpbird 257 |
1
β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β π β π½) |