Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. 2
β’ ((πΊ β Grp β§ π½ = π« π΅) β πΊ β Grp) |
2 | | simpr 486 |
. . . 4
β’ ((πΊ β Grp β§ π½ = π« π΅) β π½ = π« π΅) |
3 | | distgp.1 |
. . . . . 6
β’ π΅ = (BaseβπΊ) |
4 | 3 | fvexi 6860 |
. . . . 5
β’ π΅ β V |
5 | | distopon 22370 |
. . . . 5
β’ (π΅ β V β π« π΅ β (TopOnβπ΅)) |
6 | 4, 5 | ax-mp 5 |
. . . 4
β’ π«
π΅ β (TopOnβπ΅) |
7 | 2, 6 | eqeltrdi 2842 |
. . 3
β’ ((πΊ β Grp β§ π½ = π« π΅) β π½ β (TopOnβπ΅)) |
8 | | distgp.2 |
. . . 4
β’ π½ = (TopOpenβπΊ) |
9 | 3, 8 | istps 22306 |
. . 3
β’ (πΊ β TopSp β π½ β (TopOnβπ΅)) |
10 | 7, 9 | sylibr 233 |
. 2
β’ ((πΊ β Grp β§ π½ = π« π΅) β πΊ β TopSp) |
11 | | eqid 2733 |
. . . . . 6
β’
(-gβπΊ) = (-gβπΊ) |
12 | 3, 11 | grpsubf 18834 |
. . . . 5
β’ (πΊ β Grp β
(-gβπΊ):(π΅ Γ π΅)βΆπ΅) |
13 | 12 | adantr 482 |
. . . 4
β’ ((πΊ β Grp β§ π½ = π« π΅) β (-gβπΊ):(π΅ Γ π΅)βΆπ΅) |
14 | 4, 4 | xpex 7691 |
. . . . 5
β’ (π΅ Γ π΅) β V |
15 | 4, 14 | elmap 8815 |
. . . 4
β’
((-gβπΊ) β (π΅ βm (π΅ Γ π΅)) β (-gβπΊ):(π΅ Γ π΅)βΆπ΅) |
16 | 13, 15 | sylibr 233 |
. . 3
β’ ((πΊ β Grp β§ π½ = π« π΅) β (-gβπΊ) β (π΅ βm (π΅ Γ π΅))) |
17 | 2, 2 | oveq12d 7379 |
. . . . . 6
β’ ((πΊ β Grp β§ π½ = π« π΅) β (π½ Γt π½) = (π« π΅ Γt π« π΅)) |
18 | | txdis 23006 |
. . . . . . 7
β’ ((π΅ β V β§ π΅ β V) β (π«
π΅ Γt
π« π΅) = π«
(π΅ Γ π΅)) |
19 | 4, 4, 18 | mp2an 691 |
. . . . . 6
β’
(π« π΅
Γt π« π΅) = π« (π΅ Γ π΅) |
20 | 17, 19 | eqtrdi 2789 |
. . . . 5
β’ ((πΊ β Grp β§ π½ = π« π΅) β (π½ Γt π½) = π« (π΅ Γ π΅)) |
21 | 20 | oveq1d 7376 |
. . . 4
β’ ((πΊ β Grp β§ π½ = π« π΅) β ((π½ Γt π½) Cn π½) = (π« (π΅ Γ π΅) Cn π½)) |
22 | | cndis 22665 |
. . . . 5
β’ (((π΅ Γ π΅) β V β§ π½ β (TopOnβπ΅)) β (π« (π΅ Γ π΅) Cn π½) = (π΅ βm (π΅ Γ π΅))) |
23 | 14, 7, 22 | sylancr 588 |
. . . 4
β’ ((πΊ β Grp β§ π½ = π« π΅) β (π« (π΅ Γ π΅) Cn π½) = (π΅ βm (π΅ Γ π΅))) |
24 | 21, 23 | eqtrd 2773 |
. . 3
β’ ((πΊ β Grp β§ π½ = π« π΅) β ((π½ Γt π½) Cn π½) = (π΅ βm (π΅ Γ π΅))) |
25 | 16, 24 | eleqtrrd 2837 |
. 2
β’ ((πΊ β Grp β§ π½ = π« π΅) β (-gβπΊ) β ((π½ Γt π½) Cn π½)) |
26 | 8, 11 | istgp2 23465 |
. 2
β’ (πΊ β TopGrp β (πΊ β Grp β§ πΊ β TopSp β§
(-gβπΊ)
β ((π½
Γt π½) Cn
π½))) |
27 | 1, 10, 25, 26 | syl3anbrc 1344 |
1
β’ ((πΊ β Grp β§ π½ = π« π΅) β πΊ β TopGrp) |