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

Definition df-tlm 22862
 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 22858 . 2 class TopMod
2 vw . . . . . . 7 setvar 𝑤
32cv 1537 . . . . . 6 class 𝑤
4 csca 16626 . . . . . 6 class Scalar
53, 4cfv 6335 . . . . 5 class (Scalar‘𝑤)
6 ctrg 22856 . . . . 5 class TopRing
75, 6wcel 2111 . . . 4 wff (Scalar‘𝑤) ∈ TopRing
8 cscaf 19703 . . . . . 6 class ·sf
93, 8cfv 6335 . . . . 5 class ( ·sf𝑤)
10 ctopn 16753 . . . . . . . 8 class TopOpen
115, 10cfv 6335 . . . . . . 7 class (TopOpen‘(Scalar‘𝑤))
123, 10cfv 6335 . . . . . . 7 class (TopOpen‘𝑤)
13 ctx 22260 . . . . . . 7 class ×t
1411, 12, 13co 7150 . . . . . 6 class ((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤))
15 ccn 21924 . . . . . 6 class Cn
1614, 12, 15co 7150 . . . . 5 class (((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤))
179, 16wcel 2111 . . . 4 wff ( ·sf𝑤) ∈ (((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤))
187, 17wa 399 . . 3 wff ((Scalar‘𝑤) ∈ TopRing ∧ ( ·sf𝑤) ∈ (((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤)))
19 ctmd 22770 . . . 4 class TopMnd
20 clmod 19702 . . . 4 class LMod
2119, 20cin 3857 . . 3 class (TopMnd ∩ LMod)
2218, 2, 21crab 3074 . 2 class {𝑤 ∈ (TopMnd ∩ LMod) ∣ ((Scalar‘𝑤) ∈ TopRing ∧ ( ·sf𝑤) ∈ (((TopOpen‘(Scalar‘𝑤)) ×t (TopOpen‘𝑤)) Cn (TopOpen‘𝑤)))}
231, 22wceq 1538 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  22885
 Copyright terms: Public domain W3C validator