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 18925 | . 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing)) |
3 | 2 | simprbi 479 | 1 ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 ‘cfv 5804 Scalarcsca 15771 DivRingcdr 18570 LModclmod 18686 LVecclvec 18923 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-iota 5768 df-fv 5812 df-lvec 18924 |
This theorem is referenced by: lsslvec 18928 lvecvs0or 18929 lssvs0or 18931 lvecinv 18934 lspsnvs 18935 lspsneq 18943 lspfixed 18949 lspexch 18950 lspsolv 18964 islbs2 18975 islbs3 18976 obsne0 19888 islinds4 19993 nvctvc 22314 lssnvc 22316 cvsunit 22739 cvsdivcl 22741 cphsubrg 22788 cphreccl 22789 cphqss 22796 tchclm 22839 ipcau2 22841 tchcph 22844 hlprlem 22971 ishl2 22974 lfl1 33375 lkrsc 33402 eqlkr3 33406 lkrlsp 33407 lkrshp 33410 lduallvec 33459 dochkr1 35785 dochkr1OLDN 35786 lcfl7lem 35806 lclkrlem2m 35826 lclkrlem2o 35828 lclkrlem2p 35829 lcfrlem1 35849 lcfrlem2 35850 lcfrlem3 35851 lcfrlem29 35878 lcfrlem31 35880 lcfrlem33 35882 mapdpglem17N 35995 mapdpglem18 35996 mapdpglem19 35997 mapdpglem21 35999 mapdpglem22 36000 hdmapip1 36226 hgmapvvlem1 36233 hgmapvvlem2 36234 hgmapvvlem3 36235 lincreslvec3 42065 isldepslvec2 42068 |
Copyright terms: Public domain | W3C validator |