Colors of
variables: wff
setvar class |
Syntax hints:
β wi 4 = wceq 1541
β wcel 2106 βcfv 6543 Scalarcsca 17202
DivRingcdr 20361 LModclmod 20475 LVecclvec 20718 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-ext 2703 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-v 3476 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-iota 6495 df-fv 6551 df-lvec 20719 |
This theorem is referenced by: lsslvec
20725 lvecvs0or
20727 lssvs0or
20729 lvecinv
20732 lspsnvs
20733 lspsneq
20741 lspfixed
20747 lspexch
20748 lspsolv
20762 islbs2
20773 islbs3
20774 obsne0
21286 islinds4
21396 nvctvc
24224 lssnvc
24226 cvsunit
24654 cvsdivcl
24656 cphsubrg
24704 cphreccl
24705 cphqss
24712 phclm
24756 ipcau2
24758 tcphcph
24761 hlprlem
24891 ishl2
24894 quslvec
32516 0nellinds
32528 lmhmlvec2
32763 lfl1
38026 lkrsc
38053 eqlkr3
38057 lkrlsp
38058 lkrshp
38061 lduallvec
38110 dochkr1
40435 dochkr1OLDN
40436 lcfl7lem
40456 lclkrlem2m
40476 lclkrlem2o
40478 lclkrlem2p
40479 lcfrlem1
40499 lcfrlem2
40500 lcfrlem3
40501 lcfrlem29
40528 lcfrlem31
40530 lcfrlem33
40532 mapdpglem17N
40645 mapdpglem18
40646 mapdpglem19
40647 mapdpglem21
40649 mapdpglem22
40650 hdmapip1
40873 hgmapvvlem1
40880 hgmapvvlem2
40881 hgmapvvlem3
40882 prjspersym
41431 lincreslvec3
47241 isldepslvec2
47244 |