Theorem nlmlmod 24997

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 2761	. . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2761	. . . 4 ⊢ (norm‘𝑊) = (norm‘𝑊)
3		eqid 2761	. . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2761	. . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2761	. . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2761	. . . 4 ⊢ (norm‘(Scalar‘𝑊)) = (norm‘(Scalar‘𝑊))
7	1, 2, 3, 4, 5, 6	isnlm 24994	. . 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	simp2d 1161	1 ⊢ (𝑊 ∈ NrmMod → 𝑊 ∈ LMod)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ‘cfv 6538  (class class class)co 7420   · cmul 11205  Basecbs 17387  Scalarcsca 17431   ·_𝑠 cvsca 17432  LModclmod 21135  normcnm 24895  NrmGrpcngp 24896  NrmRingcnrg 24898  NrmModcnlm 24899

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 2733  ax-nul 5260

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-nlm 24905

This theorem is used by:  nlmdsdi  25000  nlmdsdir  25001  nlmmul0or  25002  nlmvscnlem2  25004  nlmvscn  25006  nlmtlm  25013  nvclmod  25017  isnvc2  25018  lssnlm  25020  ngpocelbl  25023  idnmhm  25073  0nmhm  25074  nmhmplusg  25076  nmhmcn  25441  cphlmod  25495  bnlmod  25664  nmmulg  34598