Theorem islvec 21292

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 6882	. . . 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 21291	. 2 ⊢ LVec = {𝑓 ∈ LMod ∣ (Scalar‘𝑓) ∈ DivRing}
6	4, 5	elrab2 3652	1 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  Scalarcsca 17349  DivRingcdr 20894  LModclmod 21048  LVecclvec 21290

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-lvec 21291

This theorem is used by:  lvecdrng  21293  lveclmod  21294  lsslvec  21297  lmhmlvec  21298  lvecprop2d  21357  lvecpropd  21358  rlmlvec  21392  frlmlvec  21978  frlmphl  21998  lindsdom  22067  lindsenlbs  22068  mpllvec  22238  tvclvec  24429  isnvc2  24929  iscvs  25359  cnstrcvs  25373  zclmncvs  25380  quslvec  33802  ply1lvec  33971  sralvec  34097  matdim  34127  lmhmlvec2  34131  assalactf1o  34147  ccfldsrarelvec  34183  fldextrspunlem1  34187  fldextrspunfld  34188  bj-isvec  38041  lduallvec  40029  dvalveclem  41900  dvhlveclem  41983  lmod1zrnlvec  49426  aacllem  50774