Theorem islvec 21144

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

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1554   ∈ wcel 2136  ‘cfv 6510  Scalarcsca 17265  DivRingcdr 20751  LModclmod 20900  LVecclvec 21142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-iota 6466  df-fv 6518  df-lvec 21143

This theorem is referenced by:  lvecdrng  21145  lveclmod  21146  lsslvec  21149  lmhmlvec  21150  lvecprop2d  21209  lvecpropd  21210  rlmlvec  21244  frlmlvec  21786  frlmphl  21806  mpllvec  22044  tvclvec  24232  isnvc2  24732  iscvs  25162  cnstrcvs  25176  zclmncvs  25183  quslvec  33500  ply1lvec  33709  sralvec  33836  matdim  33866  lmhmlvec2  33870  assalactf1o  33886  ccfldsrarelvec  33922  fldextrspunlem1  33926  fldextrspunfld  33927  bj-isvec  37727  lindsdom  38061  lindsenlbs  38062  lduallvec  39726  dvalveclem  41597  dvhlveclem  41680  lmod1zrnlvec  49064  aacllem  50370