Theorem islvec 21204

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 2814	. . 3 ⊢ (𝑓 = 𝑊 → (Scalar‘𝑓) = 𝐹)
4	3	eleq1d 2846	. 2 ⊢ (𝑓 = 𝑊 → ((Scalar‘𝑓) ∈ DivRing ↔ 𝐹 ∈ DivRing))
5		df-lvec 21203	. 2 ⊢ LVec = {𝑓 ∈ LMod ∣ (Scalar‘𝑓) ∈ DivRing}
6	4, 5	elrab2 3653	1 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1568   ∈ wcel 2141  ‘cfv 6536  Scalarcsca 17312  DivRingcdr 20812  LModclmod 20960  LVecclvec 21202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3415  df-v 3455  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 21203

This theorem is referenced by:  lvecdrng  21205  lveclmod  21206  lsslvec  21209  lmhmlvec  21210  lvecprop2d  21269  lvecpropd  21270  rlmlvec  21304  frlmlvec  21890  frlmphl  21910  mpllvec  22148  tvclvec  24335  isnvc2  24835  iscvs  25265  cnstrcvs  25279  zclmncvs  25286  quslvec  33646  ply1lvec  33815  sralvec  33941  matdim  33971  lmhmlvec2  33975  assalactf1o  33991  ccfldsrarelvec  34027  fldextrspunlem1  34031  fldextrspunfld  34032  bj-isvec  37897  lindsdom  38231  lindsenlbs  38232  lduallvec  39896  dvalveclem  41767  dvhlveclem  41850  lmod1zrnlvec  49241  aacllem  50568