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

Theorem tlmtrg 24045
Description: The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015.)
Hypothesis
Ref Expression
tlmtrg.f 𝐹 = (Scalarβ€˜π‘Š)
Assertion
Ref Expression
tlmtrg (π‘Š ∈ TopMod β†’ 𝐹 ∈ TopRing)

Proof of Theorem tlmtrg
StepHypRef Expression
1 eqid 2726 . . . 4 ( Β·sf β€˜π‘Š) = ( Β·sf β€˜π‘Š)
2 eqid 2726 . . . 4 (TopOpenβ€˜π‘Š) = (TopOpenβ€˜π‘Š)
3 tlmtrg.f . . . 4 𝐹 = (Scalarβ€˜π‘Š)
4 eqid 2726 . . . 4 (TopOpenβ€˜πΉ) = (TopOpenβ€˜πΉ)
51, 2, 3, 4istlm 24040 . . 3 (π‘Š ∈ TopMod ↔ ((π‘Š ∈ TopMnd ∧ π‘Š ∈ LMod ∧ 𝐹 ∈ TopRing) ∧ ( Β·sf β€˜π‘Š) ∈ (((TopOpenβ€˜πΉ) Γ—t (TopOpenβ€˜π‘Š)) Cn (TopOpenβ€˜π‘Š))))
65simplbi 497 . 2 (π‘Š ∈ TopMod β†’ (π‘Š ∈ TopMnd ∧ π‘Š ∈ LMod ∧ 𝐹 ∈ TopRing))
76simp3d 1141 1 (π‘Š ∈ TopMod β†’ 𝐹 ∈ TopRing)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  β€˜cfv 6536  (class class class)co 7404  Scalarcsca 17207  TopOpenctopn 17374  LModclmod 20704   Β·sf cscaf 20705   Cn ccn 23079   Γ—t ctx 23415  TopMndctmd 23925  TopRingctrg 24011  TopModctlm 24013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2704  df-cleq 2718  df-clel 2804  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-iota 6488  df-fv 6544  df-ov 7407  df-tlm 24017
This theorem is referenced by:  tlmscatps  24046
  Copyright terms: Public domain W3C validator