Colors of
variables: wff
setvar class |
Syntax hints:
β wi 4 β 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: lveclmodd
20583 lsslvec
20584 lvecvs0or
20585 lssvs0or
20587 lvecvscan
20588 lvecvscan2
20589 lvecinv
20590 lspsnvs
20591 lspsneleq
20592 lspsncmp
20593 lspsnne1
20594 lspsnnecom
20596 lspabs2
20597 lspabs3
20598 lspsneq
20599 lspsnel4
20601 lspdisj
20602 lspdisjb
20603 lspdisj2
20604 lspfixed
20605 lspexch
20606 lspexchn1
20607 lspindpi
20609 lvecindp
20615 lvecindp2
20616 lsmcv
20618 lspsolv
20620 lssacsex
20621 lspsnat
20622 lsppratlem2
20625 lsppratlem3
20626 lsppratlem4
20627 lsppratlem6
20629 lspprat
20630 islbs2
20631 islbs3
20632 lbsacsbs
20633 lbsextlem2
20636 lbsextlem3
20637 lbsextlem4
20638 phllmod
21050 isphld
21074 islinds4
21257 lvecisfrlm
21265 cvsi
24509 0nellinds
32206 lindssn
32213 linds2eq
32216 lvecdim0i
32358 lssdimle
32360 tngdim
32365 matdim
32367 lbslsat
32368 lsatdim
32369 drngdimgt0
32370 lindsunlem
32376 lindsun
32377 lbsdiflsp0
32378 dimkerim
32379 qusdimsum
32380 fedgmullem1
32381 fedgmullem2
32382 fedgmul
32383 extdg1id
32409 ccfldextdgrr
32413 lindsadd
36117 lshpnelb
37492 lshpnel2N
37493 lshpdisj
37495 lshpcmp
37496 lsatcmp
37511 lsatcmp2
37512 lsatel
37513 lsatelbN
37514 lsatfixedN
37517 lsmcv2
37537 lsatcv0
37539 lsatcveq0
37540 lsat0cv
37541 lcvp
37548 lcv1
37549 lcv2
37550 lsatexch
37551 lsatnem0
37553 lsatexch1
37554 lsatcv0eq
37555 lsatcv1
37556 lsatcvatlem
37557 lsatcvat
37558 lsatcvat2
37559 lsatcvat3
37560 islshpcv
37561 l1cvpat
37562 l1cvat
37563 lfl1
37578 lkrsc
37605 lkrscss
37606 eqlkr
37607 eqlkr3
37609 lkrlsp
37610 lkrlsp3
37612 lkrshp
37613 lkrshp3
37614 lkrshpor
37615 lkrshp4
37616 lshpsmreu
37617 lshpkrlem1
37618 lshpkrlem4
37621 lshpkrlem5
37622 lshpkrlem6
37623 lshpkr
37625 lshpkrex
37626 lfl1dim
37629 lfl1dim2N
37630 lduallvec
37662 lduallkr3
37670 lkrpssN
37671 ldual1dim
37674 lkrss2N
37677 lkreqN
37678 lkrlspeqN
37679 dva0g
39536 dia1dim2
39571 dia1dimid
39572 dia2dimlem5
39577 dia2dimlem7
39579 dia2dimlem9
39581 dia2dimlem10
39582 dia2dimlem13
39585 dvhlmod
39619 diblsmopel
39680 lclkrlem2m
40028 lclkrlem2n
40029 lcfrlem1
40051 lcfrlem2
40052 lcfrlem3
40053 lcdlmod
40101 baerlem3lem1
40216 baerlem5alem1
40217 baerlem5blem1
40218 baerlem3lem2
40219 baerlem5alem2
40220 baerlem5blem2
40221 baerlem5amN
40225 baerlem5bmN
40226 baerlem5abmN
40227 mapdindp0
40228 mapdindp1
40229 mapdindp2
40230 mapdindp3
40231 mapdindp4
40232 lspindp5
40279 lvecgrp
40766 lvecring
40768 prjspersym
40988 prjsper
40989 prjspreln0
40990 prjspvs
40991 prjspeclsp
40993 0prjspn
41009 lincreslvec3
46649 isldepslvec2
46652 lindssnlvec
46653 lvecpsslmod
46674 |