| Step | Hyp | Ref
| Expression |
|---|
| 1 | | tlmlmod 23684 |
. . 3
β’ (π β TopMod β π β LMod) |
| 2 | | lmodgrp 20470 |
. . 3
β’ (π β LMod β π β Grp) |
| 3 | 1, 2 | syl 17 |
. 2
β’ (π β TopMod β π β Grp) |
| 4 | | tlmtmd 23682 |
. 2
β’ (π β TopMod β π β TopMnd) |
| 5 | | eqid 2732 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
| 6 | | eqid 2732 |
. . . . . . 7
β’
(invgβπ) = (invgβπ) |
| 7 | 5, 6 | grpinvf 18867 |
. . . . . 6
β’ (π β Grp β
(invgβπ):(Baseβπ)βΆ(Baseβπ)) |
| 8 | 3, 7 | syl 17 |
. . . . 5
β’ (π β TopMod β
(invgβπ):(Baseβπ)βΆ(Baseβπ)) |
| 9 | 8 | feqmptd 6957 |
. . . 4
β’ (π β TopMod β
(invgβπ) =
(π₯ β (Baseβπ) β¦
((invgβπ)βπ₯))) |
| 10 | | eqid 2732 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
| 11 | | eqid 2732 |
. . . . . . 7
β’ (
Β·π βπ) = ( Β·π
βπ) |
| 12 | | eqid 2732 |
. . . . . . 7
β’
(1rβ(Scalarβπ)) =
(1rβ(Scalarβπ)) |
| 13 | | eqid 2732 |
. . . . . . 7
β’
(invgβ(Scalarβπ)) =
(invgβ(Scalarβπ)) |
| 14 | 5, 6, 10, 11, 12, 13 | lmodvneg1 20507 |
. . . . . 6
β’ ((π β LMod β§ π₯ β (Baseβπ)) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π₯) = ((invgβπ)βπ₯)) |
| 15 | 1, 14 | sylan 580 |
. . . . 5
β’ ((π β TopMod β§ π₯ β (Baseβπ)) β
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π₯) = ((invgβπ)βπ₯)) |
| 16 | 15 | mpteq2dva 5247 |
. . . 4
β’ (π β TopMod β (π₯ β (Baseβπ) β¦
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π₯)) = (π₯ β (Baseβπ) β¦ ((invgβπ)βπ₯))) |
| 17 | 9, 16 | eqtr4d 2775 |
. . 3
β’ (π β TopMod β
(invgβπ) =
(π₯ β (Baseβπ) β¦
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π₯))) |
| 18 | | eqid 2732 |
. . . 4
β’
(TopOpenβπ) =
(TopOpenβπ) |
| 19 | | eqid 2732 |
. . . 4
β’
(TopOpenβ(Scalarβπ)) = (TopOpenβ(Scalarβπ)) |
| 20 | | id 22 |
. . . 4
β’ (π β TopMod β π β TopMod) |
| 21 | | tlmtps 23683 |
. . . . 5
β’ (π β TopMod β π β TopSp) |
| 22 | 5, 18 | istps 22427 |
. . . . 5
β’ (π β TopSp β
(TopOpenβπ) β
(TopOnβ(Baseβπ))) |
| 23 | 21, 22 | sylib 217 |
. . . 4
β’ (π β TopMod β
(TopOpenβπ) β
(TopOnβ(Baseβπ))) |
| 24 | 10 | tlmscatps 23686 |
. . . . . 6
β’ (π β TopMod β
(Scalarβπ) β
TopSp) |
| 25 | | eqid 2732 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
| 26 | 25, 19 | istps 22427 |
. . . . . 6
β’
((Scalarβπ)
β TopSp β (TopOpenβ(Scalarβπ)) β
(TopOnβ(Baseβ(Scalarβπ)))) |
| 27 | 24, 26 | sylib 217 |
. . . . 5
β’ (π β TopMod β
(TopOpenβ(Scalarβπ)) β
(TopOnβ(Baseβ(Scalarβπ)))) |
| 28 | 10 | lmodring 20471 |
. . . . . . . 8
β’ (π β LMod β
(Scalarβπ) β
Ring) |
| 29 | 1, 28 | syl 17 |
. . . . . . 7
β’ (π β TopMod β
(Scalarβπ) β
Ring) |
| 30 | | ringgrp 20054 |
. . . . . . 7
β’
((Scalarβπ)
β Ring β (Scalarβπ) β Grp) |
| 31 | 29, 30 | syl 17 |
. . . . . 6
β’ (π β TopMod β
(Scalarβπ) β
Grp) |
| 32 | 25, 12 | ringidcl 20076 |
. . . . . . 7
β’
((Scalarβπ)
β Ring β (1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
| 33 | 29, 32 | syl 17 |
. . . . . 6
β’ (π β TopMod β
(1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) |
| 34 | 25, 13 | grpinvcl 18868 |
. . . . . 6
β’
(((Scalarβπ)
β Grp β§ (1rβ(Scalarβπ)) β (Baseβ(Scalarβπ))) β
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
| 35 | 31, 33, 34 | syl2anc 584 |
. . . . 5
β’ (π β TopMod β
((invgβ(Scalarβπ))β(1rβ(Scalarβπ))) β
(Baseβ(Scalarβπ))) |
| 36 | 23, 27, 35 | cnmptc 23157 |
. . . 4
β’ (π β TopMod β (π₯ β (Baseβπ) β¦
((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))) β ((TopOpenβπ) Cn
(TopOpenβ(Scalarβπ)))) |
| 37 | 23 | cnmptid 23156 |
. . . 4
β’ (π β TopMod β (π₯ β (Baseβπ) β¦ π₯) β ((TopOpenβπ) Cn (TopOpenβπ))) |
| 38 | 10, 11, 18, 19, 20, 23, 36, 37 | cnmpt1vsca 23689 |
. . 3
β’ (π β TopMod β (π₯ β (Baseβπ) β¦
(((invgβ(Scalarβπ))β(1rβ(Scalarβπ)))(
Β·π βπ)π₯)) β ((TopOpenβπ) Cn (TopOpenβπ))) |
| 39 | 17, 38 | eqeltrd 2833 |
. 2
β’ (π β TopMod β
(invgβπ)
β ((TopOpenβπ)
Cn (TopOpenβπ))) |
| 40 | 18, 6 | istgp 23572 |
. 2
β’ (π β TopGrp β (π β Grp β§ π β TopMnd β§
(invgβπ)
β ((TopOpenβπ)
Cn (TopOpenβπ)))) |
| 41 | 3, 4, 39, 40 | syl3anbrc 1343 |
1
β’ (π β TopMod β π β TopGrp) |
