Step | Hyp | Ref
| Expression |
1 | | tgpt1.j |
. . 3
β’ π½ = (TopOpenβπΊ) |
2 | 1 | tgpt1 23492 |
. 2
β’ (πΊ β TopGrp β (π½ β Haus β π½ β Fre)) |
3 | | t1t0 22722 |
. . 3
β’ (π½ β Fre β π½ β Kol2) |
4 | | eleq2 2823 |
. . . . . . . . . . . 12
β’ (π€ = π§ β (π₯ β π€ β π₯ β π§)) |
5 | | eleq2 2823 |
. . . . . . . . . . . 12
β’ (π€ = π§ β (π¦ β π€ β π¦ β π§)) |
6 | 4, 5 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π€ = π§ β ((π₯ β π€ β π¦ β π€) β (π₯ β π§ β π¦ β π§))) |
7 | 6 | rspccva 3582 |
. . . . . . . . . 10
β’
((βπ€ β
π½ (π₯ β π€ β π¦ β π€) β§ π§ β π½) β (π₯ β π§ β π¦ β π§)) |
8 | 7 | adantll 713 |
. . . . . . . . 9
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ π§ β π½) β (π₯ β π§ β π¦ β π§)) |
9 | | tgpgrp 23452 |
. . . . . . . . . . . . . . 15
β’ (πΊ β TopGrp β πΊ β Grp) |
10 | 9 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β πΊ β Grp) |
11 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) |
12 | 11 | simprd 497 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β π¦ β (BaseβπΊ)) |
13 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(BaseβπΊ) =
(BaseβπΊ) |
14 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(0gβπΊ) = (0gβπΊ) |
15 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(-gβπΊ) = (-gβπΊ) |
16 | 13, 14, 15 | grpsubid 18839 |
. . . . . . . . . . . . . 14
β’ ((πΊ β Grp β§ π¦ β (BaseβπΊ)) β (π¦(-gβπΊ)π¦) = (0gβπΊ)) |
17 | 10, 12, 16 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β (π¦(-gβπΊ)π¦) = (0gβπΊ)) |
18 | 17 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β ((π¦(-gβπΊ)π¦)(+gβπΊ)π₯) = ((0gβπΊ)(+gβπΊ)π₯)) |
19 | 11 | simpld 496 |
. . . . . . . . . . . . 13
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β π₯ β (BaseβπΊ)) |
20 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(+gβπΊ) = (+gβπΊ) |
21 | 13, 20, 14 | grplid 18788 |
. . . . . . . . . . . . 13
β’ ((πΊ β Grp β§ π₯ β (BaseβπΊ)) β
((0gβπΊ)(+gβπΊ)π₯) = π₯) |
22 | 10, 19, 21 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β ((0gβπΊ)(+gβπΊ)π₯) = π₯) |
23 | 18, 22 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β ((π¦(-gβπΊ)π¦)(+gβπΊ)π₯) = π₯) |
24 | 13, 20, 15 | grpnpcan 18847 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ β Grp β§ π¦ β (BaseβπΊ) β§ π₯ β (BaseβπΊ)) β ((π¦(-gβπΊ)π₯)(+gβπΊ)π₯) = π¦) |
25 | 10, 12, 19, 24 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β ((π¦(-gβπΊ)π₯)(+gβπΊ)π₯) = π¦) |
26 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β π¦ β π§) |
27 | 25, 26 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β ((π¦(-gβπΊ)π₯)(+gβπΊ)π₯) β π§) |
28 | | oveq2 7369 |
. . . . . . . . . . . . . . . . 17
β’ (π = π₯ β (π¦(-gβπΊ)π) = (π¦(-gβπΊ)π₯)) |
29 | 28 | oveq1d 7376 |
. . . . . . . . . . . . . . . 16
β’ (π = π₯ β ((π¦(-gβπΊ)π)(+gβπΊ)π₯) = ((π¦(-gβπΊ)π₯)(+gβπΊ)π₯)) |
30 | 29 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π = π₯ β (((π¦(-gβπΊ)π)(+gβπΊ)π₯) β π§ β ((π¦(-gβπΊ)π₯)(+gβπΊ)π₯) β π§)) |
31 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) = (π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) |
32 | 31 | mptpreima 6194 |
. . . . . . . . . . . . . . 15
β’ (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§) = {π β (BaseβπΊ) β£ ((π¦(-gβπΊ)π)(+gβπΊ)π₯) β π§} |
33 | 30, 32 | elrab2 3652 |
. . . . . . . . . . . . . 14
β’ (π₯ β (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§) β (π₯ β (BaseβπΊ) β§ ((π¦(-gβπΊ)π₯)(+gβπΊ)π₯) β π§)) |
34 | 19, 27, 33 | sylanbrc 584 |
. . . . . . . . . . . . 13
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β π₯ β (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§)) |
35 | | eleq2 2823 |
. . . . . . . . . . . . . . 15
β’ (π€ = (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§) β (π₯ β π€ β π₯ β (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§))) |
36 | | eleq2 2823 |
. . . . . . . . . . . . . . 15
β’ (π€ = (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§) β (π¦ β π€ β π¦ β (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§))) |
37 | 35, 36 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π€ = (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§) β ((π₯ β π€ β π¦ β π€) β (π₯ β (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§) β π¦ β (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§)))) |
38 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β βπ€ β π½ (π₯ β π€ β π¦ β π€)) |
39 | | tgptmd 23453 |
. . . . . . . . . . . . . . . . 17
β’ (πΊ β TopGrp β πΊ β TopMnd) |
40 | 39 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β πΊ β TopMnd) |
41 | 1, 13 | tgptopon 23456 |
. . . . . . . . . . . . . . . . 17
β’ (πΊ β TopGrp β π½ β
(TopOnβ(BaseβπΊ))) |
42 | 41 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β π½ β (TopOnβ(BaseβπΊ))) |
43 | 42, 42, 12 | cnmptc 23036 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β (π β (BaseβπΊ) β¦ π¦) β (π½ Cn π½)) |
44 | 42 | cnmptid 23035 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β (π β (BaseβπΊ) β¦ π) β (π½ Cn π½)) |
45 | 1, 15 | tgpsubcn 23464 |
. . . . . . . . . . . . . . . . . 18
β’ (πΊ β TopGrp β
(-gβπΊ)
β ((π½
Γt π½) Cn
π½)) |
46 | 45 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β (-gβπΊ) β ((π½ Γt π½) Cn π½)) |
47 | 42, 43, 44, 46 | cnmpt12f 23040 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β (π β (BaseβπΊ) β¦ (π¦(-gβπΊ)π)) β (π½ Cn π½)) |
48 | 42, 42, 19 | cnmptc 23036 |
. . . . . . . . . . . . . . . 16
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β (π β (BaseβπΊ) β¦ π₯) β (π½ Cn π½)) |
49 | 1, 20, 40, 42, 47, 48 | cnmpt1plusg 23461 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β (π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β (π½ Cn π½)) |
50 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β π§ β π½) |
51 | | cnima 22639 |
. . . . . . . . . . . . . . 15
β’ (((π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β (π½ Cn π½) β§ π§ β π½) β (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§) β π½) |
52 | 49, 50, 51 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§) β π½) |
53 | 37, 38, 52 | rspcdva 3584 |
. . . . . . . . . . . . 13
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β (π₯ β (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§) β π¦ β (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§))) |
54 | 34, 53 | mpd 15 |
. . . . . . . . . . . 12
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β π¦ β (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§)) |
55 | | oveq2 7369 |
. . . . . . . . . . . . . . . 16
β’ (π = π¦ β (π¦(-gβπΊ)π) = (π¦(-gβπΊ)π¦)) |
56 | 55 | oveq1d 7376 |
. . . . . . . . . . . . . . 15
β’ (π = π¦ β ((π¦(-gβπΊ)π)(+gβπΊ)π₯) = ((π¦(-gβπΊ)π¦)(+gβπΊ)π₯)) |
57 | 56 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’ (π = π¦ β (((π¦(-gβπΊ)π)(+gβπΊ)π₯) β π§ β ((π¦(-gβπΊ)π¦)(+gβπΊ)π₯) β π§)) |
58 | 57, 32 | elrab2 3652 |
. . . . . . . . . . . . 13
β’ (π¦ β (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§) β (π¦ β (BaseβπΊ) β§ ((π¦(-gβπΊ)π¦)(+gβπΊ)π₯) β π§)) |
59 | 58 | simprbi 498 |
. . . . . . . . . . . 12
β’ (π¦ β (β‘(π β (BaseβπΊ) β¦ ((π¦(-gβπΊ)π)(+gβπΊ)π₯)) β π§) β ((π¦(-gβπΊ)π¦)(+gβπΊ)π₯) β π§) |
60 | 54, 59 | syl 17 |
. . . . . . . . . . 11
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β ((π¦(-gβπΊ)π¦)(+gβπΊ)π₯) β π§) |
61 | 23, 60 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ (π§ β π½ β§ π¦ β π§)) β π₯ β π§) |
62 | 61 | expr 458 |
. . . . . . . . 9
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ π§ β π½) β (π¦ β π§ β π₯ β π§)) |
63 | 8, 62 | impbid 211 |
. . . . . . . 8
β’ ((((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β§ π§ β π½) β (π₯ β π§ β π¦ β π§)) |
64 | 63 | ralrimiva 3140 |
. . . . . . 7
β’ (((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β§ βπ€ β π½ (π₯ β π€ β π¦ β π€)) β βπ§ β π½ (π₯ β π§ β π¦ β π§)) |
65 | 64 | ex 414 |
. . . . . 6
β’ ((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β (βπ€ β π½ (π₯ β π€ β π¦ β π€) β βπ§ β π½ (π₯ β π§ β π¦ β π§))) |
66 | 65 | imim1d 82 |
. . . . 5
β’ ((πΊ β TopGrp β§ (π₯ β (BaseβπΊ) β§ π¦ β (BaseβπΊ))) β ((βπ§ β π½ (π₯ β π§ β π¦ β π§) β π₯ = π¦) β (βπ€ β π½ (π₯ β π€ β π¦ β π€) β π₯ = π¦))) |
67 | 66 | ralimdvva 3198 |
. . . 4
β’ (πΊ β TopGrp β
(βπ₯ β
(BaseβπΊ)βπ¦ β (BaseβπΊ)(βπ§ β π½ (π₯ β π§ β π¦ β π§) β π₯ = π¦) β βπ₯ β (BaseβπΊ)βπ¦ β (BaseβπΊ)(βπ€ β π½ (π₯ β π€ β π¦ β π€) β π₯ = π¦))) |
68 | | ist0-2 22718 |
. . . . 5
β’ (π½ β
(TopOnβ(BaseβπΊ)) β (π½ β Kol2 β βπ₯ β (BaseβπΊ)βπ¦ β (BaseβπΊ)(βπ§ β π½ (π₯ β π§ β π¦ β π§) β π₯ = π¦))) |
69 | 41, 68 | syl 17 |
. . . 4
β’ (πΊ β TopGrp β (π½ β Kol2 β
βπ₯ β
(BaseβπΊ)βπ¦ β (BaseβπΊ)(βπ§ β π½ (π₯ β π§ β π¦ β π§) β π₯ = π¦))) |
70 | | ist1-2 22721 |
. . . . 5
β’ (π½ β
(TopOnβ(BaseβπΊ)) β (π½ β Fre β βπ₯ β (BaseβπΊ)βπ¦ β (BaseβπΊ)(βπ€ β π½ (π₯ β π€ β π¦ β π€) β π₯ = π¦))) |
71 | 41, 70 | syl 17 |
. . . 4
β’ (πΊ β TopGrp β (π½ β Fre β βπ₯ β (BaseβπΊ)βπ¦ β (BaseβπΊ)(βπ€ β π½ (π₯ β π€ β π¦ β π€) β π₯ = π¦))) |
72 | 67, 69, 71 | 3imtr4d 294 |
. . 3
β’ (πΊ β TopGrp β (π½ β Kol2 β π½ β Fre)) |
73 | 3, 72 | impbid2 225 |
. 2
β’ (πΊ β TopGrp β (π½ β Fre β π½ β Kol2)) |
74 | 2, 73 | bitrd 279 |
1
β’ (πΊ β TopGrp β (π½ β Haus β π½ β Kol2)) |