Step | Hyp | Ref
| Expression |
1 | | subgtgp.h |
. . . 4
โข ๐ป = (๐บ โพs ๐) |
2 | 1 | subggrp 19008 |
. . 3
โข (๐ โ (SubGrpโ๐บ) โ ๐ป โ Grp) |
3 | 2 | adantl 482 |
. 2
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ๐ป โ Grp) |
4 | | tgptmd 23582 |
. . 3
โข (๐บ โ TopGrp โ ๐บ โ TopMnd) |
5 | | subgsubm 19027 |
. . 3
โข (๐ โ (SubGrpโ๐บ) โ ๐ โ (SubMndโ๐บ)) |
6 | 1 | submtmd 23607 |
. . 3
โข ((๐บ โ TopMnd โง ๐ โ (SubMndโ๐บ)) โ ๐ป โ TopMnd) |
7 | 4, 5, 6 | syl2an 596 |
. 2
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ๐ป โ TopMnd) |
8 | 1 | subgbas 19009 |
. . . . . . 7
โข (๐ โ (SubGrpโ๐บ) โ ๐ = (Baseโ๐ป)) |
9 | 8 | adantl 482 |
. . . . . 6
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ๐ = (Baseโ๐ป)) |
10 | 9 | mpteq1d 5243 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ (๐ฅ โ ๐ โฆ ((invgโ๐ป)โ๐ฅ)) = (๐ฅ โ (Baseโ๐ป) โฆ ((invgโ๐ป)โ๐ฅ))) |
11 | | eqid 2732 |
. . . . . . . 8
โข
(invgโ๐บ) = (invgโ๐บ) |
12 | | eqid 2732 |
. . . . . . . 8
โข
(invgโ๐ป) = (invgโ๐ป) |
13 | 1, 11, 12 | subginv 19012 |
. . . . . . 7
โข ((๐ โ (SubGrpโ๐บ) โง ๐ฅ โ ๐) โ ((invgโ๐บ)โ๐ฅ) = ((invgโ๐ป)โ๐ฅ)) |
14 | 13 | adantll 712 |
. . . . . 6
โข (((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โง ๐ฅ โ ๐) โ ((invgโ๐บ)โ๐ฅ) = ((invgโ๐ป)โ๐ฅ)) |
15 | 14 | mpteq2dva 5248 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ (๐ฅ โ ๐ โฆ ((invgโ๐บ)โ๐ฅ)) = (๐ฅ โ ๐ โฆ ((invgโ๐ป)โ๐ฅ))) |
16 | | eqid 2732 |
. . . . . . . 8
โข
(Baseโ๐ป) =
(Baseโ๐ป) |
17 | 16, 12 | grpinvf 18870 |
. . . . . . 7
โข (๐ป โ Grp โ
(invgโ๐ป):(Baseโ๐ป)โถ(Baseโ๐ป)) |
18 | 3, 17 | syl 17 |
. . . . . 6
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐ป):(Baseโ๐ป)โถ(Baseโ๐ป)) |
19 | 18 | feqmptd 6960 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐ป) =
(๐ฅ โ (Baseโ๐ป) โฆ
((invgโ๐ป)โ๐ฅ))) |
20 | 10, 15, 19 | 3eqtr4rd 2783 |
. . . 4
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐ป) =
(๐ฅ โ ๐ โฆ ((invgโ๐บ)โ๐ฅ))) |
21 | | eqid 2732 |
. . . . 5
โข
((TopOpenโ๐บ)
โพt ๐) =
((TopOpenโ๐บ)
โพt ๐) |
22 | | eqid 2732 |
. . . . . . 7
โข
(TopOpenโ๐บ) =
(TopOpenโ๐บ) |
23 | | eqid 2732 |
. . . . . . 7
โข
(Baseโ๐บ) =
(Baseโ๐บ) |
24 | 22, 23 | tgptopon 23585 |
. . . . . 6
โข (๐บ โ TopGrp โ
(TopOpenโ๐บ) โ
(TopOnโ(Baseโ๐บ))) |
25 | 24 | adantr 481 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ (TopOpenโ๐บ) โ
(TopOnโ(Baseโ๐บ))) |
26 | 23 | subgss 19006 |
. . . . . 6
โข (๐ โ (SubGrpโ๐บ) โ ๐ โ (Baseโ๐บ)) |
27 | 26 | adantl 482 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ๐ โ (Baseโ๐บ)) |
28 | | tgpgrp 23581 |
. . . . . . . . 9
โข (๐บ โ TopGrp โ ๐บ โ Grp) |
29 | 28 | adantr 481 |
. . . . . . . 8
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ๐บ โ Grp) |
30 | 23, 11 | grpinvf 18870 |
. . . . . . . 8
โข (๐บ โ Grp โ
(invgโ๐บ):(Baseโ๐บ)โถ(Baseโ๐บ)) |
31 | 29, 30 | syl 17 |
. . . . . . 7
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐บ):(Baseโ๐บ)โถ(Baseโ๐บ)) |
32 | 31 | feqmptd 6960 |
. . . . . 6
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐บ) =
(๐ฅ โ (Baseโ๐บ) โฆ
((invgโ๐บ)โ๐ฅ))) |
33 | 22, 11 | tgpinv 23588 |
. . . . . . 7
โข (๐บ โ TopGrp โ
(invgโ๐บ)
โ ((TopOpenโ๐บ)
Cn (TopOpenโ๐บ))) |
34 | 33 | adantr 481 |
. . . . . 6
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐บ)
โ ((TopOpenโ๐บ)
Cn (TopOpenโ๐บ))) |
35 | 32, 34 | eqeltrrd 2834 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ (๐ฅ โ (Baseโ๐บ) โฆ ((invgโ๐บ)โ๐ฅ)) โ ((TopOpenโ๐บ) Cn (TopOpenโ๐บ))) |
36 | 21, 25, 27, 35 | cnmpt1res 23179 |
. . . 4
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ (๐ฅ โ ๐ โฆ ((invgโ๐บ)โ๐ฅ)) โ (((TopOpenโ๐บ) โพt ๐) Cn (TopOpenโ๐บ))) |
37 | 20, 36 | eqeltrd 2833 |
. . 3
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ
(invgโ๐ป)
โ (((TopOpenโ๐บ)
โพt ๐) Cn
(TopOpenโ๐บ))) |
38 | 18 | frnd 6725 |
. . . . 5
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ran
(invgโ๐ป)
โ (Baseโ๐ป)) |
39 | 38, 9 | sseqtrrd 4023 |
. . . 4
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ran
(invgโ๐ป)
โ ๐) |
40 | | cnrest2 22789 |
. . . 4
โข
(((TopOpenโ๐บ)
โ (TopOnโ(Baseโ๐บ)) โง ran (invgโ๐ป) โ ๐ โง ๐ โ (Baseโ๐บ)) โ ((invgโ๐ป) โ (((TopOpenโ๐บ) โพt ๐) Cn (TopOpenโ๐บ)) โ
(invgโ๐ป)
โ (((TopOpenโ๐บ)
โพt ๐) Cn
((TopOpenโ๐บ)
โพt ๐)))) |
41 | 25, 39, 27, 40 | syl3anc 1371 |
. . 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 22689 |
. . 3
โข
((TopOpenโ๐บ)
โพt ๐) =
(TopOpenโ๐ป) |
44 | 43, 12 | istgp 23580 |
. 2
โข (๐ป โ TopGrp โ (๐ป โ Grp โง ๐ป โ TopMnd โง
(invgโ๐ป)
โ (((TopOpenโ๐บ)
โพt ๐) Cn
((TopOpenโ๐บ)
โพt ๐)))) |
45 | 3, 7, 42, 44 | syl3anbrc 1343 |
1
โข ((๐บ โ TopGrp โง ๐ โ (SubGrpโ๐บ)) โ ๐ป โ TopGrp) |