Theorem islvec 21071

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ‘cfv 6541  Scalarcsca 17276  DivRingcdr 20697  LModclmod 20826  LVecclvec 21069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-iota 6494  df-fv 6549  df-lvec 21070

This theorem is referenced by:  lvecdrng  21072  lveclmod  21073  lsslvec  21076  lmhmlvec  21077  lvecprop2d  21136  lvecpropd  21137  rlmlvec  21173  frlmlvec  21735  frlmphl  21755  mpllvec  21994  tvclvec  24153  isnvc2  24656  iscvs  25096  cnstrcvs  25110  zclmncvs  25118  quslvec  33323  ply1lvec  33520  sralvec  33571  matdim  33601  lmhmlvec2  33605  assalactf1o  33621  ccfldsrarelvec  33658  fldextrspunlem1  33662  fldextrspunfld  33663  bj-isvec  37247  lindsdom  37580  lindsenlbs  37581  lduallvec  39114  dvalveclem  40986  dvhlveclem  41069  lmod1zrnlvec  48369  aacllem  49328