Colors of
variables: wff
setvar class |
Syntax hints:
β wi 4 = wceq 1542
β wcel 2107 βcfv 6497 Scalarcsca 17141
DivRingcdr 20197 LModclmod 20336 LVecclvec 20578 |
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 3407 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-iota 6449 df-fv 6505 df-lvec 20579 |
This theorem is referenced by: lsslvec
20584 lvecvs0or
20585 lssvs0or
20587 lvecinv
20590 lspsnvs
20591 lspsneq
20599 lspfixed
20605 lspexch
20606 lspsolv
20620 islbs2
20631 islbs3
20632 obsne0
21147 islinds4
21257 nvctvc
24080 lssnvc
24082 cvsunit
24510 cvsdivcl
24512 cphsubrg
24560 cphreccl
24561 cphqss
24568 phclm
24612 ipcau2
24614 tcphcph
24617 hlprlem
24747 ishl2
24750 0nellinds
32206 lmhmlvec2
32371 lfl1
37578 lkrsc
37605 eqlkr3
37609 lkrlsp
37610 lkrshp
37613 lduallvec
37662 dochkr1
39987 dochkr1OLDN
39988 lcfl7lem
40008 lclkrlem2m
40028 lclkrlem2o
40030 lclkrlem2p
40031 lcfrlem1
40051 lcfrlem2
40052 lcfrlem3
40053 lcfrlem29
40080 lcfrlem31
40082 lcfrlem33
40084 mapdpglem17N
40197 mapdpglem18
40198 mapdpglem19
40199 mapdpglem21
40201 mapdpglem22
40202 hdmapip1
40425 hgmapvvlem1
40432 hgmapvvlem2
40433 hgmapvvlem3
40434 prjspersym
40988 lincreslvec3
46649 isldepslvec2
46652 |