![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > Mathboxes > lcdlss | Structured version Unicode version |
Description: Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015.) |
Ref | Expression |
---|---|
lcdlss.h |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcdlss.o |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcdlss.c |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcdlss.s |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcdlss.u |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcdlss.f |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcdlss.l |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcdlss.d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcdlss.t |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcdlss.b |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcdlss.k |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
lcdlss |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcdlss.s |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | lcdlss.h |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | lcdlss.o |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | lcdlss.c |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | lcdlss.u |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | lcdlss.f |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | lcdlss.l |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | lcdlss.d |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | lcdlss.k |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | lcdlss.b |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 2, 3, 4, 5, 6, 7, 8, 9, 10 | lcdval2 35554 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | 11 | fveq2d 5798 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
13 | 1, 12 | syl5eq 2505 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 13 | eleq2d 2522 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 2, 5, 9 | dvhlmod 35074 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 8, 15 | lduallmod 33117 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | lcdlss.t |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
18 | 2, 5, 3, 6, 7, 8, 17, 10, 9 | lclkr 35497 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | eqid 2452 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
20 | eqid 2452 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
21 | 19, 17, 20 | lsslss 17160 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | 16, 18, 21 | syl2anc 661 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
23 | 14, 22 | bitrd 253 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | elin 3642 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
25 | selpw 3970 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
26 | 25 | anbi2i 694 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
27 | 24, 26 | bitr2i 250 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
28 | 23, 27 | syl6bb 261 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
29 | 28 | eqrdv 2449 |
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 1954 ax-ext 2431 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4573 ax-pr 4634 ax-un 6477 ax-cnex 9444 ax-resscn 9445 ax-1cn 9446 ax-icn 9447 ax-addcl 9448 ax-addrcl 9449 ax-mulcl 9450 ax-mulrcl 9451 ax-mulcom 9452 ax-addass 9453 ax-mulass 9454 ax-distr 9455 ax-i2m1 9456 ax-1ne0 9457 ax-1rid 9458 ax-rnegex 9459 ax-rrecex 9460 ax-cnre 9461 ax-pre-lttri 9462 ax-pre-lttrn 9463 ax-pre-ltadd 9464 ax-pre-mulgt0 9465 ax-riotaBAD 32923 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2265 df-mo 2266 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-ne 2647 df-nel 2648 df-ral 2801 df-rex 2802 df-reu 2803 df-rmo 2804 df-rab 2805 df-v 3074 df-sbc 3289 df-csb 3391 df-dif 3434 df-un 3436 df-in 3438 df-ss 3445 df-pss 3447 df-nul 3741 df-if 3895 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4195 df-int 4232 df-iun 4276 df-iin 4277 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4489 df-eprel 4735 df-id 4739 df-po 4744 df-so 4745 df-fr 4782 df-we 4784 df-ord 4825 df-on 4826 df-lim 4827 df-suc 4828 df-xp 4949 df-rel 4950 df-cnv 4951 df-co 4952 df-dm 4953 df-rn 4954 df-res 4955 df-ima 4956 df-iota 5484 df-fun 5523 df-fn 5524 df-f 5525 df-f1 5526 df-fo 5527 df-f1o 5528 df-fv 5529 df-riota 6156 df-ov 6198 df-oprab 6199 df-mpt2 6200 df-of 6425 df-om 6582 df-1st 6682 df-2nd 6683 df-tpos 6850 df-undef 6897 df-recs 6937 df-rdg 6971 df-1o 7025 df-oadd 7029 df-er 7206 df-map 7321 df-en 7416 df-dom 7417 df-sdom 7418 df-fin 7419 df-pnf 9526 df-mnf 9527 df-xr 9528 df-ltxr 9529 df-le 9530 df-sub 9703 df-neg 9704 df-nn 10429 df-2 10486 df-3 10487 df-4 10488 df-5 10489 df-6 10490 df-n0 10686 df-z 10753 df-uz 10968 df-fz 11550 df-struct 14289 df-ndx 14290 df-slot 14291 df-base 14292 df-sets 14293 df-ress 14294 df-plusg 14365 df-mulr 14366 df-sca 14368 df-vsca 14369 df-0g 14494 df-mre 14638 df-mrc 14639 df-acs 14641 df-poset 15230 df-plt 15242 df-lub 15258 df-glb 15259 df-join 15260 df-meet 15261 df-p0 15323 df-p1 15324 df-lat 15330 df-clat 15392 df-mnd 15529 df-submnd 15579 df-grp 15659 df-minusg 15660 df-sbg 15661 df-subg 15792 df-cntz 15949 df-oppg 15975 df-lsm 16251 df-cmn 16395 df-abl 16396 df-mgp 16709 df-ur 16721 df-rng 16765 df-oppr 16833 df-dvdsr 16851 df-unit 16852 df-invr 16882 df-dvr 16893 df-drng 16952 df-lmod 17068 df-lss 17132 df-lsp 17171 df-lvec 17302 df-lsatoms 32940 df-lshyp 32941 df-lcv 32983 df-lfl 33022 df-lkr 33050 df-ldual 33088 df-oposet 33140 df-ol 33142 df-oml 33143 df-covers 33230 df-ats 33231 df-atl 33262 df-cvlat 33286 df-hlat 33315 df-llines 33461 df-lplanes 33462 df-lvols 33463 df-lines 33464 df-psubsp 33466 df-pmap 33467 df-padd 33759 df-lhyp 33951 df-laut 33952 df-ldil 34067 df-ltrn 34068 df-trl 34122 df-tgrp 34706 df-tendo 34718 df-edring 34720 df-dveca 34966 df-disoa 34993 df-dvech 35043 df-dib 35103 df-dic 35137 df-dih 35193 df-doch 35312 df-djh 35359 df-lcdual 35551 |
This theorem is referenced by: lcdlss2N 35584 mapdrn2 35615 |
Copyright terms: Public domain | W3C validator |