Theorem islvec 21048

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 6831	. . . 4 ⊢ (𝑓 = 𝑊 → (Scalar‘𝑓) = (Scalar‘𝑊))
2		islvec.1	. . . 4 ⊢ 𝐹 = (Scalar‘𝑊)
3	1, 2	eqtr4di 2786	. . 3 ⊢ (𝑓 = 𝑊 → (Scalar‘𝑓) = 𝐹)
4	3	eleq1d 2818	. 2 ⊢ (𝑓 = 𝑊 → ((Scalar‘𝑓) ∈ DivRing ↔ 𝐹 ∈ DivRing))
5		df-lvec 21047	. 2 ⊢ LVec = {𝑓 ∈ LMod ∣ (Scalar‘𝑓) ∈ DivRing}
6	4, 5	elrab2 3647	1 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ‘cfv 6489  Scalarcsca 17174  DivRingcdr 20654  LModclmod 20803  LVecclvec 21046

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-lvec 21047

This theorem is referenced by:  lvecdrng  21049  lveclmod  21050  lsslvec  21053  lmhmlvec  21054  lvecprop2d  21113  lvecpropd  21114  rlmlvec  21148  frlmlvec  21708  frlmphl  21728  mpllvec  21967  tvclvec  24124  isnvc2  24624  iscvs  25064  cnstrcvs  25078  zclmncvs  25085  quslvec  33336  ply1lvec  33533  sralvec  33608  matdim  33639  lmhmlvec2  33643  assalactf1o  33659  ccfldsrarelvec  33695  fldextrspunlem1  33699  fldextrspunfld  33700  bj-isvec  37342  lindsdom  37664  lindsenlbs  37665  lduallvec  39263  dvalveclem  41134  dvhlveclem  41217  lmod1zrnlvec  48609  aacllem  49916