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 | | indistopon 22374 |
. . . . 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 | oveq2d 7377 |
. . . 4
β’ ((πΊ β Grp β§ π½ = {β
, π΅}) β ((π½ Γt π½) Cn π½) = ((π½ Γt π½) Cn {β
, π΅})) |
18 | | txtopon 22965 |
. . . . . 6
β’ ((π½ β (TopOnβπ΅) β§ π½ β (TopOnβπ΅)) β (π½ Γt π½) β (TopOnβ(π΅ Γ π΅))) |
19 | 7, 7, 18 | syl2anc 585 |
. . . . 5
β’ ((πΊ β Grp β§ π½ = {β
, π΅}) β (π½ Γt π½) β (TopOnβ(π΅ Γ π΅))) |
20 | | cnindis 22666 |
. . . . 5
β’ (((π½ Γt π½) β (TopOnβ(π΅ Γ π΅)) β§ π΅ β V) β ((π½ Γt π½) Cn {β
, π΅}) = (π΅ βm (π΅ Γ π΅))) |
21 | 19, 4, 20 | sylancl 587 |
. . . 4
β’ ((πΊ β Grp β§ π½ = {β
, π΅}) β ((π½ Γt π½) Cn {β
, π΅}) = (π΅ βm (π΅ Γ π΅))) |
22 | 17, 21 | eqtrd 2773 |
. . 3
β’ ((πΊ β Grp β§ π½ = {β
, π΅}) β ((π½ Γt π½) Cn π½) = (π΅ βm (π΅ Γ π΅))) |
23 | 16, 22 | eleqtrrd 2837 |
. 2
β’ ((πΊ β Grp β§ π½ = {β
, π΅}) β (-gβπΊ) β ((π½ Γt π½) Cn π½)) |
24 | 8, 11 | istgp2 23465 |
. 2
β’ (πΊ β TopGrp β (πΊ β Grp β§ πΊ β TopSp β§
(-gβπΊ)
β ((π½
Γt π½) Cn
π½))) |
25 | 1, 10, 23, 24 | syl3anbrc 1344 |
1
β’ ((πΊ β Grp β§ π½ = {β
, π΅}) β πΊ β TopGrp) |