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

Theorem nlmngp 24638
Description: A normed module is a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.)
Assertion
Ref Expression
nlmngp (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp)

Proof of Theorem nlmngp
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2725 . . . 4 (Base‘𝑊) = (Base‘𝑊)
2 eqid 2725 . . . 4 (norm‘𝑊) = (norm‘𝑊)
3 eqid 2725 . . . 4 ( ·𝑠𝑊) = ( ·𝑠𝑊)
4 eqid 2725 . . . 4 (Scalar‘𝑊) = (Scalar‘𝑊)
5 eqid 2725 . . . 4 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6 eqid 2725 . . . 4 (norm‘(Scalar‘𝑊)) = (norm‘(Scalar‘𝑊))
71, 2, 3, 4, 5, 6isnlm 24636 . . 3 (𝑊 ∈ NrmMod ↔ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NrmRing) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ (Base‘𝑊)((norm‘𝑊)‘(𝑥( ·𝑠𝑊)𝑦)) = (((norm‘(Scalar‘𝑊))‘𝑥) · ((norm‘𝑊)‘𝑦))))
87simplbi 496 . 2 (𝑊 ∈ NrmMod → (𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NrmRing))
98simp1d 1139 1 (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084   = wceq 1533  wcel 2098  wral 3050  cfv 6549  (class class class)co 7419   · cmul 11145  Basecbs 17183  Scalarcsca 17239   ·𝑠 cvsca 17240  LModclmod 20755  normcnm 24529  NrmGrpcngp 24530  NrmRingcnrg 24532  NrmModcnlm 24533
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 2696  ax-nul 5307
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-ral 3051  df-rab 3419  df-v 3463  df-sbc 3774  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-ov 7422  df-nlm 24539
This theorem is referenced by:  nlmdsdi  24642  nlmdsdir  24643  nlmmul0or  24644  nlmvscnlem2  24646  nlmvscnlem1  24647  nlmvscn  24648  nlmtlm  24655  lssnlm  24662  ngpocelbl  24665  isnmhm2  24713  idnmhm  24715  0nmhm  24716  nmoleub2lem  25085  nmoleub2lem3  25086  nmoleub2lem2  25087  nmoleub3  25090  nmhmcn  25091  ncvsm1  25126  ncvsdif  25127  ncvspi  25128  ncvs1  25129  ncvspds  25133  cphngp  25145  ipcnlem2  25216  ipcnlem1  25217  csscld  25221  bnngp  25314  cssbn  25347
  Copyright terms: Public domain W3C validator