MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nlmlmod Unicode version

Theorem nlmlmod 18585
Description: A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)
Assertion
Ref Expression
nlmlmod  |-  ( W  e. NrmMod  ->  W  e.  LMod )

Proof of Theorem nlmlmod
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2387 . . . 4  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2387 . . . 4  |-  ( norm `  W )  =  (
norm `  W )
3 eqid 2387 . . . 4  |-  ( .s
`  W )  =  ( .s `  W
)
4 eqid 2387 . . . 4  |-  (Scalar `  W )  =  (Scalar `  W )
5 eqid 2387 . . . 4  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
6 eqid 2387 . . . 4  |-  ( norm `  (Scalar `  W )
)  =  ( norm `  (Scalar `  W )
)
71, 2, 3, 4, 5, 6isnlm 18582 . . 3  |-  ( W  e. NrmMod 
<->  ( ( W  e. NrmGrp  /\  W  e.  LMod  /\  (Scalar `  W )  e. NrmRing )  /\  A. x  e.  ( Base `  (Scalar `  W ) ) A. y  e.  ( Base `  W ) ( (
norm `  W ) `  ( x ( .s
`  W ) y ) )  =  ( ( ( norm `  (Scalar `  W ) ) `  x )  x.  (
( norm `  W ) `  y ) ) ) )
87simplbi 447 . 2  |-  ( W  e. NrmMod  ->  ( W  e. NrmGrp  /\  W  e.  LMod  /\  (Scalar `  W )  e. NrmRing ) )
98simp2d 970 1  |-  ( W  e. NrmMod  ->  W  e.  LMod )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936    = wceq 1649    e. wcel 1717   A.wral 2649   ` cfv 5394  (class class class)co 6020    x. cmul 8928   Basecbs 13396  Scalarcsca 13459   .scvsca 13460   LModclmod 15877   normcnm 18495  NrmGrpcngp 18496  NrmRingcnrg 18498  NrmModcnlm 18499
This theorem is referenced by:  nlmdsdi  18588  nlmdsdir  18589  nlmmul0or  18590  nlmvscnlem2  18592  nlmvscn  18594  nlmtlm  18600  nvclmod  18604  isnvc2  18605  lssnlm  18607  idnmhm  18659  0nmhm  18660  nmhmplusg  18662  nmoleub2lem3  18994  nmoleub3  18998  nmhmcn  18999  cphlmod  19008  bnlmod  19165  nmmulg  24153
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-nul 4279
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-sbc 3105  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402  df-ov 6023  df-nlm 18505
  Copyright terms: Public domain W3C validator