Step | Hyp | Ref
| Expression |
1 | | prdstgpd.y |
. . 3
β’ π = (πXsπ
) |
2 | | prdstgpd.i |
. . 3
β’ (π β πΌ β π) |
3 | | prdstgpd.s |
. . 3
β’ (π β π β π) |
4 | | prdstgpd.r |
. . . 4
β’ (π β π
:πΌβΆTopGrp) |
5 | | tgpgrp 23452 |
. . . . 5
β’ (π₯ β TopGrp β π₯ β Grp) |
6 | 5 | ssriv 3952 |
. . . 4
β’ TopGrp
β Grp |
7 | | fss 6689 |
. . . 4
β’ ((π
:πΌβΆTopGrp β§ TopGrp β Grp)
β π
:πΌβΆGrp) |
8 | 4, 6, 7 | sylancl 587 |
. . 3
β’ (π β π
:πΌβΆGrp) |
9 | 1, 2, 3, 8 | prdsgrpd 18865 |
. 2
β’ (π β π β Grp) |
10 | | tgptmd 23453 |
. . . . 5
β’ (π₯ β TopGrp β π₯ β TopMnd) |
11 | 10 | ssriv 3952 |
. . . 4
β’ TopGrp
β TopMnd |
12 | | fss 6689 |
. . . 4
β’ ((π
:πΌβΆTopGrp β§ TopGrp β TopMnd)
β π
:πΌβΆTopMnd) |
13 | 4, 11, 12 | sylancl 587 |
. . 3
β’ (π β π
:πΌβΆTopMnd) |
14 | 1, 2, 3, 13 | prdstmdd 23498 |
. 2
β’ (π β π β TopMnd) |
15 | | eqid 2733 |
. . . 4
β’
(βtβ(TopOpen β π
)) = (βtβ(TopOpen
β π
)) |
16 | | eqid 2733 |
. . . . . 6
β’
(TopOpenβπ) =
(TopOpenβπ) |
17 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
18 | 16, 17 | tmdtopon 23455 |
. . . . 5
β’ (π β TopMnd β
(TopOpenβπ) β
(TopOnβ(Baseβπ))) |
19 | 14, 18 | syl 17 |
. . . 4
β’ (π β (TopOpenβπ) β
(TopOnβ(Baseβπ))) |
20 | | topnfn 17315 |
. . . . . 6
β’ TopOpen
Fn V |
21 | 4 | ffnd 6673 |
. . . . . . 7
β’ (π β π
Fn πΌ) |
22 | | dffn2 6674 |
. . . . . . 7
β’ (π
Fn πΌ β π
:πΌβΆV) |
23 | 21, 22 | sylib 217 |
. . . . . 6
β’ (π β π
:πΌβΆV) |
24 | | fnfco 6711 |
. . . . . 6
β’ ((TopOpen
Fn V β§ π
:πΌβΆV) β (TopOpen
β π
) Fn πΌ) |
25 | 20, 23, 24 | sylancr 588 |
. . . . 5
β’ (π β (TopOpen β π
) Fn πΌ) |
26 | | fvco3 6944 |
. . . . . . . 8
β’ ((π
:πΌβΆTopGrp β§ π¦ β πΌ) β ((TopOpen β π
)βπ¦) = (TopOpenβ(π
βπ¦))) |
27 | 4, 26 | sylan 581 |
. . . . . . 7
β’ ((π β§ π¦ β πΌ) β ((TopOpen β π
)βπ¦) = (TopOpenβ(π
βπ¦))) |
28 | 4 | ffvelcdmda 7039 |
. . . . . . . 8
β’ ((π β§ π¦ β πΌ) β (π
βπ¦) β TopGrp) |
29 | | eqid 2733 |
. . . . . . . . 9
β’
(TopOpenβ(π
βπ¦)) = (TopOpenβ(π
βπ¦)) |
30 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβ(π
βπ¦)) = (Baseβ(π
βπ¦)) |
31 | 29, 30 | tgptopon 23456 |
. . . . . . . 8
β’ ((π
βπ¦) β TopGrp β (TopOpenβ(π
βπ¦)) β (TopOnβ(Baseβ(π
βπ¦)))) |
32 | | topontop 22285 |
. . . . . . . 8
β’
((TopOpenβ(π
βπ¦)) β (TopOnβ(Baseβ(π
βπ¦))) β (TopOpenβ(π
βπ¦)) β Top) |
33 | 28, 31, 32 | 3syl 18 |
. . . . . . 7
β’ ((π β§ π¦ β πΌ) β (TopOpenβ(π
βπ¦)) β Top) |
34 | 27, 33 | eqeltrd 2834 |
. . . . . 6
β’ ((π β§ π¦ β πΌ) β ((TopOpen β π
)βπ¦) β Top) |
35 | 34 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ¦ β πΌ ((TopOpen β π
)βπ¦) β Top) |
36 | | ffnfv 7070 |
. . . . 5
β’ ((TopOpen
β π
):πΌβΆTop β ((TopOpen
β π
) Fn πΌ β§ βπ¦ β πΌ ((TopOpen β π
)βπ¦) β Top)) |
37 | 25, 35, 36 | sylanbrc 584 |
. . . 4
β’ (π β (TopOpen β π
):πΌβΆTop) |
38 | 19 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β πΌ) β (TopOpenβπ) β (TopOnβ(Baseβπ))) |
39 | 1, 3, 2, 21, 16 | prdstopn 23002 |
. . . . . . . . . . . 12
β’ (π β (TopOpenβπ) =
(βtβ(TopOpen β π
))) |
40 | 39 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β πΌ) β (TopOpenβπ) = (βtβ(TopOpen
β π
))) |
41 | 40 | eqcomd 2739 |
. . . . . . . . . 10
β’ ((π β§ π¦ β πΌ) β (βtβ(TopOpen
β π
)) =
(TopOpenβπ)) |
42 | 41, 38 | eqeltrd 2834 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΌ) β (βtβ(TopOpen
β π
)) β
(TopOnβ(Baseβπ))) |
43 | | toponuni 22286 |
. . . . . . . . 9
β’
((βtβ(TopOpen β π
)) β (TopOnβ(Baseβπ)) β (Baseβπ) = βͺ
(βtβ(TopOpen β π
))) |
44 | | mpteq1 5202 |
. . . . . . . . 9
β’
((Baseβπ) =
βͺ (βtβ(TopOpen β π
)) β (π₯ β (Baseβπ) β¦ (π₯βπ¦)) = (π₯ β βͺ
(βtβ(TopOpen β π
)) β¦ (π₯βπ¦))) |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ π¦ β πΌ) β (π₯ β (Baseβπ) β¦ (π₯βπ¦)) = (π₯ β βͺ
(βtβ(TopOpen β π
)) β¦ (π₯βπ¦))) |
46 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΌ) β πΌ β π) |
47 | 37 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΌ) β (TopOpen β π
):πΌβΆTop) |
48 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π¦ β πΌ) β π¦ β πΌ) |
49 | | eqid 2733 |
. . . . . . . . . 10
β’ βͺ (βtβ(TopOpen β π
)) = βͺ (βtβ(TopOpen β π
)) |
50 | 49, 15 | ptpjcn 22985 |
. . . . . . . . 9
β’ ((πΌ β π β§ (TopOpen β π
):πΌβΆTop β§ π¦ β πΌ) β (π₯ β βͺ
(βtβ(TopOpen β π
)) β¦ (π₯βπ¦)) β ((βtβ(TopOpen
β π
)) Cn ((TopOpen
β π
)βπ¦))) |
51 | 46, 47, 48, 50 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π¦ β πΌ) β (π₯ β βͺ
(βtβ(TopOpen β π
)) β¦ (π₯βπ¦)) β ((βtβ(TopOpen
β π
)) Cn ((TopOpen
β π
)βπ¦))) |
52 | 45, 51 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β§ π¦ β πΌ) β (π₯ β (Baseβπ) β¦ (π₯βπ¦)) β ((βtβ(TopOpen
β π
)) Cn ((TopOpen
β π
)βπ¦))) |
53 | 41, 27 | oveq12d 7379 |
. . . . . . 7
β’ ((π β§ π¦ β πΌ) β ((βtβ(TopOpen
β π
)) Cn ((TopOpen
β π
)βπ¦)) = ((TopOpenβπ) Cn (TopOpenβ(π
βπ¦)))) |
54 | 52, 53 | eleqtrd 2836 |
. . . . . 6
β’ ((π β§ π¦ β πΌ) β (π₯ β (Baseβπ) β¦ (π₯βπ¦)) β ((TopOpenβπ) Cn (TopOpenβ(π
βπ¦)))) |
55 | | eqid 2733 |
. . . . . . . 8
β’
(invgβ(π
βπ¦)) = (invgβ(π
βπ¦)) |
56 | 29, 55 | tgpinv 23459 |
. . . . . . 7
β’ ((π
βπ¦) β TopGrp β
(invgβ(π
βπ¦)) β ((TopOpenβ(π
βπ¦)) Cn (TopOpenβ(π
βπ¦)))) |
57 | 28, 56 | syl 17 |
. . . . . 6
β’ ((π β§ π¦ β πΌ) β (invgβ(π
βπ¦)) β ((TopOpenβ(π
βπ¦)) Cn (TopOpenβ(π
βπ¦)))) |
58 | 38, 54, 57 | cnmpt11f 23038 |
. . . . 5
β’ ((π β§ π¦ β πΌ) β (π₯ β (Baseβπ) β¦ ((invgβ(π
βπ¦))β(π₯βπ¦))) β ((TopOpenβπ) Cn (TopOpenβ(π
βπ¦)))) |
59 | 27 | oveq2d 7377 |
. . . . 5
β’ ((π β§ π¦ β πΌ) β ((TopOpenβπ) Cn ((TopOpen β π
)βπ¦)) = ((TopOpenβπ) Cn (TopOpenβ(π
βπ¦)))) |
60 | 58, 59 | eleqtrrd 2837 |
. . . 4
β’ ((π β§ π¦ β πΌ) β (π₯ β (Baseβπ) β¦ ((invgβ(π
βπ¦))β(π₯βπ¦))) β ((TopOpenβπ) Cn ((TopOpen β π
)βπ¦))) |
61 | 15, 19, 2, 37, 60 | ptcn 23001 |
. . 3
β’ (π β (π₯ β (Baseβπ) β¦ (π¦ β πΌ β¦ ((invgβ(π
βπ¦))β(π₯βπ¦)))) β ((TopOpenβπ) Cn (βtβ(TopOpen
β π
)))) |
62 | | eqid 2733 |
. . . . . . 7
β’
(invgβπ) = (invgβπ) |
63 | 17, 62 | grpinvf 18805 |
. . . . . 6
β’ (π β Grp β
(invgβπ):(Baseβπ)βΆ(Baseβπ)) |
64 | 9, 63 | syl 17 |
. . . . 5
β’ (π β
(invgβπ):(Baseβπ)βΆ(Baseβπ)) |
65 | 64 | feqmptd 6914 |
. . . 4
β’ (π β
(invgβπ) =
(π₯ β (Baseβπ) β¦
((invgβπ)βπ₯))) |
66 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ)) β πΌ β π) |
67 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ)) β π β π) |
68 | 8 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ)) β π
:πΌβΆGrp) |
69 | | simpr 486 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ)) β π₯ β (Baseβπ)) |
70 | 1, 66, 67, 68, 17, 62, 69 | prdsinvgd 18866 |
. . . . 5
β’ ((π β§ π₯ β (Baseβπ)) β ((invgβπ)βπ₯) = (π¦ β πΌ β¦ ((invgβ(π
βπ¦))β(π₯βπ¦)))) |
71 | 70 | mpteq2dva 5209 |
. . . 4
β’ (π β (π₯ β (Baseβπ) β¦ ((invgβπ)βπ₯)) = (π₯ β (Baseβπ) β¦ (π¦ β πΌ β¦ ((invgβ(π
βπ¦))β(π₯βπ¦))))) |
72 | 65, 71 | eqtrd 2773 |
. . 3
β’ (π β
(invgβπ) =
(π₯ β (Baseβπ) β¦ (π¦ β πΌ β¦ ((invgβ(π
βπ¦))β(π₯βπ¦))))) |
73 | 39 | oveq2d 7377 |
. . 3
β’ (π β ((TopOpenβπ) Cn (TopOpenβπ)) = ((TopOpenβπ) Cn
(βtβ(TopOpen β π
)))) |
74 | 61, 72, 73 | 3eltr4d 2849 |
. 2
β’ (π β
(invgβπ)
β ((TopOpenβπ)
Cn (TopOpenβπ))) |
75 | 16, 62 | istgp 23451 |
. 2
β’ (π β TopGrp β (π β Grp β§ π β TopMnd β§
(invgβπ)
β ((TopOpenβπ)
Cn (TopOpenβπ)))) |
76 | 9, 14, 74, 75 | syl3anbrc 1344 |
1
β’ (π β π β TopGrp) |