Theorem islvec 21060

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ‘cfv 6493  Scalarcsca 17184  DivRingcdr 20666  LModclmod 20815  LVecclvec 21058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-lvec 21059

This theorem is referenced by:  lvecdrng  21061  lveclmod  21062  lsslvec  21065  lmhmlvec  21066  lvecprop2d  21125  lvecpropd  21126  rlmlvec  21160  frlmlvec  21720  frlmphl  21740  mpllvec  21979  tvclvec  24147  isnvc2  24647  iscvs  25087  cnstrcvs  25101  zclmncvs  25108  quslvec  33422  ply1lvec  33621  sralvec  33722  matdim  33753  lmhmlvec2  33757  assalactf1o  33773  ccfldsrarelvec  33809  fldextrspunlem1  33813  fldextrspunfld  33814  bj-isvec  37463  lindsdom  37786  lindsenlbs  37787  lduallvec  39451  dvalveclem  41322  dvhlveclem  41405  lmod1zrnlvec  48776  aacllem  50082