| Step | Hyp | Ref
| Expression |
| 1 | | tlmlmod 24197 |
. . 3
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ LMod) |
| 2 | | lmodgrp 20865 |
. . 3
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
| 3 | 1, 2 | syl 17 |
. 2
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ Grp) |
| 4 | | tlmtmd 24195 |
. 2
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopMnd) |
| 5 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 6 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘𝑊) = (invg‘𝑊) |
| 7 | 5, 6 | grpinvf 19004 |
. . . . . 6
⊢ (𝑊 ∈ Grp →
(invg‘𝑊):(Base‘𝑊)⟶(Base‘𝑊)) |
| 8 | 3, 7 | syl 17 |
. . . . 5
⊢ (𝑊 ∈ TopMod →
(invg‘𝑊):(Base‘𝑊)⟶(Base‘𝑊)) |
| 9 | 8 | feqmptd 6977 |
. . . 4
⊢ (𝑊 ∈ TopMod →
(invg‘𝑊) =
(𝑥 ∈ (Base‘𝑊) ↦
((invg‘𝑊)‘𝑥))) |
| 10 | | eqid 2737 |
. . . . . . 7
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
| 11 | | eqid 2737 |
. . . . . . 7
⊢ (
·𝑠 ‘𝑊) = ( ·𝑠
‘𝑊) |
| 12 | | eqid 2737 |
. . . . . . 7
⊢
(1r‘(Scalar‘𝑊)) =
(1r‘(Scalar‘𝑊)) |
| 13 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘(Scalar‘𝑊)) =
(invg‘(Scalar‘𝑊)) |
| 14 | 5, 6, 10, 11, 12, 13 | lmodvneg1 20903 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ (Base‘𝑊)) →
(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑥) = ((invg‘𝑊)‘𝑥)) |
| 15 | 1, 14 | sylan 580 |
. . . . 5
⊢ ((𝑊 ∈ TopMod ∧ 𝑥 ∈ (Base‘𝑊)) →
(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑥) = ((invg‘𝑊)‘𝑥)) |
| 16 | 15 | mpteq2dva 5242 |
. . . 4
⊢ (𝑊 ∈ TopMod → (𝑥 ∈ (Base‘𝑊) ↦
(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑥)) = (𝑥 ∈ (Base‘𝑊) ↦ ((invg‘𝑊)‘𝑥))) |
| 17 | 9, 16 | eqtr4d 2780 |
. . 3
⊢ (𝑊 ∈ TopMod →
(invg‘𝑊) =
(𝑥 ∈ (Base‘𝑊) ↦
(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑥))) |
| 18 | | eqid 2737 |
. . . 4
⊢
(TopOpen‘𝑊) =
(TopOpen‘𝑊) |
| 19 | | eqid 2737 |
. . . 4
⊢
(TopOpen‘(Scalar‘𝑊)) = (TopOpen‘(Scalar‘𝑊)) |
| 20 | | id 22 |
. . . 4
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopMod) |
| 21 | | tlmtps 24196 |
. . . . 5
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopSp) |
| 22 | 5, 18 | istps 22940 |
. . . . 5
⊢ (𝑊 ∈ TopSp ↔
(TopOpen‘𝑊) ∈
(TopOn‘(Base‘𝑊))) |
| 23 | 21, 22 | sylib 218 |
. . . 4
⊢ (𝑊 ∈ TopMod →
(TopOpen‘𝑊) ∈
(TopOn‘(Base‘𝑊))) |
| 24 | 10 | tlmscatps 24199 |
. . . . . 6
⊢ (𝑊 ∈ TopMod →
(Scalar‘𝑊) ∈
TopSp) |
| 25 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
| 26 | 25, 19 | istps 22940 |
. . . . . 6
⊢
((Scalar‘𝑊)
∈ TopSp ↔ (TopOpen‘(Scalar‘𝑊)) ∈
(TopOn‘(Base‘(Scalar‘𝑊)))) |
| 27 | 24, 26 | sylib 218 |
. . . . 5
⊢ (𝑊 ∈ TopMod →
(TopOpen‘(Scalar‘𝑊)) ∈
(TopOn‘(Base‘(Scalar‘𝑊)))) |
| 28 | 10 | lmodring 20866 |
. . . . . . . 8
⊢ (𝑊 ∈ LMod →
(Scalar‘𝑊) ∈
Ring) |
| 29 | 1, 28 | syl 17 |
. . . . . . 7
⊢ (𝑊 ∈ TopMod →
(Scalar‘𝑊) ∈
Ring) |
| 30 | | ringgrp 20235 |
. . . . . . 7
⊢
((Scalar‘𝑊)
∈ Ring → (Scalar‘𝑊) ∈ Grp) |
| 31 | 29, 30 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ TopMod →
(Scalar‘𝑊) ∈
Grp) |
| 32 | 25, 12 | ringidcl 20262 |
. . . . . . 7
⊢
((Scalar‘𝑊)
∈ Ring → (1r‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) |
| 33 | 29, 32 | syl 17 |
. . . . . 6
⊢ (𝑊 ∈ TopMod →
(1r‘(Scalar‘𝑊)) ∈ (Base‘(Scalar‘𝑊))) |
| 34 | 25, 13 | grpinvcl 19005 |
. . . . . 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 23670 |
. . . 4
⊢ (𝑊 ∈ TopMod → (𝑥 ∈ (Base‘𝑊) ↦
((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))) ∈ ((TopOpen‘𝑊) Cn
(TopOpen‘(Scalar‘𝑊)))) |
| 37 | 23 | cnmptid 23669 |
. . . 4
⊢ (𝑊 ∈ TopMod → (𝑥 ∈ (Base‘𝑊) ↦ 𝑥) ∈ ((TopOpen‘𝑊) Cn (TopOpen‘𝑊))) |
| 38 | 10, 11, 18, 19, 20, 23, 36, 37 | cnmpt1vsca 24202 |
. . 3
⊢ (𝑊 ∈ TopMod → (𝑥 ∈ (Base‘𝑊) ↦
(((invg‘(Scalar‘𝑊))‘(1r‘(Scalar‘𝑊)))(
·𝑠 ‘𝑊)𝑥)) ∈ ((TopOpen‘𝑊) Cn (TopOpen‘𝑊))) |
| 39 | 17, 38 | eqeltrd 2841 |
. 2
⊢ (𝑊 ∈ TopMod →
(invg‘𝑊)
∈ ((TopOpen‘𝑊)
Cn (TopOpen‘𝑊))) |
| 40 | 18, 6 | istgp 24085 |
. 2
⊢ (𝑊 ∈ TopGrp ↔ (𝑊 ∈ Grp ∧ 𝑊 ∈ TopMnd ∧
(invg‘𝑊)
∈ ((TopOpen‘𝑊)
Cn (TopOpen‘𝑊)))) |
| 41 | 3, 4, 39, 40 | syl3anbrc 1344 |
1
⊢ (𝑊 ∈ TopMod → 𝑊 ∈ TopGrp) |