![]() |
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 20703 | . 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing)) |
3 | 2 | simprbi 498 | 1 ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 ‘cfv 6540 Scalarcsca 17196 DivRingcdr 20304 LModclmod 20459 LVecclvec 20701 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-iota 6492 df-fv 6548 df-lvec 20702 |
This theorem is referenced by: lsslvec 20707 lvecvs0or 20709 lssvs0or 20711 lvecinv 20714 lspsnvs 20715 lspsneq 20723 lspfixed 20729 lspexch 20730 lspsolv 20744 islbs2 20755 islbs3 20756 obsne0 21264 islinds4 21374 nvctvc 24199 lssnvc 24201 cvsunit 24629 cvsdivcl 24631 cphsubrg 24679 cphreccl 24680 cphqss 24687 phclm 24731 ipcau2 24733 tcphcph 24736 hlprlem 24866 ishl2 24869 quslvec 32440 0nellinds 32452 lmhmlvec2 32649 lfl1 37878 lkrsc 37905 eqlkr3 37909 lkrlsp 37910 lkrshp 37913 lduallvec 37962 dochkr1 40287 dochkr1OLDN 40288 lcfl7lem 40308 lclkrlem2m 40328 lclkrlem2o 40330 lclkrlem2p 40331 lcfrlem1 40351 lcfrlem2 40352 lcfrlem3 40353 lcfrlem29 40380 lcfrlem31 40382 lcfrlem33 40384 mapdpglem17N 40497 mapdpglem18 40498 mapdpglem19 40499 mapdpglem21 40501 mapdpglem22 40502 hdmapip1 40725 hgmapvvlem1 40732 hgmapvvlem2 40733 hgmapvvlem3 40734 prjspersym 41293 lincreslvec3 47065 isldepslvec2 47068 |
Copyright terms: Public domain | W3C validator |