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

Theorem islvec 18867
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 6084 . . . 4 (𝑓 = 𝑊 → (Scalar‘𝑓) = (Scalar‘𝑊))
2 islvec.1 . . . 4 𝐹 = (Scalar‘𝑊)
31, 2syl6eqr 2657 . . 3 (𝑓 = 𝑊 → (Scalar‘𝑓) = 𝐹)
43eleq1d 2667 . 2 (𝑓 = 𝑊 → ((Scalar‘𝑓) ∈ DivRing ↔ 𝐹 ∈ DivRing))
5 df-lvec 18866 . 2 LVec = {𝑓 ∈ LMod ∣ (Scalar‘𝑓) ∈ DivRing}
64, 5elrab2 3328 1 (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382   = wceq 1474  wcel 1975  cfv 5786  Scalarcsca 15713  DivRingcdr 18512  LModclmod 18628  LVecclvec 18865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-iota 5750  df-fv 5794  df-lvec 18866
This theorem is referenced by:  lvecdrng  18868  lveclmod  18869  lsslvec  18870  lvecprop2d  18929  lvecpropd  18930  rlmlvec  18969  frlmphl  19877  tvclvec  21750  isnvc2  22242  iscvs  22660  cnstrcvs  22674  lindsdom  32372  lindsenlbs  32373  lduallvec  33258  dvalveclem  35131  dvhlveclem  35214  lmod1zrnlvec  42075  aacllem  42315
  Copyright terms: Public domain W3C validator