Theorem nlmngp 24843

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 24841	. . 3 ⊢ (𝑊 ∈ NrmMod ↔ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NrmRing) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ (Base‘𝑊)((norm‘𝑊)‘(𝑥( ·𝑠 ‘𝑊)𝑦)) = (((norm‘(Scalar‘𝑊))‘𝑥) · ((norm‘𝑊)‘𝑦))))
8	7	simplbi 501	. 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 2143  ∀wral 3079  ‘cfv 6536  (class class class)co 7410   · cmul 11109  Basecbs 17273  Scalarcsca 17317   ·_𝑠 cvsca 17318  LModclmod 20990  normcnm 24742  NrmGrpcngp 24743  NrmRingcnrg 24745  NrmModcnlm 24746

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5269

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rab 3417  df-v 3457  df-sbc 3745  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-nlm 24752

This theorem is used by:  nlmdsdi  24847  nlmdsdir  24848  nlmmul0or  24849  nlmvscnlem2  24851  nlmvscnlem1  24852  nlmvscn  24853  nlmtlm  24860  lssnlm  24867  ngpocelbl  24870  isnmhm2  24918  idnmhm  24920  0nmhm  24921  nmoleub2lem  25282  nmoleub2lem3  25283  nmoleub2lem2  25284  nmoleub3  25287  nmhmcn  25288  ncvsm1  25322  ncvsdif  25323  ncvspi  25324  ncvs1  25325  ncvspds  25329  cphngp  25341  ipcnlem2  25412  ipcnlem1  25413  csscld  25417  bnngp  25510  cssbn  25543