| 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 21103 | . 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing)) |
| 3 | 2 | simprbi 496 | 1 ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 ‘cfv 6561 Scalarcsca 17300 DivRingcdr 20729 LModclmod 20858 LVecclvec 21101 |
| 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 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-iota 6514 df-fv 6569 df-lvec 21102 |
| This theorem is referenced by: lsslvec 21108 lvecvs0or 21110 lssvs0or 21112 lvecinv 21115 lspsnvs 21116 lspsneq 21124 lspfixed 21130 lspexch 21131 lspsolv 21145 islbs2 21156 islbs3 21157 obsne0 21745 islinds4 21855 nvctvc 24721 lssnvc 24723 cvsunit 25164 cvsdivcl 25166 cphsubrg 25214 cphreccl 25215 cphqss 25222 phclm 25266 ipcau2 25268 tcphcph 25271 hlprlem 25401 ishl2 25404 quslvec 33388 0nellinds 33398 lmhmlvec2 33670 dimlssid 33683 lfl1 39071 lkrsc 39098 eqlkr3 39102 lkrlsp 39103 lkrshp 39106 lduallvec 39155 dochkr1 41480 dochkr1OLDN 41481 lcfl7lem 41501 lclkrlem2m 41521 lclkrlem2o 41523 lclkrlem2p 41524 lcfrlem1 41544 lcfrlem2 41545 lcfrlem3 41546 lcfrlem29 41573 lcfrlem31 41575 lcfrlem33 41577 mapdpglem17N 41690 mapdpglem18 41691 mapdpglem19 41692 mapdpglem21 41694 mapdpglem22 41695 hdmapip1 41918 hgmapvvlem1 41925 hgmapvvlem2 41926 hgmapvvlem3 41927 prjspersym 42617 lincreslvec3 48399 isldepslvec2 48402 |
| Copyright terms: Public domain | W3C validator |