MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  islvec Structured version   Visualization version   GIF version

Theorem islvec 20703
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.
StepHypRef Expression
1 fveq2 6888 . . . 4 (𝑓 = 𝑊 → (Scalar‘𝑓) = (Scalar‘𝑊))
2 islvec.1 . . . 4 𝐹 = (Scalar‘𝑊)
31, 2eqtr4di 2791 . . 3 (𝑓 = 𝑊 → (Scalar‘𝑓) = 𝐹)
43eleq1d 2819 . 2 (𝑓 = 𝑊 → ((Scalar‘𝑓) ∈ DivRing ↔ 𝐹 ∈ DivRing))
5 df-lvec 20702 . 2 LVec = {𝑓 ∈ LMod ∣ (Scalar‘𝑓) ∈ DivRing}
64, 5elrab2 3685 1 (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397   = wceq 1542  wcel 2107  cfv 6540  Scalarcsca 17196  DivRingcdr 20304  LModclmod 20459  LVecclvec 20701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-lvec 20702
This theorem is referenced by:  lvecdrng  20704  lveclmod  20705  lsslvec  20707  lmhmlvec  20708  lvecprop2d  20767  lvecpropd  20768  rlmlvec  20815  frlmlvec  21300  frlmphl  21320  mpllvec  21561  tvclvec  23685  isnvc2  24198  iscvs  24625  cnstrcvs  24639  zclmncvs  24647  quslvec  32440  ply1lvec  32590  sralvec  32621  matdim  32645  lmhmlvec2  32649  ccfldsrarelvec  32690  bj-isvec  36106  lindsdom  36420  lindsenlbs  36421  lduallvec  37962  dvalveclem  39834  dvhlveclem  39917  lmod1zrnlvec  47077  aacllem  47750
  Copyright terms: Public domain W3C validator