Theorem lmodvscld 20981

Description: Closure of scalar product for a left module. (Contributed by SN, 15-Mar-2025.)

Hypotheses

Ref	Expression
lmodvscld.v	⊢ 𝑉 = (Base‘𝑊)
lmodvscld.f	⊢ 𝐹 = (Scalar‘𝑊)
lmodvscld.s	⊢ · = ( ·𝑠 ‘𝑊)
lmodvscld.k	⊢ 𝐾 = (Base‘𝐹)
lmodvscld.w	⊢ (𝜑 → 𝑊 ∈ LMod)
lmodvscld.r	⊢ (𝜑 → 𝑅 ∈ 𝐾)
lmodvscld.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)

Assertion

Ref	Expression
lmodvscld	⊢ (𝜑 → (𝑅 · 𝑋) ∈ 𝑉)

Proof of Theorem lmodvscld

Step	Hyp	Ref	Expression
1		lmodvscld.w	. 2 ⊢ (𝜑 → 𝑊 ∈ LMod)
2		lmodvscld.r	. 2 ⊢ (𝜑 → 𝑅 ∈ 𝐾)
3		lmodvscld.x	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
4		lmodvscld.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
5		lmodvscld.f	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
6		lmodvscld.s	. . 3 ⊢ · = ( ·𝑠 ‘𝑊)
7		lmodvscld.k	. . 3 ⊢ 𝐾 = (Base‘𝐹)
8	4, 5, 6, 7	lmodvscl 20980	. 2 ⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝑅 · 𝑋) ∈ 𝑉)
9	1, 2, 3, 8	syl3anc 1398	1 ⊢ (𝜑 → (𝑅 · 𝑋) ∈ 𝑉)

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  Scalarcsca 17314   ·_𝑠 cvsca 17315  LModclmod 20962

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 5270

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 3746  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415  df-lmod 20964

This theorem is referenced by:  assa2ass2  21995  selvvvval  22274  mhpvscacl  22298  ply1vscl  22522  ressasclcl  33842  ply1coedeg  33860  q1pvsca  33875  r1pvsca  33876  r1plmhm  33880  vietalem  33950  ply1degltdimlem  33993  lactlmhm  34005  extdgfialglem2  34064  algextdeglem8  34095  frlmsnic  43291  prjspvs  43325  prjspeclsp  43327  asclelbasALT  49767