Step | Hyp | Ref
| Expression |
1 | | subgtgp.h |
. . . 4
โข ๐ป = (๐บ โพs ๐) |
2 | 1 | subggrp 18939 |
. . 3
โข (๐ โ (SubGrpโ๐บ) โ ๐ป โ Grp) |
3 | 2 | adantl 483 |
. 2
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ๐ป โ Grp) |
4 | | tgptmd 23453 |
. . 3
โข (๐บ โ TopGrp โ ๐บ โ TopMnd) |
5 | | subgsubm 18958 |
. . 3
โข (๐ โ (SubGrpโ๐บ) โ ๐ โ (SubMndโ๐บ)) |
6 | 1 | submtmd 23478 |
. . 3
โข ((๐บ โ TopMnd โง ๐ โ (SubMndโ๐บ)) โ ๐ป โ TopMnd) |
7 | 4, 5, 6 | syl2an 597 |
. 2
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ๐ป โ TopMnd) |
8 | 1 | subgbas 18940 |
. . . . . . 7
โข (๐ โ (SubGrpโ๐บ) โ ๐ = (Baseโ๐ป)) |
9 | 8 | adantl 483 |
. . . . . 6
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ๐ = (Baseโ๐ป)) |
10 | 9 | mpteq1d 5204 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ (๐ฅ โ ๐ โฆ ((invgโ๐ป)โ๐ฅ)) = (๐ฅ โ (Baseโ๐ป) โฆ ((invgโ๐ป)โ๐ฅ))) |
11 | | eqid 2733 |
. . . . . . . 8
โข
(invgโ๐บ) = (invgโ๐บ) |
12 | | eqid 2733 |
. . . . . . . 8
โข
(invgโ๐ป) = (invgโ๐ป) |
13 | 1, 11, 12 | subginv 18943 |
. . . . . . 7
โข ((๐ โ (SubGrpโ๐บ) โง ๐ฅ โ ๐) โ ((invgโ๐บ)โ๐ฅ) = ((invgโ๐ป)โ๐ฅ)) |
14 | 13 | adantll 713 |
. . . . . 6
โข (((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โง ๐ฅ โ ๐) โ ((invgโ๐บ)โ๐ฅ) = ((invgโ๐ป)โ๐ฅ)) |
15 | 14 | mpteq2dva 5209 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ (๐ฅ โ ๐ โฆ ((invgโ๐บ)โ๐ฅ)) = (๐ฅ โ ๐ โฆ ((invgโ๐ป)โ๐ฅ))) |
16 | | eqid 2733 |
. . . . . . . 8
โข
(Baseโ๐ป) =
(Baseโ๐ป) |
17 | 16, 12 | grpinvf 18805 |
. . . . . . 7
โข (๐ป โ Grp โ
(invgโ๐ป):(Baseโ๐ป)โถ(Baseโ๐ป)) |
18 | 3, 17 | syl 17 |
. . . . . 6
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐ป):(Baseโ๐ป)โถ(Baseโ๐ป)) |
19 | 18 | feqmptd 6914 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐ป) =
(๐ฅ โ (Baseโ๐ป) โฆ
((invgโ๐ป)โ๐ฅ))) |
20 | 10, 15, 19 | 3eqtr4rd 2784 |
. . . 4
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐ป) =
(๐ฅ โ ๐ โฆ ((invgโ๐บ)โ๐ฅ))) |
21 | | eqid 2733 |
. . . . 5
โข
((TopOpenโ๐บ)
โพt ๐) =
((TopOpenโ๐บ)
โพt ๐) |
22 | | eqid 2733 |
. . . . . . 7
โข
(TopOpenโ๐บ) =
(TopOpenโ๐บ) |
23 | | eqid 2733 |
. . . . . . 7
โข
(Baseโ๐บ) =
(Baseโ๐บ) |
24 | 22, 23 | tgptopon 23456 |
. . . . . 6
โข (๐บ โ TopGrp โ
(TopOpenโ๐บ) โ
(TopOnโ(Baseโ๐บ))) |
25 | 24 | adantr 482 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ (TopOpenโ๐บ) โ
(TopOnโ(Baseโ๐บ))) |
26 | 23 | subgss 18937 |
. . . . . 6
โข (๐ โ (SubGrpโ๐บ) โ ๐ โ (Baseโ๐บ)) |
27 | 26 | adantl 483 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ๐ โ (Baseโ๐บ)) |
28 | | tgpgrp 23452 |
. . . . . . . . 9
โข (๐บ โ TopGrp โ ๐บ โ Grp) |
29 | 28 | adantr 482 |
. . . . . . . 8
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ๐บ โ Grp) |
30 | 23, 11 | grpinvf 18805 |
. . . . . . . 8
โข (๐บ โ Grp โ
(invgโ๐บ):(Baseโ๐บ)โถ(Baseโ๐บ)) |
31 | 29, 30 | syl 17 |
. . . . . . 7
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐บ):(Baseโ๐บ)โถ(Baseโ๐บ)) |
32 | 31 | feqmptd 6914 |
. . . . . 6
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐บ) =
(๐ฅ โ (Baseโ๐บ) โฆ
((invgโ๐บ)โ๐ฅ))) |
33 | 22, 11 | tgpinv 23459 |
. . . . . . 7
โข (๐บ โ TopGrp โ
(invgโ๐บ)
โ ((TopOpenโ๐บ)
Cn (TopOpenโ๐บ))) |
34 | 33 | adantr 482 |
. . . . . 6
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐บ)
โ ((TopOpenโ๐บ)
Cn (TopOpenโ๐บ))) |
35 | 32, 34 | eqeltrrd 2835 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ (๐ฅ โ (Baseโ๐บ) โฆ ((invgโ๐บ)โ๐ฅ)) โ ((TopOpenโ๐บ) Cn (TopOpenโ๐บ))) |
36 | 21, 25, 27, 35 | cnmpt1res 23050 |
. . . 4
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ (๐ฅ โ ๐ โฆ ((invgโ๐บ)โ๐ฅ)) โ (((TopOpenโ๐บ) โพt ๐) Cn (TopOpenโ๐บ))) |
37 | 20, 36 | eqeltrd 2834 |
. . 3
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐ป)
โ (((TopOpenโ๐บ)
โพt ๐) Cn
(TopOpenโ๐บ))) |
38 | 18 | frnd 6680 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ran
(invgโ๐ป)
โ (Baseโ๐ป)) |
39 | 38, 9 | sseqtrrd 3989 |
. . . 4
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ran
(invgโ๐ป)
โ ๐) |
40 | | cnrest2 22660 |
. . . 4
โข
(((TopOpenโ๐บ)
โ (TopOnโ(Baseโ๐บ)) โง ran (invgโ๐ป) โ ๐ โง ๐ โ (Baseโ๐บ)) โ ((invgโ๐ป) โ (((TopOpenโ๐บ) โพt ๐) Cn (TopOpenโ๐บ)) โ
(invgโ๐ป)
โ (((TopOpenโ๐บ)
โพt ๐) Cn
((TopOpenโ๐บ)
โพt ๐)))) |
41 | 25, 39, 27, 40 | syl3anc 1372 |
. . 3
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
((invgโ๐ป)
โ (((TopOpenโ๐บ)
โพt ๐) Cn
(TopOpenโ๐บ)) โ
(invgโ๐ป)
โ (((TopOpenโ๐บ)
โพt ๐) Cn
((TopOpenโ๐บ)
โพt ๐)))) |
42 | 37, 41 | mpbid 231 |
. 2
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐ป)
โ (((TopOpenโ๐บ)
โพt ๐) Cn
((TopOpenโ๐บ)
โพt ๐))) |
43 | 1, 22 | resstopn 22560 |
. . 3
โข
((TopOpenโ๐บ)
โพt ๐) =
(TopOpenโ๐ป) |
44 | 43, 12 | istgp 23451 |
. 2
โข (๐ป โ TopGrp โ (๐ป โ Grp โง ๐ป โ TopMnd โง
(invgโ๐ป)
โ (((TopOpenโ๐บ)
โพt ๐) Cn
((TopOpenโ๐บ)
โพt ๐)))) |
45 | 3, 7, 42, 44 | syl3anbrc 1344 |
1
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ๐ป โ TopGrp) |