Theorem nlmngp 24902

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 2762	. . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2762	. . . 4 ⊢ (norm‘𝑊) = (norm‘𝑊)
3		eqid 2762	. . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2762	. . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2762	. . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2762	. . . 4 ⊢ (norm‘(Scalar‘𝑊)) = (norm‘(Scalar‘𝑊))
7	1, 2, 3, 4, 5, 6	isnlm 24900	. . 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 2145  ∀wral 3078  ‘cfv 6537  (class class class)co 7416   · cmul 11130  Basecbs 17303  Scalarcsca 17347   ·_𝑠 cvsca 17348  LModclmod 21043  normcnm 24801  NrmGrpcngp 24802  NrmRingcnrg 24804  NrmModcnlm 24805

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

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 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419  df-nlm 24811

This theorem is used by:  nlmdsdi  24906  nlmdsdir  24907  nlmmul0or  24908  nlmvscnlem2  24910  nlmvscnlem1  24911  nlmvscn  24912  nlmtlm  24919  lssnlm  24926  ngpocelbl  24929  isnmhm2  24977  idnmhm  24979  0nmhm  24980  nmoleub2lem  25341  nmoleub2lem3  25342  nmoleub2lem2  25343  nmoleub3  25346  nmhmcn  25347  ncvsm1  25381  ncvsdif  25382  ncvspi  25383  ncvs1  25384  ncvspds  25388  cphngp  25400  ipcnlem2  25471  ipcnlem1  25472  csscld  25476  bnngp  25569  cssbn  25602