Theorem nlmngp 25023

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.

Step	Hyp	Ref	Expression
1		eqid 2763	. . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2763	. . . 4 ⊢ (norm‘𝑊) = (norm‘𝑊)
3		eqid 2763	. . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2763	. . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2763	. . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2763	. . . 4 ⊢ (norm‘(Scalar‘𝑊)) = (norm‘(Scalar‘𝑊))
7	1, 2, 3, 4, 5, 6	isnlm 25021	. . 3 ⊢ (𝑊 ∈ NrmMod ↔ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NrmRing) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ (Base‘𝑊)((norm‘𝑊)‘(𝑥( ·𝑠 ‘𝑊)𝑦)) = (((norm‘(Scalar‘𝑊))‘𝑥) · ((norm‘𝑊)‘𝑦))))
8	7	simplbi 502	. 2 ⊢ (𝑊 ∈ NrmMod → (𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NrmRing))
9	8	simp1d 1160	1 ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ‘cfv 6555  (class class class)co 7440   · cmul 11229  Basecbs 17413  Scalarcsca 17457   ·_𝑠 cvsca 17458  LModclmod 21162  normcnm 24922  NrmGrpcngp 24923  NrmRingcnrg 24925  NrmModcnlm 24926

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6509  df-fv 6563  df-ov 7443  df-nlm 24932

This theorem is used by:  nlmdsdi  25027  nlmdsdir  25028  nlmmul0or  25029  nlmvscnlem2  25031  nlmvscnlem1  25032  nlmvscn  25033  nlmtlm  25040  lssnlm  25047  ngpocelbl  25050  isnmhm2  25098  idnmhm  25100  0nmhm  25101  nmoleub2lem  25462  nmoleub2lem3  25463  nmoleub2lem2  25464  nmoleub3  25467  nmhmcn  25468  ncvsm1  25502  ncvsdif  25503  ncvspi  25504  ncvs1  25505  ncvspds  25509  cphngp  25521  ipcnlem2  25592  ipcnlem1  25593  csscld  25597  bnngp  25690  cssbn  25723