![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > Mathboxes > lkrssv | Structured version Unicode version |
Description: The kernel of a linear functional is a set of vectors. (Contributed by NM, 1-Jan-2015.) |
Ref | Expression |
---|---|
lkrssv.v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lkrssv.f |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lkrssv.k |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lkrssv.w |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lkrssv.g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
lkrssv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lkrssv.w |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | lkrssv.g |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | lkrssv.f |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | lkrssv.k |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eqid 2451 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | lkrlss 33046 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 2, 6 | syl2anc 661 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | lkrssv.v |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 8, 5 | lssss 17124 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 7, 9 | syl 16 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-rep 4501 ax-sep 4511 ax-nul 4519 ax-pow 4568 ax-pr 4629 ax-un 6472 ax-cnex 9439 ax-resscn 9440 ax-1cn 9441 ax-icn 9442 ax-addcl 9443 ax-addrcl 9444 ax-mulcl 9445 ax-mulrcl 9446 ax-mulcom 9447 ax-addass 9448 ax-mulass 9449 ax-distr 9450 ax-i2m1 9451 ax-1ne0 9452 ax-1rid 9453 ax-rnegex 9454 ax-rrecex 9455 ax-cnre 9456 ax-pre-lttri 9457 ax-pre-lttrn 9458 ax-pre-ltadd 9459 ax-pre-mulgt0 9460 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rmo 2803 df-rab 2804 df-v 3070 df-sbc 3285 df-csb 3387 df-dif 3429 df-un 3431 df-in 3433 df-ss 3440 df-pss 3442 df-nul 3736 df-if 3890 df-pw 3960 df-sn 3976 df-pr 3978 df-tp 3980 df-op 3982 df-uni 4190 df-iun 4271 df-br 4391 df-opab 4449 df-mpt 4450 df-tr 4484 df-eprel 4730 df-id 4734 df-po 4739 df-so 4740 df-fr 4777 df-we 4779 df-ord 4820 df-on 4821 df-lim 4822 df-suc 4823 df-xp 4944 df-rel 4945 df-cnv 4946 df-co 4947 df-dm 4948 df-rn 4949 df-res 4950 df-ima 4951 df-iota 5479 df-fun 5518 df-fn 5519 df-f 5520 df-f1 5521 df-fo 5522 df-f1o 5523 df-fv 5524 df-riota 6151 df-ov 6193 df-oprab 6194 df-mpt2 6195 df-om 6577 df-1st 6677 df-2nd 6678 df-recs 6932 df-rdg 6966 df-er 7201 df-map 7316 df-en 7411 df-dom 7412 df-sdom 7413 df-pnf 9521 df-mnf 9522 df-xr 9523 df-ltxr 9524 df-le 9525 df-sub 9698 df-neg 9699 df-nn 10424 df-2 10481 df-ndx 14279 df-slot 14280 df-base 14281 df-sets 14282 df-plusg 14353 df-0g 14482 df-mnd 15517 df-grp 15647 df-minusg 15648 df-sbg 15649 df-mgp 16697 df-ur 16709 df-rng 16753 df-lmod 17056 df-lss 17120 df-lfl 33009 df-lkr 33037 |
This theorem is referenced by: lkrscss 33049 lkrlsp3 33055 lshpkr 33068 lfl1dim 33072 lfl1dim2N 33073 lkrpssN 33114 dochlkr 35336 dochkrsat 35406 dochkrsat2 35407 dochsnkrlem1 35420 dochsnkr 35423 dochfln0 35428 dochkr1 35429 dochkr1OLDN 35430 lcfl4N 35446 lcfl5 35447 lcfl6lem 35449 lcfl6 35451 lcfl9a 35456 lclkrlem2s 35476 lclkrlem2v 35479 lclkrslem1 35488 lclkrslem2 35489 lcfrvalsnN 35492 lcfrlem4 35496 lcfrlem5 35497 lcfrlem6 35498 lcfrlem16 35509 lcfrlem26 35519 lcfrlem36 35529 lcfr 35536 mapdsn 35592 mapdrvallem2 35596 mapd0 35616 hdmaplkr 35867 |
Copyright terms: Public domain | W3C validator |