Step | Hyp | Ref
| Expression |
1 | | tgptmd 23453 |
. . 3
β’ (πΊ β TopGrp β πΊ β TopMnd) |
2 | | tgplacthmeo.1 |
. . . 4
β’ πΉ = (π₯ β π β¦ (π΄ + π₯)) |
3 | | tgplacthmeo.2 |
. . . 4
β’ π = (BaseβπΊ) |
4 | | tgplacthmeo.3 |
. . . 4
β’ + =
(+gβπΊ) |
5 | | tgplacthmeo.4 |
. . . 4
β’ π½ = (TopOpenβπΊ) |
6 | 2, 3, 4, 5 | tmdlactcn 23476 |
. . 3
β’ ((πΊ β TopMnd β§ π΄ β π) β πΉ β (π½ Cn π½)) |
7 | 1, 6 | sylan 581 |
. 2
β’ ((πΊ β TopGrp β§ π΄ β π) β πΉ β (π½ Cn π½)) |
8 | | tgpgrp 23452 |
. . . . . 6
β’ (πΊ β TopGrp β πΊ β Grp) |
9 | | eqid 2733 |
. . . . . . 7
β’ (π β π β¦ (π₯ β π β¦ (π + π₯))) = (π β π β¦ (π₯ β π β¦ (π + π₯))) |
10 | | eqid 2733 |
. . . . . . 7
β’
(invgβπΊ) = (invgβπΊ) |
11 | 9, 3, 4, 10 | grplactcnv 18858 |
. . . . . 6
β’ ((πΊ β Grp β§ π΄ β π) β (((π β π β¦ (π₯ β π β¦ (π + π₯)))βπ΄):πβ1-1-ontoβπ β§ β‘((π β π β¦ (π₯ β π β¦ (π + π₯)))βπ΄) = ((π β π β¦ (π₯ β π β¦ (π + π₯)))β((invgβπΊ)βπ΄)))) |
12 | 8, 11 | sylan 581 |
. . . . 5
β’ ((πΊ β TopGrp β§ π΄ β π) β (((π β π β¦ (π₯ β π β¦ (π + π₯)))βπ΄):πβ1-1-ontoβπ β§ β‘((π β π β¦ (π₯ β π β¦ (π + π₯)))βπ΄) = ((π β π β¦ (π₯ β π β¦ (π + π₯)))β((invgβπΊ)βπ΄)))) |
13 | 12 | simprd 497 |
. . . 4
β’ ((πΊ β TopGrp β§ π΄ β π) β β‘((π β π β¦ (π₯ β π β¦ (π + π₯)))βπ΄) = ((π β π β¦ (π₯ β π β¦ (π + π₯)))β((invgβπΊ)βπ΄))) |
14 | 9, 3 | grplactfval 18856 |
. . . . . . 7
β’ (π΄ β π β ((π β π β¦ (π₯ β π β¦ (π + π₯)))βπ΄) = (π₯ β π β¦ (π΄ + π₯))) |
15 | 14 | adantl 483 |
. . . . . 6
β’ ((πΊ β TopGrp β§ π΄ β π) β ((π β π β¦ (π₯ β π β¦ (π + π₯)))βπ΄) = (π₯ β π β¦ (π΄ + π₯))) |
16 | 15, 2 | eqtr4di 2791 |
. . . . 5
β’ ((πΊ β TopGrp β§ π΄ β π) β ((π β π β¦ (π₯ β π β¦ (π + π₯)))βπ΄) = πΉ) |
17 | 16 | cnveqd 5835 |
. . . 4
β’ ((πΊ β TopGrp β§ π΄ β π) β β‘((π β π β¦ (π₯ β π β¦ (π + π₯)))βπ΄) = β‘πΉ) |
18 | 3, 10 | grpinvcl 18806 |
. . . . . 6
β’ ((πΊ β Grp β§ π΄ β π) β ((invgβπΊ)βπ΄) β π) |
19 | 8, 18 | sylan 581 |
. . . . 5
β’ ((πΊ β TopGrp β§ π΄ β π) β ((invgβπΊ)βπ΄) β π) |
20 | 9, 3 | grplactfval 18856 |
. . . . 5
β’
(((invgβπΊ)βπ΄) β π β ((π β π β¦ (π₯ β π β¦ (π + π₯)))β((invgβπΊ)βπ΄)) = (π₯ β π β¦ (((invgβπΊ)βπ΄) + π₯))) |
21 | 19, 20 | syl 17 |
. . . 4
β’ ((πΊ β TopGrp β§ π΄ β π) β ((π β π β¦ (π₯ β π β¦ (π + π₯)))β((invgβπΊ)βπ΄)) = (π₯ β π β¦ (((invgβπΊ)βπ΄) + π₯))) |
22 | 13, 17, 21 | 3eqtr3d 2781 |
. . 3
β’ ((πΊ β TopGrp β§ π΄ β π) β β‘πΉ = (π₯ β π β¦ (((invgβπΊ)βπ΄) + π₯))) |
23 | | eqid 2733 |
. . . . 5
β’ (π₯ β π β¦ (((invgβπΊ)βπ΄) + π₯)) = (π₯ β π β¦ (((invgβπΊ)βπ΄) + π₯)) |
24 | 23, 3, 4, 5 | tmdlactcn 23476 |
. . . 4
β’ ((πΊ β TopMnd β§
((invgβπΊ)βπ΄) β π) β (π₯ β π β¦ (((invgβπΊ)βπ΄) + π₯)) β (π½ Cn π½)) |
25 | 1, 19, 24 | syl2an2r 684 |
. . 3
β’ ((πΊ β TopGrp β§ π΄ β π) β (π₯ β π β¦ (((invgβπΊ)βπ΄) + π₯)) β (π½ Cn π½)) |
26 | 22, 25 | eqeltrd 2834 |
. 2
β’ ((πΊ β TopGrp β§ π΄ β π) β β‘πΉ β (π½ Cn π½)) |
27 | | ishmeo 23133 |
. 2
β’ (πΉ β (π½Homeoπ½) β (πΉ β (π½ Cn π½) β§ β‘πΉ β (π½ Cn π½))) |
28 | 7, 26, 27 | sylanbrc 584 |
1
β’ ((πΊ β TopGrp β§ π΄ β π) β πΉ β (π½Homeoπ½)) |