lvecdrng - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lvecdrng		Structured version Visualization version GIF version

Theorem lvecdrng 19996

Description: The set of scalars of a left vector space is a division ring. (Contributed by NM, 17-Apr-2014.)

**Hypothesis**
Ref	Expression
islvec.1	⊢ 𝐹 = (Scalar‘𝑊)

**Assertion**
Ref	Expression
lvecdrng	⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing)

**Proof of Theorem lvecdrng**
Step	Hyp	Ref	Expression
1		islvec.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
2	1	islvec 19995	. 2 ⊢ (𝑊 ∈ LVec ↔ (𝑊 ∈ LMod ∧ 𝐹 ∈ DivRing))
3	2	simprbi 500	1 ⊢ (𝑊 ∈ LVec → 𝐹 ∈ DivRing)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ‘cfv 6339 Scalarcsca 16671 DivRingcdr 19621 LModclmod 19753 LVecclvec 19993

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-rab 3062 df-v 3400 df-un 3848 df-in 3850 df-ss 3860 df-sn 4517 df-pr 4519 df-op 4523 df-uni 4797 df-br 5031 df-iota 6297 df-fv 6347 df-lvec 19994

This theorem is referenced by: lsslvec 19998 lvecvs0or 19999 lssvs0or 20001 lvecinv 20004 lspsnvs 20005 lspsneq 20013 lspfixed 20019 lspexch 20020 lspsolv 20034 islbs2 20045 islbs3 20046 obsne0 20541 islinds4 20651 nvctvc 23453 lssnvc 23455 cvsunit 23883 cvsdivcl 23885 cphsubrg 23932 cphreccl 23933 cphqss 23940 phclm 23984 ipcau2 23986 tcphcph 23989 hlprlem 24119 ishl2 24122 0nellinds 31138 lmhmlvec2 31274 lfl1 36707 lkrsc 36734 eqlkr3 36738 lkrlsp 36739 lkrshp 36742 lduallvec 36791 dochkr1 39115 dochkr1OLDN 39116 lcfl7lem 39136 lclkrlem2m 39156 lclkrlem2o 39158 lclkrlem2p 39159 lcfrlem1 39179 lcfrlem2 39180 lcfrlem3 39181 lcfrlem29 39208 lcfrlem31 39210 lcfrlem33 39212 mapdpglem17N 39325 mapdpglem18 39326 mapdpglem19 39327 mapdpglem21 39329 mapdpglem22 39330 hdmapip1 39553 hgmapvvlem1 39560 hgmapvvlem2 39561 hgmapvvlem3 39562 prjspersym 40023 lincreslvec3 45357 isldepslvec2 45360