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

Theorem islvec 19227
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 6304 . . . 4 (𝑓 = 𝑊 → (Scalar‘𝑓) = (Scalar‘𝑊))
2 islvec.1 . . . 4 𝐹 = (Scalar‘𝑊)
31, 2syl6eqr 2776 . . 3 (𝑓 = 𝑊 → (Scalar‘𝑓) = 𝐹)
43eleq1d 2788 . 2 (𝑓 = 𝑊 → ((Scalar‘𝑓) ∈ DivRing ↔ 𝐹 ∈ DivRing))
5 df-lvec 19226 . 2 LVec = {𝑓 ∈ LMod ∣ (Scalar‘𝑓) ∈ DivRing}
64, 5elrab2 3472 1 (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1596  wcel 2103  cfv 6001  Scalarcsca 16067  DivRingcdr 18870  LModclmod 18986  LVecclvec 19225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-rex 3020  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-br 4761  df-iota 5964  df-fv 6009  df-lvec 19226
This theorem is referenced by:  lvecdrng  19228  lveclmod  19229  lsslvec  19230  lvecprop2d  19289  lvecpropd  19290  rlmlvec  19329  frlmphl  20243  tvclvec  22124  isnvc2  22625  iscvs  23048  cnstrcvs  23062  zclmncvs  23069  lindsdom  33635  lindsenlbs  33636  lduallvec  34861  dvalveclem  36733  dvhlveclem  36816  lmod1zrnlvec  42710  aacllem  42977
  Copyright terms: Public domain W3C validator