Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lvecdrng | Structured version Visualization version Unicode 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | islvec.1 | . . 3 Scalar | |
2 | 1 | islvec 19104 | . 2 |
3 | 2 | simprbi 480 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 wcel 1990 cfv 5888 Scalarcsca 15944 cdr 18747 clmod 18863 clvec 19102 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-lvec 19103 |
This theorem is referenced by: lsslvec 19107 lvecvs0or 19108 lssvs0or 19110 lvecinv 19113 lspsnvs 19114 lspsneq 19122 lspfixed 19128 lspexch 19129 lspsolv 19143 islbs2 19154 islbs3 19155 obsne0 20069 islinds4 20174 nvctvc 22504 lssnvc 22506 cvsunit 22931 cvsdivcl 22933 cphsubrg 22980 cphreccl 22981 cphqss 22988 tchclm 23031 ipcau2 23033 tchcph 23036 hlprlem 23163 ishl2 23166 lfl1 34357 lkrsc 34384 eqlkr3 34388 lkrlsp 34389 lkrshp 34392 lduallvec 34441 dochkr1 36767 dochkr1OLDN 36768 lcfl7lem 36788 lclkrlem2m 36808 lclkrlem2o 36810 lclkrlem2p 36811 lcfrlem1 36831 lcfrlem2 36832 lcfrlem3 36833 lcfrlem29 36860 lcfrlem31 36862 lcfrlem33 36864 mapdpglem17N 36977 mapdpglem18 36978 mapdpglem19 36979 mapdpglem21 36981 mapdpglem22 36982 hdmapip1 37208 hgmapvvlem1 37215 hgmapvvlem2 37216 hgmapvvlem3 37217 lincreslvec3 42271 isldepslvec2 42274 |
Copyright terms: Public domain | W3C validator |