Theorem islvec 21121

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ‘cfv 6563  Scalarcsca 17301  DivRingcdr 20746  LModclmod 20875  LVecclvec 21119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-lvec 21120

This theorem is referenced by:  lvecdrng  21122  lveclmod  21123  lsslvec  21126  lmhmlvec  21127  lvecprop2d  21186  lvecpropd  21187  rlmlvec  21229  frlmlvec  21799  frlmphl  21819  mpllvec  22058  tvclvec  24223  isnvc2  24736  iscvs  25174  cnstrcvs  25188  zclmncvs  25196  quslvec  33368  ply1lvec  33565  sralvec  33615  matdim  33643  lmhmlvec2  33647  assalactf1o  33663  ccfldsrarelvec  33696  bj-isvec  37270  lindsdom  37601  lindsenlbs  37602  lduallvec  39136  dvalveclem  41008  dvhlveclem  41091  lmod1zrnlvec  48340  aacllem  49032