Theorem islvec 21380

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ‘cfv 6538  Scalarcsca 17432  DivRingcdr 20981  LModclmod 21136  LVecclvec 21378

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-lvec 21379

This theorem is used by:  lvecdrng  21381  lveclmod  21382  lsslvec  21385  lmhmlvec  21386  lvecprop2d  21445  lvecpropd  21446  rlmlvec  21480  frlmlvec  22068  frlmphl  22088  lindsdom  22157  lindsenlbs  22158  mpllvec  22328  tvclvec  24519  isnvc2  25019  iscvs  25449  cnstrcvs  25463  zclmncvs  25470  quslvec  33964  ply1lvec  34134  sralvec  34260  matdim  34290  lmhmlvec2  34294  assalactf1o  34310  ccfldsrarelvec  34346  fldextrspunlem1  34350  fldextrspunfld  34351  bj-isvec  38284  lduallvec  40287  dvalveclem  42158  dvhlveclem  42241  lmod1zrnlvec  49682  aacllem  51015