Theorem nlmlmod 24835

Description: A normed module is a left module. (Contributed by Mario Carneiro, 4-Oct-2015.)

Assertion

Ref	Expression
nlmlmod	⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod)

Proof of Theorem nlmlmod

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 24832	. . 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	simp2d 1161	1 ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod)

Syntax hints:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ‘cfv 6536  (class class class)co 7410   · cmul 11100  Basecbs 17264  Scalarcsca 17308   ·_𝑠 cvsca 17309  LModclmod 20981  normcnm 24733  NrmGrpcngp 24734  NrmRingcnrg 24736  NrmModcnlm 24737

This theorem was proved from 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 theorem 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 24743

This theorem is referenced by:  nlmdsdi  24838  nlmdsdir  24839  nlmmul0or  24840  nlmvscnlem2  24842  nlmvscn  24844  nlmtlm  24851  nvclmod  24855  isnvc2  24856  lssnlm  24858  ngpocelbl  24861  idnmhm  24911  0nmhm  24912  nmhmplusg  24914  nmhmcn  25279  cphlmod  25333  bnlmod  25502  nmmulg  34356