Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > hdmapcl | Structured version Visualization version GIF version |
Description: Closure of map from vectors to functionals with closed kernels. (Contributed by NM, 15-May-2015.) |
Ref | Expression |
---|---|
hdmapcl.h | β’ π» = (LHypβπΎ) |
hdmapcl.u | β’ π = ((DVecHβπΎ)βπ) |
hdmapcl.v | β’ π = (Baseβπ) |
hdmapcl.c | β’ πΆ = ((LCDualβπΎ)βπ) |
hdmapcl.d | β’ π· = (BaseβπΆ) |
hdmapcl.s | β’ π = ((HDMapβπΎ)βπ) |
hdmapcl.k | β’ (π β (πΎ β HL β§ π β π»)) |
hdmapcl.t | β’ (π β π β π) |
Ref | Expression |
---|---|
hdmapcl | β’ (π β (πβπ) β π·) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hdmapcl.h | . . 3 β’ π» = (LHypβπΎ) | |
2 | eqid 2736 | . . 3 β’ β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© = β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© | |
3 | hdmapcl.u | . . 3 β’ π = ((DVecHβπΎ)βπ) | |
4 | hdmapcl.v | . . 3 β’ π = (Baseβπ) | |
5 | eqid 2736 | . . 3 β’ (LSpanβπ) = (LSpanβπ) | |
6 | hdmapcl.c | . . 3 β’ πΆ = ((LCDualβπΎ)βπ) | |
7 | hdmapcl.d | . . 3 β’ π· = (BaseβπΆ) | |
8 | eqid 2736 | . . 3 β’ ((HVMapβπΎ)βπ) = ((HVMapβπΎ)βπ) | |
9 | eqid 2736 | . . 3 β’ ((HDMap1βπΎ)βπ) = ((HDMap1βπΎ)βπ) | |
10 | hdmapcl.s | . . 3 β’ π = ((HDMapβπΎ)βπ) | |
11 | hdmapcl.k | . . 3 β’ (π β (πΎ β HL β§ π β π»)) | |
12 | hdmapcl.t | . . 3 β’ (π β π β π) | |
13 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 | hdmapval 39884 | . 2 β’ (π β (πβπ) = (β©β β π· βπ¦ β π (Β¬ π¦ β (((LSpanβπ)β{β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©}) βͺ ((LSpanβπ)β{π})) β β = (((HDMap1βπΎ)βπ)ββ¨π¦, (((HDMap1βπΎ)βπ)ββ¨β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©, (((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©), π¦β©), πβ©)))) |
14 | eqid 2736 | . . . 4 β’ (0gβπ) = (0gβπ) | |
15 | eqid 2736 | . . . 4 β’ (LSpanβπΆ) = (LSpanβπΆ) | |
16 | eqid 2736 | . . . 4 β’ ((mapdβπΎ)βπ) = ((mapdβπΎ)βπ) | |
17 | eqid 2736 | . . . . . 6 β’ (BaseβπΎ) = (BaseβπΎ) | |
18 | eqid 2736 | . . . . . 6 β’ ((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) | |
19 | 1, 17, 18, 3, 4, 14, 2, 11 | dvheveccl 39168 | . . . . 5 β’ (π β β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β© β (π β {(0gβπ)})) |
20 | 1, 3, 4, 14, 5, 6, 15, 16, 8, 11, 19 | mapdhvmap 39825 | . . . 4 β’ (π β (((mapdβπΎ)βπ)β((LSpanβπ)β{β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©})) = ((LSpanβπΆ)β{(((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©)})) |
21 | eqid 2736 | . . . . . 6 β’ (0gβπΆ) = (0gβπΆ) | |
22 | 1, 3, 4, 14, 6, 7, 21, 8, 11, 19 | hvmapcl2 39822 | . . . . 5 β’ (π β (((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©) β (π· β {(0gβπΆ)})) |
23 | 22 | eldifad 3904 | . . . 4 β’ (π β (((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©) β π·) |
24 | 1, 3, 4, 14, 5, 6, 7, 15, 16, 9, 11, 20, 19, 23, 12 | hdmap1eu 39880 | . . 3 β’ (π β β!β β π· βπ¦ β π (Β¬ π¦ β (((LSpanβπ)β{β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©}) βͺ ((LSpanβπ)β{π})) β β = (((HDMap1βπΎ)βπ)ββ¨π¦, (((HDMap1βπΎ)βπ)ββ¨β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©, (((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©), π¦β©), πβ©))) |
25 | riotacl 7282 | . . 3 β’ (β!β β π· βπ¦ β π (Β¬ π¦ β (((LSpanβπ)β{β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©}) βͺ ((LSpanβπ)β{π})) β β = (((HDMap1βπΎ)βπ)ββ¨π¦, (((HDMap1βπΎ)βπ)ββ¨β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©, (((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©), π¦β©), πβ©)) β (β©β β π· βπ¦ β π (Β¬ π¦ β (((LSpanβπ)β{β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©}) βͺ ((LSpanβπ)β{π})) β β = (((HDMap1βπΎ)βπ)ββ¨π¦, (((HDMap1βπΎ)βπ)ββ¨β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©, (((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©), π¦β©), πβ©))) β π·) | |
26 | 24, 25 | syl 17 | . 2 β’ (π β (β©β β π· βπ¦ β π (Β¬ π¦ β (((LSpanβπ)β{β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©}) βͺ ((LSpanβπ)β{π})) β β = (((HDMap1βπΎ)βπ)ββ¨π¦, (((HDMap1βπΎ)βπ)ββ¨β¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©, (((HVMapβπΎ)βπ)ββ¨( I βΎ (BaseβπΎ)), ( I βΎ ((LTrnβπΎ)βπ))β©), π¦β©), πβ©))) β π·) |
27 | 13, 26 | eqeltrd 2837 | 1 β’ (π β (πβπ) β π·) |
Colors of variables: wff setvar class |
Syntax hints: Β¬ wn 3 β wi 4 β§ wa 397 = wceq 1539 β wcel 2104 βwral 3062 β!wreu 3282 βͺ cun 3890 {csn 4565 β¨cop 4571 β¨cotp 4573 I cid 5499 βΎ cres 5602 βcfv 6458 β©crio 7263 Basecbs 16957 0gc0g 17195 LSpanclspn 20278 HLchlt 37406 LHypclh 38040 LTrncltrn 38157 DVecHcdvh 39134 LCDualclcd 39642 mapdcmpd 39680 HVMapchvm 39812 HDMap1chdma1 39847 HDMapchdma 39848 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-rep 5218 ax-sep 5232 ax-nul 5239 ax-pow 5297 ax-pr 5361 ax-un 7620 ax-cnex 10973 ax-resscn 10974 ax-1cn 10975 ax-icn 10976 ax-addcl 10977 ax-addrcl 10978 ax-mulcl 10979 ax-mulrcl 10980 ax-mulcom 10981 ax-addass 10982 ax-mulass 10983 ax-distr 10984 ax-i2m1 10985 ax-1ne0 10986 ax-1rid 10987 ax-rnegex 10988 ax-rrecex 10989 ax-cnre 10990 ax-pre-lttri 10991 ax-pre-lttrn 10992 ax-pre-ltadd 10993 ax-pre-mulgt0 10994 ax-riotaBAD 37009 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3285 df-reu 3286 df-rab 3287 df-v 3439 df-sbc 3722 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4566 df-pr 4568 df-tp 4570 df-op 4572 df-ot 4574 df-uni 4845 df-int 4887 df-iun 4933 df-iin 4934 df-br 5082 df-opab 5144 df-mpt 5165 df-tr 5199 df-id 5500 df-eprel 5506 df-po 5514 df-so 5515 df-fr 5555 df-we 5557 df-xp 5606 df-rel 5607 df-cnv 5608 df-co 5609 df-dm 5610 df-rn 5611 df-res 5612 df-ima 5613 df-pred 6217 df-ord 6284 df-on 6285 df-lim 6286 df-suc 6287 df-iota 6410 df-fun 6460 df-fn 6461 df-f 6462 df-f1 6463 df-fo 6464 df-f1o 6465 df-fv 6466 df-riota 7264 df-ov 7310 df-oprab 7311 df-mpo 7312 df-of 7565 df-om 7745 df-1st 7863 df-2nd 7864 df-tpos 8073 df-undef 8120 df-frecs 8128 df-wrecs 8159 df-recs 8233 df-rdg 8272 df-1o 8328 df-er 8529 df-map 8648 df-en 8765 df-dom 8766 df-sdom 8767 df-fin 8768 df-pnf 11057 df-mnf 11058 df-xr 11059 df-ltxr 11060 df-le 11061 df-sub 11253 df-neg 11254 df-nn 12020 df-2 12082 df-3 12083 df-4 12084 df-5 12085 df-6 12086 df-n0 12280 df-z 12366 df-uz 12629 df-fz 13286 df-struct 16893 df-sets 16910 df-slot 16928 df-ndx 16940 df-base 16958 df-ress 16987 df-plusg 17020 df-mulr 17021 df-sca 17023 df-vsca 17024 df-0g 17197 df-mre 17340 df-mrc 17341 df-acs 17343 df-proset 18058 df-poset 18076 df-plt 18093 df-lub 18109 df-glb 18110 df-join 18111 df-meet 18112 df-p0 18188 df-p1 18189 df-lat 18195 df-clat 18262 df-mgm 18371 df-sgrp 18420 df-mnd 18431 df-submnd 18476 df-grp 18625 df-minusg 18626 df-sbg 18627 df-subg 18797 df-cntz 18968 df-oppg 18995 df-lsm 19286 df-cmn 19433 df-abl 19434 df-mgp 19766 df-ur 19783 df-ring 19830 df-oppr 19907 df-dvdsr 19928 df-unit 19929 df-invr 19959 df-dvr 19970 df-drng 20038 df-lmod 20170 df-lss 20239 df-lsp 20279 df-lvec 20410 df-lsatoms 37032 df-lshyp 37033 df-lcv 37075 df-lfl 37114 df-lkr 37142 df-ldual 37180 df-oposet 37232 df-ol 37234 df-oml 37235 df-covers 37322 df-ats 37323 df-atl 37354 df-cvlat 37378 df-hlat 37407 df-llines 37554 df-lplanes 37555 df-lvols 37556 df-lines 37557 df-psubsp 37559 df-pmap 37560 df-padd 37852 df-lhyp 38044 df-laut 38045 df-ldil 38160 df-ltrn 38161 df-trl 38215 df-tgrp 38799 df-tendo 38811 df-edring 38813 df-dveca 39059 df-disoa 39085 df-dvech 39135 df-dib 39195 df-dic 39229 df-dih 39285 df-doch 39404 df-djh 39451 df-lcdual 39643 df-mapd 39681 df-hvmap 39813 df-hdmap1 39849 df-hdmap 39850 |
This theorem is referenced by: hdmapval2 39888 hdmap10lem 39895 hdmapeq0 39900 hdmapnzcl 39901 hdmapneg 39902 hdmapsub 39903 hdmap11 39904 hdmaprnlem3N 39906 hdmaprnlem3uN 39907 hdmaprnlem7N 39911 hdmaprnlem8N 39912 hdmaprnlem9N 39913 hdmaprnlem3eN 39914 hdmaprnN 39920 hdmap14lem2a 39923 hdmap14lem2N 39925 hdmap14lem3 39926 hdmap14lem4a 39927 hdmap14lem6 39929 hdmap14lem8 39931 hgmapval0 39948 hgmapval1 39949 hgmapadd 39950 hgmapmul 39951 hgmaprnlem1N 39952 hgmaprnlem2N 39953 hgmaprnlem4N 39955 hdmapipcl 39961 hdmapln1 39962 hdmaplna1 39963 hdmaplns1 39964 hdmaplnm1 39965 hdmaplna2 39966 hdmapglnm2 39967 hdmaplkr 39969 hdmapellkr 39970 hdmapip0 39971 hdmapinvlem1 39974 hdmapinvlem3 39976 |
Copyright terms: Public domain | W3C validator |