Theorem islvec 19944

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

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ‘cfv 6335  Scalarcsca 16626  DivRingcdr 19570  LModclmod 19702  LVecclvec 19942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-rab 3079  df-v 3411  df-un 3863  df-in 3865  df-ss 3875  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-iota 6294  df-fv 6343  df-lvec 19943

This theorem is referenced by:  lvecdrng  19945  lveclmod  19946  lsslvec  19947  lvecprop2d  20006  lvecpropd  20007  rlmlvec  20046  frlmlvec  20526  frlmphl  20546  mpllvec  20784  tvclvec  22899  isnvc2  23401  iscvs  23828  cnstrcvs  23842  zclmncvs  23849  sralvec  31196  matdim  31219  lmhmlvec2  31223  ccfldsrarelvec  31262  bj-isvec  34982  lindsdom  35331  lindsenlbs  35332  lduallvec  36730  dvalveclem  38601  dvhlveclem  38684  lmhmlvec  39768  lmod1zrnlvec  45268  aacllem  45720