Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lvecdrng | Structured version Visualization version GIF version |
Description: The set of scalars of a left vector space is a division ring. (Contributed by NM, 17-Apr-2014.) |
Ref | Expression |
---|---|
islvec.1 | ⊢ 𝐹 = (Scalar‘𝑊) |
Ref | Expression |
---|---|
lvecdrng | ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | islvec.1 | . . 3 ⊢ 𝐹 = (Scalar‘𝑊) | |
2 | 1 | islvec 19879 | . 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing)) |
3 | 2 | simprbi 499 | 1 ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1536 ∈ wcel 2113 ‘cfv 6358 Scalarcsca 16571 DivRingcdr 19505 LModclmod 19637 LVecclvec 19877 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-rab 3150 df-v 3499 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-sn 4571 df-pr 4573 df-op 4577 df-uni 4842 df-br 5070 df-iota 6317 df-fv 6366 df-lvec 19878 |
This theorem is referenced by: lsslvec 19882 lvecvs0or 19883 lssvs0or 19885 lvecinv 19888 lspsnvs 19889 lspsneq 19897 lspfixed 19903 lspexch 19904 lspsolv 19918 islbs2 19929 islbs3 19930 obsne0 20872 islinds4 20982 nvctvc 23312 lssnvc 23314 cvsunit 23738 cvsdivcl 23740 cphsubrg 23787 cphreccl 23788 cphqss 23795 phclm 23838 ipcau2 23840 tcphcph 23843 hlprlem 23973 ishl2 23976 0nellinds 30939 lmhmlvec2 31021 lfl1 36210 lkrsc 36237 eqlkr3 36241 lkrlsp 36242 lkrshp 36245 lduallvec 36294 dochkr1 38618 dochkr1OLDN 38619 lcfl7lem 38639 lclkrlem2m 38659 lclkrlem2o 38661 lclkrlem2p 38662 lcfrlem1 38682 lcfrlem2 38683 lcfrlem3 38684 lcfrlem29 38711 lcfrlem31 38713 lcfrlem33 38715 mapdpglem17N 38828 mapdpglem18 38829 mapdpglem19 38830 mapdpglem21 38832 mapdpglem22 38833 hdmapip1 39056 hgmapvvlem1 39063 hgmapvvlem2 39064 hgmapvvlem3 39065 prjspersym 39263 lincreslvec3 44544 isldepslvec2 44547 |
Copyright terms: Public domain | W3C validator |