Theorem islvec 21236

Description: The predicate "is a left vector space". (Contributed by NM, 11-Nov-2013.)

Hypothesis

Ref	Expression
islvec.1	⊢ 𝐹 = (Scalar‘𝑊)

Assertion

Ref	Expression
islvec	⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))

Proof of Theorem islvec

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6881	. . . 4 ⊢ (𝑓 = 𝑊 → (Scalar‘𝑓) = (Scalar‘𝑊))
2		islvec.1	. . . 4 ⊢ 𝐹 = (Scalar‘𝑊)
3	1, 2	eqtr4di 2815	. . 3 ⊢ (𝑓 = 𝑊 → (Scalar‘𝑓) = 𝐹)
4	3	eleq1d 2847	. 2 ⊢ (𝑓 = 𝑊 → ((Scalar‘𝑓) ∈ DivRing ↔ 𝐹 ∈ DivRing))
5		df-lvec 21235	. 2 ⊢ LVec = {𝑓 ∈ LMod ∣ (Scalar‘𝑓) ∈ DivRing}
6	4, 5	elrab2 3653	1 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400   = wceq 1569   ∈ wcel 2142  ‘cfv 6536  Scalarcsca 17319  DivRingcdr 20838  LModclmod 20992  LVecclvec 21234

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-lvec 21235

This theorem is used by:  lvecdrng  21237  lveclmod  21238  lsslvec  21241  lmhmlvec  21242  lvecprop2d  21301  lvecpropd  21302  rlmlvec  21336  frlmlvec  21922  frlmphl  21942  mpllvec  22180  tvclvec  24367  isnvc2  24867  iscvs  25297  cnstrcvs  25311  zclmncvs  25318  quslvec  33689  ply1lvec  33858  sralvec  33984  matdim  34014  lmhmlvec2  34018  assalactf1o  34034  ccfldsrarelvec  34070  fldextrspunlem1  34074  fldextrspunfld  34075  bj-isvec  37959  lindsdom  38293  lindsenlbs  38294  lduallvec  39956  dvalveclem  41827  dvhlveclem  41910  lmod1zrnlvec  49302  aacllem  50649