Theorem nlmngp 24563

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 2729	. . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2729	. . . 4 ⊢ (norm‘𝑊) = (norm‘𝑊)
3		eqid 2729	. . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2729	. . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2729	. . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2729	. . . 4 ⊢ (norm‘(Scalar‘𝑊)) = (norm‘(Scalar‘𝑊))
7	1, 2, 3, 4, 5, 6	isnlm 24561	. . 3 ⊢ (𝑊 ∈ NrmMod ↔ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NrmRing) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑊))∀𝑦 ∈ (Base‘𝑊)((norm‘𝑊)‘(𝑥( ·𝑠 ‘𝑊)𝑦)) = (((norm‘(Scalar‘𝑊))‘𝑥) · ((norm‘𝑊)‘𝑦))))
8	7	simplbi 497	. 2 ⊢ (𝑊 ∈ NrmMod → (𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NrmRing))
9	8	simp1d 1142	1 ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ‘cfv 6482  (class class class)co 7349   · cmul 11014  Basecbs 17120  Scalarcsca 17164   ·_𝑠 cvsca 17165  LModclmod 20763  normcnm 24462  NrmGrpcngp 24463  NrmRingcnrg 24465  NrmModcnlm 24466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5245

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-nlm 24472

This theorem is referenced by:  nlmdsdi  24567  nlmdsdir  24568  nlmmul0or  24569  nlmvscnlem2  24571  nlmvscnlem1  24572  nlmvscn  24573  nlmtlm  24580  lssnlm  24587  ngpocelbl  24590  isnmhm2  24638  idnmhm  24640  0nmhm  24641  nmoleub2lem  25012  nmoleub2lem3  25013  nmoleub2lem2  25014  nmoleub3  25017  nmhmcn  25018  ncvsm1  25052  ncvsdif  25053  ncvspi  25054  ncvs1  25055  ncvspds  25059  cphngp  25071  ipcnlem2  25142  ipcnlem1  25143  csscld  25147  bnngp  25240  cssbn  25273