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

Theorem nlmngp 23599
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 2738 . . . 4 (Base‘𝑊) = (Base‘𝑊)
2 eqid 2738 . . . 4 (norm‘𝑊) = (norm‘𝑊)
3 eqid 2738 . . . 4 ( ·𝑠𝑊) = ( ·𝑠𝑊)
4 eqid 2738 . . . 4 (Scalar‘𝑊) = (Scalar‘𝑊)
5 eqid 2738 . . . 4 (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6 eqid 2738 . . . 4 (norm‘(Scalar‘𝑊)) = (norm‘(Scalar‘𝑊))
71, 2, 3, 4, 5, 6isnlm 23597 . . 3 (𝑊 ∈ NrmMod ↔ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NrmRing) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ (Base‘𝑊)((norm‘𝑊)‘(𝑥( ·𝑠𝑊)𝑦)) = (((norm‘(Scalar‘𝑊))‘𝑥) · ((norm‘𝑊)‘𝑦))))
87simplbi 501 . 2 (𝑊 ∈ NrmMod → (𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NrmRing))
98simp1d 1144 1 (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1089   = wceq 1543  wcel 2111  wral 3062  cfv 6398  (class class class)co 7232   · cmul 10759  Basecbs 16785  Scalarcsca 16830   ·𝑠 cvsca 16831  LModclmod 19924  normcnm 23498  NrmGrpcngp 23499  NrmRingcnrg 23501  NrmModcnlm 23502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-nul 5214
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3423  df-sbc 3710  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4253  df-if 4455  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4835  df-br 5069  df-iota 6356  df-fv 6406  df-ov 7235  df-nlm 23508
This theorem is referenced by:  nlmdsdi  23603  nlmdsdir  23604  nlmmul0or  23605  nlmvscnlem2  23607  nlmvscnlem1  23608  nlmvscn  23609  nlmtlm  23616  lssnlm  23623  ngpocelbl  23626  isnmhm2  23674  idnmhm  23676  0nmhm  23677  nmoleub2lem  24035  nmoleub2lem3  24036  nmoleub2lem2  24037  nmoleub3  24040  nmhmcn  24041  ncvsm1  24075  ncvsdif  24076  ncvspi  24077  ncvs1  24078  ncvspds  24082  cphngp  24094  ipcnlem2  24165  ipcnlem1  24166  csscld  24170  bnngp  24263  cssbn  24296
  Copyright terms: Public domain W3C validator