Step | Hyp | Ref
| Expression |
1 | | tlmlmod 23556 |
. . 3
β’ (π β TopMod β π β LMod) |
2 | | lmodgrp 20343 |
. . 3
β’ (π β LMod β π β Grp) |
3 | 1, 2 | syl 17 |
. 2
β’ (π β TopMod β π β Grp) |
4 | | tlmtmd 23554 |
. 2
β’ (π β TopMod β π β TopMnd) |
5 | | eqid 2733 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
6 | | eqid 2733 |
. . . . . . 7
β’
(invgβπ) = (invgβπ) |
7 | 5, 6 | grpinvf 18802 |
. . . . . 6
β’ (π β Grp β
(invgβπ):(Baseβπ)βΆ(Baseβπ)) |
8 | 3, 7 | syl 17 |
. . . . 5
β’ (π β TopMod β
(invgβπ):(Baseβπ)βΆ(Baseβπ)) |
9 | 8 | feqmptd 6911 |
. . . 4
β’ (π β TopMod β
(invgβπ) =
(π₯ β (Baseβπ) β¦
((invgβπ)βπ₯))) |
10 | | eqid 2733 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
11 | | eqid 2733 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
12 | | eqid 2733 |
. . . . . . 7
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
13 | | eqid 2733 |
. . . . . . 7
β’
(invgβ(Scalarβπ)) =
(invgβ(Scalarβπ)) |
14 | 5, 6, 10, 11, 12, 13 | lmodvneg1 20380 |
. . . . . 6
β’ ((π β LMod β§ π₯ β (Baseβπ)) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π₯) = ((invgβπ)βπ₯)) |
15 | 1, 14 | sylan 581 |
. . . . 5
β’ ((π β TopMod β§ π₯ β (Baseβπ)) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π₯) = ((invgβπ)βπ₯)) |
16 | 15 | mpteq2dva 5206 |
. . . 4
β’ (π β TopMod β (π₯ β (Baseβπ) β¦
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π₯)) = (π₯ β (Baseβπ) β¦ ((invgβπ)βπ₯))) |
17 | 9, 16 | eqtr4d 2776 |
. . 3
β’ (π β TopMod β
(invgβπ) =
(π₯ β (Baseβπ) β¦
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π₯))) |
18 | | eqid 2733 |
. . . 4
β’
(TopOpenβπ) =
(TopOpenβπ) |
19 | | eqid 2733 |
. . . 4
β’
(TopOpenβ(Scalarβπ)) = (TopOpenβ(Scalarβπ)) |
20 | | id 22 |
. . . 4
β’ (π β TopMod β π β TopMod) |
21 | | tlmtps 23555 |
. . . . 5
β’ (π β TopMod β π β TopSp) |
22 | 5, 18 | istps 22299 |
. . . . 5
β’ (π β TopSp β
(TopOpenβπ) β
(TopOnβ(Baseβπ))) |
23 | 21, 22 | sylib 217 |
. . . 4
β’ (π β TopMod β
(TopOpenβπ) β
(TopOnβ(Baseβπ))) |
24 | 10 | tlmscatps 23558 |
. . . . . 6
β’ (π β TopMod β
(Scalarβπ) β
TopSp) |
25 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
26 | 25, 19 | istps 22299 |
. . . . . 6
β’
((Scalarβπ)
β TopSp β (TopOpenβ(Scalarβπ)) β
(TopOnβ(Baseβ(Scalarβπ)))) |
27 | 24, 26 | sylib 217 |
. . . . 5
β’ (π β TopMod β
(TopOpenβ(Scalarβπ)) β
(TopOnβ(Baseβ(Scalarβπ)))) |
28 | 10 | lmodring 20344 |
. . . . . . . 8
β’ (π β LMod β
(Scalarβπ) β
Ring) |
29 | 1, 28 | syl 17 |
. . . . . . 7
β’ (π β TopMod β
(Scalarβπ) β
Ring) |
30 | | ringgrp 19974 |
. . . . . . 7
β’
((Scalarβπ)
β Ring β (Scalarβπ) β Grp) |
31 | 29, 30 | syl 17 |
. . . . . 6
β’ (π β TopMod β
(Scalarβπ) β
Grp) |
32 | 25, 12 | ringidcl 19994 |
. . . . . . 7
β’
((Scalarβπ)
β Ring β (1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
33 | 29, 32 | syl 17 |
. . . . . 6
β’ (π β TopMod β
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
34 | 25, 13 | grpinvcl 18803 |
. . . . . 6
β’
(((Scalarβπ)
β Grp β§ (1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) β
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
35 | 31, 33, 34 | syl2anc 585 |
. . . . 5
β’ (π β TopMod β
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
36 | 23, 27, 35 | cnmptc 23029 |
. . . 4
β’ (π β TopMod β (π₯ β (Baseβπ) β¦
((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))) β ((TopOpenβπ) Cn
(TopOpenβ(Scalarβπ)))) |
37 | 23 | cnmptid 23028 |
. . . 4
β’ (π β TopMod β (π₯ β (Baseβπ) β¦ π₯) β ((TopOpenβπ) Cn (TopOpenβπ))) |
38 | 10, 11, 18, 19, 20, 23, 36, 37 | cnmpt1vsca 23561 |
. . 3
β’ (π β TopMod β (π₯ β (Baseβπ) β¦
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π₯)) β ((TopOpenβπ) Cn (TopOpenβπ))) |
39 | 17, 38 | eqeltrd 2834 |
. 2
β’ (π β TopMod β
(invgβπ)
β ((TopOpenβπ)
Cn (TopOpenβπ))) |
40 | 18, 6 | istgp 23444 |
. 2
β’ (π β TopGrp β (π β Grp β§ π β TopMnd β§
(invgβπ)
β ((TopOpenβπ)
Cn (TopOpenβπ)))) |
41 | 3, 4, 39, 40 | syl3anbrc 1344 |
1
β’ (π β TopMod β π β TopGrp) |