Theorem nlmngp 24664

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

Syntax hints:   → wi 4   ∧ w3a 1093   = wceq 1548   ∈ wcel 2121  ∀wral 3055  ‘cfv 6489  (class class class)co 7360   · cmul 11038  Basecbs 17174  Scalarcsca 17218   ·_𝑠 cvsca 17219  LModclmod 20854  normcnm 24563  NrmGrpcngp 24564  NrmRingcnrg 24566  NrmModcnlm 24567

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 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-nul 5231

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-ral 3056  df-rab 3394  df-v 3435  df-sbc 3726  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-iota 6445  df-fv 6497  df-ov 7363  df-nlm 24573

This theorem is referenced by:  nlmdsdi  24668  nlmdsdir  24669  nlmmul0or  24670  nlmvscnlem2  24672  nlmvscnlem1  24673  nlmvscn  24674  nlmtlm  24681  lssnlm  24688  ngpocelbl  24691  isnmhm2  24739  idnmhm  24741  0nmhm  24742  nmoleub2lem  25103  nmoleub2lem3  25104  nmoleub2lem2  25105  nmoleub3  25108  nmhmcn  25109  ncvsm1  25143  ncvsdif  25144  ncvspi  25145  ncvs1  25146  ncvspds  25150  cphngp  25162  ipcnlem2  25233  ipcnlem1  25234  csscld  25238  bnngp  25331  cssbn  25364