MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tlm Structured version   Visualization version   GIF version

Definition df-tlm 21959
Description: Define a topological left module, which is just what its name suggests: instead of a group over a ring with a scalar product connecting them, it is a topological group over a topological ring with a continuous scalar product. (Contributed by Mario Carneiro, 5-Oct-2015.)
Assertion
Ref Expression
df-tlm TopMod = {𝑤 ∈ (TopMnd ∩ LMod) ∣ ((Scalar‘𝑤) ∈ TopRing ∧ ( ·sf𝑤) ∈ (((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤)))}

Detailed syntax breakdown of Definition df-tlm
StepHypRef Expression
1 ctlm 21955 . 2 class TopMod
2 vw . . . . . . 7 setvar 𝑤
32cv 1481 . . . . . 6 class 𝑤
4 csca 15938 . . . . . 6 class Scalar
53, 4cfv 5886 . . . . 5 class (Scalar‘𝑤)
6 ctrg 21953 . . . . 5 class TopRing
75, 6wcel 1989 . . . 4 wff (Scalar‘𝑤) ∈ TopRing
8 cscaf 18858 . . . . . 6 class ·sf
93, 8cfv 5886 . . . . 5 class ( ·sf𝑤)
10 ctopn 16076 . . . . . . . 8 class TopOpen
115, 10cfv 5886 . . . . . . 7 class (TopOpen‘(Scalar‘𝑤))
123, 10cfv 5886 . . . . . . 7 class (TopOpen‘𝑤)
13 ctx 21357 . . . . . . 7 class ×t
1411, 12, 13co 6647 . . . . . 6 class ((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤))
15 ccn 21022 . . . . . 6 class Cn
1614, 12, 15co 6647 . . . . 5 class (((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤))
179, 16wcel 1989 . . . 4 wff ( ·sf𝑤) ∈ (((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤))
187, 17wa 384 . . 3 wff ((Scalar‘𝑤) ∈ TopRing ∧ ( ·sf𝑤) ∈ (((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤)))
19 ctmd 21868 . . . 4 class TopMnd
20 clmod 18857 . . . 4 class LMod
2119, 20cin 3571 . . 3 class (TopMnd ∩ LMod)
2218, 2, 21crab 2915 . 2 class {𝑤 ∈ (TopMnd ∩ LMod) ∣ ((Scalar‘𝑤) ∈ TopRing ∧ ( ·sf𝑤) ∈ (((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤)))}
231, 22wceq 1482 1 wff TopMod = {𝑤 ∈ (TopMnd ∩ LMod) ∣ ((Scalar‘𝑤) ∈ TopRing ∧ ( ·sf𝑤) ∈ (((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤)))}
Colors of variables: wff setvar class
This definition is referenced by:  istlm  21982
  Copyright terms: Public domain W3C validator