Theorem nlmlmod 24888

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 2765	. . . 4 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2765	. . . 4 ⊢ (norm‘𝑊) = (norm‘𝑊)
3		eqid 2765	. . . 4 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		eqid 2765	. . . 4 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
5		eqid 2765	. . . 4 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
6		eqid 2765	. . . 4 ⊢ (norm‘(Scalar‘𝑊)) = (norm‘(Scalar‘𝑊))
7	1, 2, 3, 4, 5, 6	isnlm 24885	. . 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 2146  ∀wral 3081  ‘cfv 6540  (class class class)co 7419   · cmul 11122  Basecbs 17293  Scalarcsca 17337   ·_𝑠 cvsca 17338  LModclmod 21033  normcnm 24786  NrmGrpcngp 24787  NrmRingcnrg 24789  NrmModcnlm 24790

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 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-nlm 24796

This theorem is used by:  nlmdsdi  24891  nlmdsdir  24892  nlmmul0or  24893  nlmvscnlem2  24895  nlmvscn  24897  nlmtlm  24904  nvclmod  24908  isnvc2  24909  lssnlm  24911  ngpocelbl  24914  idnmhm  24964  0nmhm  24965  nmhmplusg  24967  nmhmcn  25332  cphlmod  25386  bnlmod  25555  nmmulg  34422