Theorem islvec 21101

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

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ‘cfv 6492  Scalarcsca 17221  DivRingcdr 20708  LModclmod 20857  LVecclvec 21099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-lvec 21100

This theorem is referenced by:  lvecdrng  21102  lveclmod  21103  lsslvec  21106  lmhmlvec  21107  lvecprop2d  21166  lvecpropd  21167  rlmlvec  21201  frlmlvec  21743  frlmphl  21763  mpllvec  22001  tvclvec  24189  isnvc2  24689  iscvs  25119  cnstrcvs  25133  zclmncvs  25140  quslvec  33450  ply1lvec  33649  sralvec  33776  matdim  33806  lmhmlvec2  33810  assalactf1o  33826  ccfldsrarelvec  33862  fldextrspunlem1  33866  fldextrspunfld  33867  bj-isvec  37648  lindsdom  37982  lindsenlbs  37983  lduallvec  39647  dvalveclem  41518  dvhlveclem  41601  lmod1zrnlvec  48986  aacllem  50292