Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Norm Megill
Table of Contents - 20.25. Mathbox for Norm Megill
We are sad to report the passing of Metamath creator and long-time
contributor Norm Megill (1950 - 2021).
Norm of course was the author of the Metamath proof language, the
specification, all of the early tools (and some of the later ones),
and the foundational work in logic and set theory for set.mm.
His tools, now at https://github.com/metamath/metamath-exe , include
a proof verifier, a proof assistant, a proof minimizer, style
checking and reformatting, and tools for searching and displaying
proofs.
One of his key insights was that formal proofs can exist not only to
be verified by computers, but also to be read by humans. Both the
specification of the proof format (which stores full proofs, as
opposed to the proof templates used by most proof assistants) and
the generated web display of Metamath proofs, one of its distinctive
features, contribute to this double objective.
Metamath innovated both by using a very simple substitution rule (and
then using that to build more complicated notions like free and bound
variables) and also by taking the axiom schemas found in many theories
and taking them to the next level - by making all axioms, theorems and
proofs operate in terms of schemas.
Not content to create Metamath for his own amusement, he also published it
for the world and encouraged the development of a community of people who
contributed to it and created their own tools. He was an active participant
in the Metamath mailing list and other forums until days before his passing.
It is often our custom to supply a quote from someone memorialized
in a mathbox entry. And it is difficult to select a quote for someone
who has written so much about Metamath over the years. But here is one
quote from the Metamath web page which illustrates not just his clear
thinking about what Metamath can and cannot do but also his desire to
encourage students at all levels:
Q: Will Metamath help me learn abstract mathematics?
A: Yes, but probably not by itself. In order to follow a proof in an
advanced math textbook, you may need to know prerequisites that could take
years to learn. Some people find this frustrating. In contrast, Metamath
uses a single, simple substitution rule that allows you to follow any proof
mechanically. You can actually jump in anywhere and be convinced that
the symbol string you see in a proof step is a consequence of the symbol
strings in the earlier steps that it references, even if you don't
understand what the symbols mean. But this is quite different from
understanding the meaning of the math that results. Metamath alone
probably will not give you an intuitive feel for abstract math, in the
same way it can be hard to grasp a large computer program just by
reading its source code, even though you may understand each individual
instruction. However, the Bibliographic Cross-Reference lets you compare
informal proofs in math textbooks and see all the implicit missing
details "left to the reader."
Predicate calculus with equality: Older axiomatization (1 rule, 14 schemes)
Obsolete schemes ax-c4,c5,c7,c10,c11,c11n,c15,c9,c14,c16
ax-c5 ax-c4 ax-c7 ax-c10 ax-c11 ax-c11n ax-c15 ax-c9 ax-c14 ax-c16
Rederive new axioms ax-4, ax-10, ax-6, ax-12, ax-13 from old
axc5 ax4fromc4 ax10fromc7 ax6fromc10 hba1-o axc4i-o equid1 equcomi1 aecom-o aecoms-o hbae-o dral1-o ax12fromc15 ax13fromc9
Legacy theorems using obsolete axioms
ax5ALT sps-o hbequid nfequid-o axc5c7 axc5c7toc5 axc5c7toc7 axc711 nfa1-o axc711toc7 axc711to11 axc5c711 axc5c711toc5 axc5c711toc7 axc5c711to11 equidqe axc5sp1 equidq equid1ALT axc11nfromc11 naecoms-o hbnae-o dvelimf-o dral2-o aev-o ax5eq dveeq2-o axc16g-o dveeq1-o dveeq1-o16 ax5el axc11n-16 dveel2ALT ax12f ax12eq ax12el ax12indn ax12indi ax12indalem ax12inda2ALT ax12inda2 ax12inda ax12v2-o ax12a2-o axc11-o fsumshftd ax-riotaBAD riotaclbgBAD riotaclbBAD riotasvd riotasv2d riotasv2s riotasv riotasv3d
Experiments with weak deduction theorem
elimhyps dedths renegclALT elimhyps2 dedths2 nfcxfrdf nfded nfded2 nfunidALT2 nfunidALT nfopdALT
Miscellanea
cnaddcom toycom
Atoms, hyperplanes, and covering in a left vector space (or module)
clsa clsh df-lsatoms df-lshyp lshpset islshp islshpsm lshplss lshpne lshpnel lshpnelb lshpnel2N lshpne0 lshpdisj lshpcmp lshpinN lsatset islsat lsatlspsn2 lsatlspsn islsati lsateln0 lsatlss lsatlssel lsatssv lsatn0 lsatspn0 lsator0sp lsatssn0 lsatcmp lsatcmp2 lsatel lsatelbN lsat2el lsmsat lsatfixedN lsmsatcv lssatomic lssats lpssat lrelat lssatle lssat islshpat clcv df-lcv lcvfbr lcvbr lcvbr2 lcvbr3 lcvpss lcvnbtwn lcvntr lcvnbtwn2 lcvnbtwn3 lsmcv2 lcvat lsatcv0 lsatcveq0 lsat0cv lcvexchlem1 lcvexchlem2 lcvexchlem3 lcvexchlem4 lcvexchlem5 lcvexch lcvp lcv1 lcv2 lsatexch lsatnle lsatnem0 lsatexch1 lsatcv0eq lsatcv1 lsatcvatlem lsatcvat lsatcvat2 lsatcvat3 islshpcv l1cvpat l1cvat lshpat
Functionals and kernels of a left vector space (or module)
clfn df-lfl lflset islfl lfli islfld lflf lflcl lfl0 lfladd lflsub lflmul lfl0f lfl1 lfladdcl lfladdcom lfladdass lfladd0l lflnegcl lflnegl lflvscl lflvsdi1 lflvsdi2 lflvsdi2a lflvsass lfl0sc lflsc0N lfl1sc clk df-lkr lkrfval lkrval ellkr lkrval2 ellkr2 lkrcl lkrf0 lkr0f lkrlss lkrssv lkrsc lkrscss eqlkr eqlkr2 eqlkr3 lkrlsp lkrlsp2 lkrlsp3 lkrshp lkrshp3 lkrshpor lkrshp4 lshpsmreu lshpkrlem1 lshpkrlem2 lshpkrlem3 lshpkrlem4 lshpkrlem5 lshpkrlem6 lshpkrcl lshpkr lshpkrex lshpset2N islshpkrN lfl1dim lfl1dim2N
Opposite rings and dual vector spaces
cld df-ldual ldualset ldualvbase ldualelvbase ldualfvadd ldualvadd ldualvaddcl ldualvaddval ldualsca ldualsbase ldualsaddN ldualsmul ldualfvs ldualvs ldualvsval ldualvscl ldualvaddcom ldualvsass ldualvsass2 ldualvsdi1 ldualvsdi2 ldualgrplem ldualgrp ldual0 ldual1 ldualneg ldual0v ldual0vcl lduallmodlem lduallmod lduallvec ldualvsub ldualvsubcl ldualvsubval ldualssvscl ldualssvsubcl ldual0vs lkr0f2 lduallkr3 lkrpssN lkrin eqlkr4 ldual1dim ldualkrsc lkrss lkrss2N lkreqN lkrlspeqN
Ortholattices and orthomodular lattices
cops ccmtN col coml df-oposet df-cmtN df-ol df-oml isopos opposet oposlem op01dm op0cl op1cl op0le ople0 opnlen0 lub0N opltn0 ople1 op1le glb0N opoccl opococ opcon3b opcon2b opcon1b oplecon3 oplecon3b oplecon1b opoc1 opoc0 opltcon3b opltcon1b opltcon2b opexmid opnoncon riotaocN cmtfvalN cmtvalN isolat ollat olop olposN isolatiN oldmm1 oldmm2 oldmm3N oldmm4 oldmj1 oldmj2 oldmj3 oldmj4 olj01 olj02 olm11 olm12 latmassOLD latm12 latm32 latmrot latm4 latmmdiN latmmdir olm01 olm02 isoml isomliN omlol omlop omllat omllaw omllaw2N omllaw3 omllaw4 omllaw5N cmtcomlemN cmtcomN cmt2N cmt3N cmt4N cmtbr2N cmtbr3N cmtbr4N lecmtN cmtidN omlfh1N omlfh3N omlmod1i2N omlspjN
Atomic lattices with covering property
ccvr catm cal clc df-covers df-ats cvrfval cvrval cvrlt cvrnbtwn ncvr1 cvrletrN cvrval2 cvrnbtwn2 cvrnbtwn3 cvrcon3b cvrle cvrnbtwn4 cvrnle cvrne cvrnrefN cvrcmp cvrcmp2 pats isat isat2 atcvr0 atbase atssbase 0ltat leatb leat leat2 leat3 meetat meetat2 df-atl isatl atllat atlpos atl0dm atl0cl atl0le atlle0 atlltn0 isat3 atn0 atnle0 atlen0 atcmp atncmp atnlt atcvreq0 atncvrN atlex atnle atnem0 atlatmstc atlatle atlrelat1 df-cvlat iscvlat iscvlat2N cvlatl cvllat cvlposN cvlexch1 cvlexch2 cvlexchb1 cvlexchb2 cvlexch3 cvlexch4N cvlatexchb1 cvlatexchb2 cvlatexch1 cvlatexch2 cvlatexch3 cvlcvr1 cvlcvrp cvlatcvr1 cvlatcvr2 cvlsupr2 cvlsupr3 cvlsupr4 cvlsupr5 cvlsupr6 cvlsupr7 cvlsupr8
Hilbert lattices
chlt df-hlat ishlat1 ishlat2 ishlat3N ishlatiN hlomcmcv hloml hlclat hlcvl hlatl hlol hlop hllat hllatd hlomcmat hlpos hlatjcl hlatjcom hlatjidm hlatjass hlatj12 hlatj32 hlatjrot hlatj4 hlatlej1 hlatlej2 glbconN glbconxN atnlej1 atnlej2 hlsuprexch hlexch1 hlexch2 hlexchb1 hlexchb2 hlsupr hlsupr2 hlhgt4 hlhgt2 hl0lt1N hlexch3 hlexch4N hlatexchb1 hlatexchb2 hlatexch1 hlatexch2 hlatmstcOLDN hlatle hlateq hlrelat1 hlrelat5N hlrelat hlrelat2 exatleN hl2at atex intnatN 2llnne2N 2llnneN cvr1 cvr2N hlrelat3 cvrval3 cvrval4N cvrval5 cvrp atcvr1 atcvr2 cvrexchlem cvrexch cvratlem cvrat ltltncvr ltcvrntr cvrntr atcvr0eq lnnat atcvrj0 cvrat2 atcvrneN atcvrj1 atcvrj2b atcvrj2 atleneN atltcvr atle atlt atlelt 2atlt atexchcvrN atexchltN cvrat3 cvrat4 cvrat42 2atjm atbtwn atbtwnexOLDN atbtwnex 3noncolr2 3noncolr1N hlatcon3 hlatcon2 4noncolr3 4noncolr2 4noncolr1 athgt 3dim0 3dimlem1 3dimlem2 3dimlem3a 3dimlem3 3dimlem3OLDN 3dimlem4a 3dimlem4 3dimlem4OLDN 3dim1lem5 3dim1 3dim2 3dim3 2dim 1dimN 1cvrco 1cvratex 1cvratlt 1cvrjat 1cvrat ps-1 ps-2 2atjlej hlatexch3N hlatexch4 ps-2b 3atlem1 3atlem2 3atlem3 3atlem4 3atlem5 3atlem6 3atlem7 3at
Projective geometries based on Hilbert lattices
clln clpl clvol clines cpointsN cpsubsp cpmap df-llines df-lplanes df-lvols df-lines df-pointsN df-psubsp df-pmap llnset islln islln4 llni llnbase islln3 islln2 llni2 llnnleat llnneat 2atneat llnn0 islln2a llnle atcvrlln2 atcvrlln llnexatN llncmp llnnlt 2llnmat 2at0mat0 2atmat0 2atm ps-2c lplnset islpln islpln4 lplni islpln3 lplnbase islpln5 islpln2 lplni2 lvolex3N llnmlplnN lplnle lplnnle2at lplnnleat lplnnlelln 2atnelpln lplnneat lplnnelln lplnn0N islpln2a islpln2ah lplnriaN lplnribN lplnric lplnri1 lplnri2N lplnri3N lplnllnneN llncvrlpln2 llncvrlpln 2lplnmN 2llnmj 2atmat lplncmp lplnexatN lplnexllnN lplnnlt 2llnjaN 2llnjN 2llnm2N 2llnm3N 2llnm4 2llnmeqat lvolset islvol islvol4 lvoli islvol3 lvoli3 lvolbase islvol5 islvol2 lvoli2 lvolnle3at lvolnleat lvolnlelln lvolnlelpln 3atnelvolN 2atnelvolN lvolneatN lvolnelln lvolnelpln lvoln0N islvol2aN 4atlem0a 4atlem0ae 4atlem0be 4atlem3 4atlem3a 4atlem3b 4atlem4a 4atlem4b 4atlem4c 4atlem4d 4atlem9 4atlem10a 4atlem10b 4atlem10 4atlem11a 4atlem11b 4atlem11 4atlem12a 4atlem12b 4atlem12 4at 4at2 lplncvrlvol2 lplncvrlvol lvolcmp lvolnltN 2lplnja 2lplnj 2lplnm2N 2lplnmj dalemkehl dalemkelat dalemkeop dalempea dalemqea dalemrea dalemsea dalemtea dalemuea dalemyeo dalemzeo dalemclpjs dalemclqjt dalemclrju dalem-clpjq dalemceb dalempeb dalemqeb dalemreb dalemseb dalemteb dalemueb dalempjqeb dalemsjteb dalemtjueb dalemqrprot dalemyeb dalemcnes dalempnes dalemqnet dalempjsen dalemply dalemsly dalemswapyz dalemrot dalemrotyz dalem1 dalemcea dalem2 dalemdea dalemeea dalem3 dalem4 dalemdnee dalem5 dalem6 dalem7 dalem8 dalem-cly dalem9 dalem10 dalem11 dalem12 dalem13 dalem14 dalem15 dalem16 dalem17 dalem18 dalem19 dalemccea dalemddea dalem-ccly dalem-ddly dalemccnedd dalemclccjdd dalemcceb dalemswapyzps dalemrotps dalemcjden dalem20 dalem21 dalem22 dalem23 dalem24 dalem25 dalem27 dalem28 dalem29 dalem30 dalem31N dalem32 dalem33 dalem34 dalem35 dalem36 dalem37 dalem38 dalem39 dalem40 dalem41 dalem42 dalem43 dalem44 dalem45 dalem46 dalem47 dalem48 dalem49 dalem50 dalem51 dalem52 dalem53 dalem54 dalem55 dalem56 dalem57 dalem58 dalem59 dalem60 dalem61 dalem62 dalem63 dath dath2 lineset isline islinei pointsetN ispointN atpointN psubspset ispsubsp ispsubsp2 psubspi psubspi2N 0psubN snatpsubN pointpsubN linepsubN atpsubN psubssat psubatN pmapfval pmapval elpmap pmapssat pmapssbaN pmaple pmap11 pmapat elpmapat pmap0 pmapeq0 pmap1N pmapsub pmapglbx pmapglb pmapglb2N pmapglb2xN pmapmeet isline2 linepmap isline3 isline4N lneq2at lnatexN lnjatN lncvrelatN lncvrat lncmp 2lnat 2atm2atN 2llnma1b 2llnma1 2llnma3r 2llnma2 2llnma2rN
Construction of a vector space from a Hilbert lattice
cdlema1N cdlema2N cdlemblem cdlemb cpadd df-padd paddfval paddval elpadd elpaddn0 paddvaln0N elpaddri elpaddatriN elpaddat elpaddatiN elpadd2at elpadd2at2 paddunssN elpadd0 paddval0 padd01 padd02 paddcom paddssat sspadd1 sspadd2 paddss1 paddss2 paddss12 paddasslem1 paddasslem2 paddasslem3 paddasslem4 paddasslem5 paddasslem6 paddasslem7 paddasslem8 paddasslem9 paddasslem10 paddasslem11 paddasslem12 paddasslem13 paddasslem14 paddasslem15 paddasslem16 paddasslem17 paddasslem18 paddass padd12N padd4N paddidm paddclN paddssw1 paddssw2 paddss pmodlem1 pmodlem2 pmod1i pmod2iN pmodN pmodl42N pmapjoin pmapjat1 pmapjat2 pmapjlln1 hlmod1i atmod1i1 atmod1i1m atmod1i2 llnmod1i2 atmod2i1 atmod2i2 llnmod2i2 atmod3i1 atmod3i2 atmod4i1 atmod4i2 llnexchb2lem llnexchb2 llnexch2N dalawlem1 dalawlem2 dalawlem3 dalawlem4 dalawlem5 dalawlem6 dalawlem7 dalawlem8 dalawlem9 dalawlem10 dalawlem11 dalawlem12 dalawlem13 dalawlem14 dalawlem15 dalaw cpclN df-pclN pclfvalN pclvalN pclclN elpclN elpcliN pclssN pclssidN pclidN pclbtwnN pclunN pclun2N pclfinN pclcmpatN cpolN df-polarityN polfvalN polvalN polval2N polsubN polssatN pol0N pol1N 2pol0N polpmapN 2polpmapN 2polvalN 2polssN 3polN polcon3N 2polcon4bN polcon2N polcon2bN pclss2polN pcl0N pcl0bN pmaplubN sspmaplubN 2pmaplubN paddunN poldmj1N pmapj2N pmapocjN polatN 2polatN pnonsingN cpscN df-psubclN psubclsetN ispsubclN psubcliN psubcli2N psubclsubN psubclssatN pmapidclN 0psubclN 1psubclN atpsubclN pmapsubclN ispsubcl2N psubclinN paddatclN pclfinclN linepsubclN polsubclN poml4N poml5N poml6N osumcllem1N osumcllem2N osumcllem3N osumcllem4N osumcllem5N osumcllem6N osumcllem7N osumcllem8N osumcllem9N osumcllem10N osumcllem11N osumclN pmapojoinN pexmidN pexmidlem1N pexmidlem2N pexmidlem3N pexmidlem4N pexmidlem5N pexmidlem6N pexmidlem7N pexmidlem8N pexmidALTN pl42lem1N pl42lem2N pl42lem3N pl42lem4N pl42N clh claut cwpointsN cpautN df-lhyp df-laut df-watsN df-pautN watfvalN watvalN iswatN lhpset islhp islhp2 lhpbase lhp1cvr lhplt lhp2lt lhpexlt lhp0lt lhpn0 lhpexle lhpexnle lhpexle1lem lhpexle1 lhpexle2lem lhpexle2 lhpexle3lem lhpexle3 lhpex2leN lhpoc lhpoc2N lhpocnle lhpocat lhpocnel lhpocnel2 lhpjat1 lhpjat2 lhpj1 lhpmcvr lhpmcvr2 lhpmcvr3 lhpmcvr4N lhpmcvr5N lhpmcvr6N lhpm0atN lhpmat lhpmatb lhp2at0 lhp2atnle lhp2atne lhp2at0nle lhp2at0ne lhpelim lhpmod2i2 lhpmod6i1 lhprelat3N cdlemb2 lhple lhpat lhpat4N lhpat2 lhpat3 4atexlemk 4atexlemw 4atexlempw 4atexlemp 4atexlemq 4atexlems 4atexlemt 4atexlemutvt 4atexlempnq 4atexlemnslpq 4atexlemkl 4atexlemkc 4atexlemwb 4atexlempsb 4atexlemqtb 4atexlempns 4atexlemswapqr 4atexlemu 4atexlemv 4atexlemunv 4atexlemtlw 4atexlemntlpq 4atexlemc 4atexlemnclw 4atexlemex2 4atexlemcnd 4atexlemex4 4atexlemex6 4atexlem7 4atex 4atex2 4atex2-0aOLDN 4atex2-0bOLDN 4atex2-0cOLDN 4atex3 lautset islaut lautle laut1o laut11 lautcl lautcnvclN lautcnvle lautcnv lautlt lautcvr lautj lautm lauteq idlaut lautco pautsetN ispautN cldil cltrn cdilN ctrnN df-ldil df-ltrn df-dilN df-trnN ldilfset ldilset isldil ldillaut ldil1o ldilval idldil ldilcnv ldilco ltrnfset ltrnset isltrn isltrn2N ltrnu ltrnldil ltrnlaut ltrn1o ltrncl ltrn11 ltrncnvnid ltrncoidN ltrnle ltrncnvleN ltrnm ltrnj ltrncvr ltrnval1 ltrnid ltrnnid ltrnatb ltrncnvatb ltrnel ltrnat ltrncnvat ltrncnvel ltrncoelN ltrncoat ltrncoval ltrncnv ltrn11at ltrneq2 ltrneq idltrn ltrnmw dilfsetN dilsetN isdilN trnfsetN trnsetN istrnN ctrl df-trl trlfset trlset trlval trlval2 trlcl trlcnv trljat1 trljat2 trljat3 trlat trl0 trlator0 trlatn0 trlnidat ltrnnidn ltrnideq trlid0 trlnidatb trlid0b trlnid ltrn2ateq ltrnateq ltrnatneq ltrnatlw trlle trlne trlnle trlval3 trlval4 trlval5 arglem1N cdlemc1 cdlemc2 cdlemc3 cdlemc4 cdlemc5 cdlemc6 cdlemc cdlemd1 cdlemd2 cdlemd3 cdlemd4 cdlemd5 cdlemd6 cdlemd7 cdlemd8 cdlemd9 cdlemd ltrneq3 cdleme00a cdleme0aa cdleme0a cdleme0b cdleme0c cdleme0cp cdleme0cq cdleme0dN cdleme0e cdleme0fN cdleme0gN cdlemeulpq cdleme01N cdleme02N cdleme0ex1N cdleme0ex2N cdleme0moN cdleme1b cdleme1 cdleme2 cdleme3b cdleme3c cdleme3d cdleme3e cdleme3fN cdleme3g cdleme3h cdleme3fa cdleme3 cdleme4 cdleme4a cdleme5 cdleme6 cdleme7aa cdleme7a cdleme7b cdleme7c cdleme7d cdleme7e cdleme7ga cdleme7 cdleme8 cdleme9a cdleme9b cdleme9 cdleme10 cdleme8tN cdleme9taN cdleme9tN cdleme10tN cdleme16aN cdleme11a cdleme11c cdleme11dN cdleme11e cdleme11fN cdleme11g cdleme11h cdleme11j cdleme11k cdleme11l cdleme11 cdleme12 cdleme13 cdleme14 cdleme15a cdleme15b cdleme15c cdleme15d cdleme15 cdleme16b cdleme16c cdleme16d cdleme16e cdleme16f cdleme16g cdleme16 cdleme17a cdleme17b cdleme17c cdleme17d1 cdleme0nex cdleme18a cdleme18b cdleme18c cdleme22gb cdleme18d cdlemesner cdlemedb cdlemeda cdlemednpq cdlemednuN cdleme20zN cdleme20y cdleme19a cdleme19b cdleme19c cdleme19d cdleme19e cdleme19f cdleme20aN cdleme20bN cdleme20c cdleme20d cdleme20e cdleme20f cdleme20g cdleme20h cdleme20i cdleme20j cdleme20k cdleme20l1 cdleme20l2 cdleme20l cdleme20m cdleme20 cdleme21a cdleme21b cdleme21c cdleme21at cdleme21ct cdleme21d cdleme21e cdleme21f cdleme21g cdleme21h cdleme21i cdleme21j cdleme21 cdleme21k cdleme22aa cdleme22a cdleme22b cdleme22cN cdleme22d cdleme22e cdleme22eALTN cdleme22f cdleme22f2 cdleme22g cdleme23a cdleme23b cdleme23c cdleme24 cdleme25a cdleme25b cdleme25c cdleme25dN cdleme25cl cdleme25cv cdleme26e cdleme26ee cdleme26eALTN cdleme26fALTN cdleme26f cdleme26f2ALTN cdleme26f2 cdleme27cl cdleme27a cdleme27b cdleme27N cdleme28a cdleme28b cdleme28c cdleme28 cdleme29ex cdleme29b cdleme29c cdleme29cl cdleme30a cdleme31so cdleme31sn cdleme31sn1 cdleme31se cdleme31se2 cdleme31sc cdleme31sde cdleme31snd cdleme31sdnN cdleme31sn1c cdleme31sn2 cdleme31fv cdleme31fv1 cdleme31fv1s cdleme31fv2 cdleme31id cdlemefrs29pre00 cdlemefrs29bpre0 cdlemefrs29bpre1 cdlemefrs29cpre1 cdlemefrs29clN cdlemefrs32fva cdlemefrs32fva1 cdlemefr29exN cdlemefr27cl cdlemefr32sn2aw cdlemefr32snb cdlemefr29bpre0N cdlemefr29clN cdleme43frv1snN cdlemefr32fvaN cdlemefr32fva1 cdlemefr31fv1 cdlemefs29pre00N cdlemefs27cl cdlemefs32sn1aw cdlemefs32snb cdlemefs29bpre0N cdlemefs29bpre1N cdlemefs29cpre1N cdlemefs29clN cdleme43fsv1snlem cdleme43fsv1sn cdlemefs32fvaN cdlemefs32fva1 cdlemefs31fv1 cdlemefr44 cdlemefs44 cdlemefr45 cdlemefr45e cdlemefs45 cdlemefs45ee cdlemefs45eN cdleme32sn1awN cdleme41sn3a cdleme32sn2awN cdleme32snaw cdleme32snb cdleme32fva cdleme32fva1 cdleme32fvaw cdleme32fvcl cdleme32a cdleme32b cdleme32c cdleme32d cdleme32e cdleme32f cdleme32le cdleme35a cdleme35fnpq cdleme35b cdleme35c cdleme35d cdleme35e cdleme35f cdleme35g cdleme35h cdleme35h2 cdleme35sn2aw cdleme35sn3a cdleme36a cdleme36m cdleme37m cdleme38m cdleme38n cdleme39a cdleme39n cdleme40m cdleme40n cdleme40v cdleme40w cdleme42a cdleme42c cdleme42d cdleme41sn3aw cdleme41sn4aw cdleme41snaw cdleme41fva11 cdleme42b cdleme42e cdleme42f cdleme42g cdleme42h cdleme42i cdleme42k cdleme42ke cdleme42keg cdleme42mN cdleme42mgN cdleme43aN cdleme43bN cdleme43cN cdleme43dN cdleme46f2g2 cdleme46f2g1 cdleme17d2 cdleme17d3 cdleme17d4 cdleme17d cdleme48fv cdleme48fvg cdleme46fvaw cdleme48bw cdleme48b cdleme46frvlpq cdleme46fsvlpq cdlemeg46fvcl cdleme4gfv cdlemeg47b cdlemeg47rv cdlemeg47rv2 cdlemeg49le cdlemeg46bOLDN cdlemeg46c cdlemeg46rvOLDN cdlemeg46rv2OLDN cdlemeg46fvaw cdlemeg46nlpq cdlemeg46ngfr cdlemeg46nfgr cdlemeg46sfg cdlemeg46fjgN cdlemeg46rjgN cdlemeg46fjv cdlemeg46fsfv cdlemeg46frv cdlemeg46v1v2 cdlemeg46vrg cdlemeg46rgv cdlemeg46req cdlemeg46gfv cdlemeg46gfr cdlemeg46gfre cdlemeg46gf cdlemeg46fgN cdleme48d cdleme48gfv1 cdleme48gfv cdleme48fgv cdlemeg49lebilem cdleme50lebi cdleme50eq cdleme50f cdleme50f1 cdleme50rnlem cdleme50rn cdleme50f1o cdleme50laut cdleme50ldil cdleme50trn1 cdleme50trn2a cdleme50trn2 cdleme50trn12 cdleme50trn3 cdleme50trn123 cdleme51finvfvN cdleme51finvN cdleme50ltrn cdleme51finvtrN cdleme50ex cdleme cdlemf1 cdlemf2 cdlemf cdlemfnid cdlemftr3 cdlemftr2 cdlemftr1 cdlemftr0 trlord cdlemg1a cdlemg1b2 cdlemg1idlemN cdlemg1fvawlemN cdlemg1ltrnlem cdlemg1finvtrlemN cdlemg1bOLDN cdlemg1idN ltrniotafvawN ltrniotacl ltrniotacnvN ltrniotaval ltrniotacnvval ltrniotaidvalN ltrniotavalbN cdlemeiota cdlemg1ci2 cdlemg1cN cdlemg1cex cdlemg2cN cdlemg2dN cdlemg2cex cdlemg2ce cdlemg2jlemOLDN cdlemg2fvlem cdlemg2klem cdlemg2idN cdlemg3a cdlemg2jOLDN cdlemg2fv cdlemg2fv2 cdlemg2k cdlemg2kq cdlemg2l cdlemg2m cdlemg5 cdlemb3 cdlemg7fvbwN cdlemg4a cdlemg4b1 cdlemg4b2 cdlemg4b12 cdlemg4c cdlemg4d cdlemg4e cdlemg4f cdlemg4g cdlemg4 cdlemg6a cdlemg6b cdlemg6c cdlemg6d cdlemg6e cdlemg6 cdlemg7fvN cdlemg7aN cdlemg7N cdlemg8a cdlemg8b cdlemg8c cdlemg8d cdlemg8 cdlemg9a cdlemg9b cdlemg9 cdlemg10b cdlemg10bALTN cdlemg11a cdlemg11aq cdlemg10c cdlemg10a cdlemg10 cdlemg11b cdlemg12a cdlemg12b cdlemg12c cdlemg12d cdlemg12e cdlemg12f cdlemg12g cdlemg12 cdlemg13a cdlemg13 cdlemg14f cdlemg14g cdlemg15a cdlemg15 cdlemg16 cdlemg16ALTN cdlemg16z cdlemg16zz cdlemg17a cdlemg17b cdlemg17dN cdlemg17dALTN cdlemg17e cdlemg17f cdlemg17g cdlemg17h cdlemg17i cdlemg17ir cdlemg17j cdlemg17pq cdlemg17bq cdlemg17iqN cdlemg17irq cdlemg17jq cdlemg17 cdlemg18a cdlemg18b cdlemg18c cdlemg18d cdlemg18 cdlemg19a cdlemg19 cdlemg20 cdlemg21 cdlemg22 cdlemg24 cdlemg37 cdlemg25zz cdlemg26zz cdlemg27a cdlemg28a cdlemg31b0N cdlemg31b0a cdlemg27b cdlemg31a cdlemg31b cdlemg31c cdlemg31d cdlemg33b0 cdlemg33c0 cdlemg28b cdlemg28 cdlemg29 cdlemg33a cdlemg33b cdlemg33c cdlemg33d cdlemg33e cdlemg33 cdlemg34 cdlemg35 cdlemg36 cdlemg38 cdlemg39 cdlemg40 cdlemg41 ltrnco trlcocnv trlcoabs trlcoabs2N trlcoat trlcocnvat trlconid trlcolem trlco trlcone cdlemg42 cdlemg43 cdlemg44a cdlemg44b cdlemg44 cdlemg47a cdlemg46 cdlemg47 cdlemg48 ltrncom ltrnco4 trljco trljco2 ctgrp df-tgrp tgrpfset tgrpset tgrpbase tgrpopr tgrpov tgrpgrplem tgrpgrp tgrpabl ctendo cedring cedring-rN df-tendo df-edring-rN df-edring tendofset tendoset istendo tendotp istendod tendof tendoeq1 tendovalco tendocoval tendocl tendoco2 tendoidcl tendo1mul tendo1mulr tendococl tendoid tendoeq2 tendoplcbv tendopl tendopl2 tendoplcl2 tendoplco2 tendopltp tendoplcl tendoplcom tendoplass tendodi1 tendodi2 tendo0cbv tendo02 tendo0co2 tendo0tp tendo0cl tendo0pl tendo0plr tendoicbv tendoi tendoi2 tendoicl tendoipl tendoipl2 erngfset erngset erngbase erngfplus erngplus erngplus2 erngfmul erngmul erngfset-rN erngset-rN erngbase-rN erngfplus-rN erngplus-rN erngplus2-rN erngfmul-rN erngmul-rN cdlemh1 cdlemh2 cdlemh cdlemi1 cdlemi2 cdlemi cdlemj1 cdlemj2 cdlemj3 tendocan tendoid0 tendo0mul tendo0mulr tendo1ne0 tendoconid tendotr cdlemk1 cdlemk2 cdlemk3 cdlemk4 cdlemk5a cdlemk5 cdlemk6 cdlemk8 cdlemk9 cdlemk9bN cdlemki cdlemkvcl cdlemk10 cdlemksv cdlemksel cdlemksat cdlemksv2 cdlemk7 cdlemk11 cdlemk12 cdlemkoatnle cdlemk13 cdlemkole cdlemk14 cdlemk15 cdlemk16a cdlemk16 cdlemk17 cdlemk1u cdlemk5auN cdlemk5u cdlemk6u cdlemkj cdlemkuvN cdlemkuel cdlemkuat cdlemkuv2 cdlemk18 cdlemk19 cdlemk7u cdlemk11u cdlemk12u cdlemk21N cdlemk20 cdlemkoatnle-2N cdlemk13-2N cdlemkole-2N cdlemk14-2N cdlemk15-2N cdlemk16-2N cdlemk17-2N cdlemkj-2N cdlemkuv-2N cdlemkuel-2N cdlemkuv2-2 cdlemk18-2N cdlemk19-2N cdlemk7u-2N cdlemk11u-2N cdlemk12u-2N cdlemk21-2N cdlemk20-2N cdlemk22 cdlemk30 cdlemkuu cdlemk31 cdlemk32 cdlemkuel-3 cdlemkuv2-3N cdlemk18-3N cdlemk22-3 cdlemk23-3 cdlemk24-3 cdlemk25-3 cdlemk26b-3 cdlemk26-3 cdlemk27-3 cdlemk28-3 cdlemk33N cdlemk34 cdlemk29-3 cdlemk35 cdlemk36 cdlemk37 cdlemk38 cdlemk39 cdlemk40 cdlemk40t cdlemk40f cdlemk41 cdlemkfid1N cdlemkid1 cdlemkfid2N cdlemkid2 cdlemkfid3N cdlemky cdlemkyu cdlemkyuu cdlemk11ta cdlemk19ylem cdlemk11tb cdlemk19y cdlemkid3N cdlemkid4 cdlemkid5 cdlemkid cdlemk35s cdlemk35s-id cdlemk39s cdlemk39s-id cdlemk42 cdlemk19xlem cdlemk19x cdlemk42yN cdlemk11tc cdlemk11t cdlemk45 cdlemk46 cdlemk47 cdlemk48 cdlemk49 cdlemk50 cdlemk51 cdlemk52 cdlemk53a cdlemk53b cdlemk53 cdlemk54 cdlemk55a cdlemk55b cdlemk55 cdlemkyyN cdlemk43N cdlemk35u cdlemk55u1 cdlemk55u cdlemk39u1 cdlemk39u cdlemk19u1 cdlemk19u cdlemk56 cdlemk19w cdlemk56w cdlemk tendoex cdleml1N cdleml2N cdleml3N cdleml4N cdleml5N cdleml6 cdleml7 cdleml8 cdleml9 dva1dim dvhb1dimN erng1lem erngdvlem1 erngdvlem2N erngdvlem3 erngdvlem4 eringring erngdv erng0g erng1r erngdvlem1-rN erngdvlem2-rN erngdvlem3-rN erngdvlem4-rN erngring-rN erngdv-rN cdveca df-dveca dvafset dvaset dvasca dvabase dvafplusg dvaplusg dvaplusgv dvafmulr dvamulr dvavbase dvafvadd dvavadd dvafvsca dvavsca tendospcl tendospass tendospdi1 tendocnv tendospdi2 tendospcanN dvaabl dvalveclem dvalvec dva0g cdia df-disoa diaffval diafval diaval diaelval diafn diadm diaeldm diadmclN diadmleN dian0 dia0eldmN dia1eldmN diass diael diatrl diaelrnN dialss diaord dia11N diaf11N diaclN diacnvclN dia0 dia1N dia1elN diaglbN diameetN diainN diaintclN diasslssN diassdvaN dia1dim dia1dim2 dia1dimid dia2dimlem1 dia2dimlem2 dia2dimlem3 dia2dimlem4 dia2dimlem5 dia2dimlem6 dia2dimlem7 dia2dimlem8 dia2dimlem9 dia2dimlem10 dia2dimlem11 dia2dimlem12 dia2dimlem13 dia2dim cdvh df-dvech dvhfset dvhset dvhsca dvhbase dvhfplusr dvhfmulr dvhmulr dvhvbase dvhelvbasei dvhvaddcbv dvhvaddval dvhfvadd dvhvadd dvhopvadd dvhopvadd2 dvhvaddcl dvhvaddcomN dvhvaddass dvhvscacbv dvhvscaval dvhfvsca dvhvsca dvhopvsca dvhvscacl tendoinvcl tendolinv tendorinv dvhgrp dvhlveclem dvhlvec dvhlmod dvh0g dvheveccl dvhopclN dvhopaddN dvhopspN dvhopN dvhopellsm cdlemm10N cocaN df-docaN docaffvalN docafvalN docavalN docaclN diaocN doca2N doca3N dvadiaN diarnN diaf1oN cdjaN df-djaN djaffvalN djafvalN djavalN djaclN djajN cdib df-dib dibffval dibfval dibval dibopelvalN dibval2 dibopelval2 dibval3N dibelval3 dibopelval3 dibelval1st dibelval1st1 dibelval1st2N dibelval2nd dibn0 dibfna dibdiadm dibfnN dibdmN dibeldmN dibord dib11N dibf11N dibclN dibvalrel dib0 dib1dim dibglbN dibintclN dib1dim2 dibss diblss diblsmopel cdic df-dic dicffval dicfval dicval dicopelval dicelvalN dicval2 dicelval3 dicopelval2 dicelval2N dicfnN dicdmN dicvalrelN dicssdvh dicelval1sta dicelval1stN dicelval2nd dicvaddcl dicvscacl dicn0 diclss diclspsn cdlemn2 cdlemn2a cdlemn3 cdlemn4 cdlemn4a cdlemn5pre cdlemn5 cdlemn6 cdlemn7 cdlemn8 cdlemn9 cdlemn10 cdlemn11a cdlemn11b cdlemn11c cdlemn11pre cdlemn11 cdlemn dihordlem6 dihordlem7 dihordlem7b dihjustlem dihjust dihord1 dihord2a dihord2b dihord2cN dihord11b dihord10 dihord11c dihord2pre dihord2pre2 dihord2 cdih df-dih dihffval dihfval dihval dihvalc dihlsscpre dihvalcqpre dihvalcq dihvalb dihopelvalbN dihvalcqat dih1dimb dih1dimb2 dih1dimc dib2dim dih2dimb dih2dimbALTN dihopelvalcqat dihvalcq2 dihopelvalcpre dihopelvalc dihlss dihss dihssxp dihopcl xihopellsmN dihopellsm dihord6apre dihord3 dihord4 dihord5b dihord6b dihord6a dihord5apre dihord5a dihord dih11 dihf11lem dihf11 dihfn dihdm dihcl dihcnvcl dihcnvid1 dihcnvid2 dihcnvord dihcnv11 dihsslss dihrnlss dihrnss dihvalrel dih0 dih0bN dih0vbN dih0cnv dih0rn dih0sb dih1 dih1rn dih1cnv dihwN dihmeetlem1N dihglblem5apreN dihglblem5aN dihglblem2aN dihglblem2N dihglblem3N dihglblem3aN dihglblem4 dihglblem5 dihmeetlem2N dihglbcpreN dihglbcN dihmeetcN dihmeetbN dihmeetbclemN dihmeetlem3N dihmeetlem4preN dihmeetlem4N dihmeetlem5 dihmeetlem6 dihmeetlem7N dihjatc1 dihjatc2N dihjatc3 dihmeetlem8N dihmeetlem9N dihmeetlem10N dihmeetlem11N dihmeetlem12N dihmeetlem13N dihmeetlem14N dihmeetlem15N dihmeetlem16N dihmeetlem17N dihmeetlem18N dihmeetlem19N dihmeetlem20N dihmeetALTN dih1dimatlem0 dih1dimatlem dih1dimat dihlsprn dihlspsnssN dihlspsnat dihatlat dihat dihpN dihlatat dihatexv dihatexv2 dihglblem6 dihglb dihglb2 dihmeet dihintcl dihmeetcl dihmeet2 coch df-doch dochffval dochfval dochval dochval2 dochcl dochlss dochssv dochfN dochvalr doch0 doch1 dochoc0 dochoc1 dochvalr2 dochvalr3 doch2val2 dochss dochocss dochoc dochsscl dochoccl dochord dochord2N dochord3 doch11 dochsordN dochn0nv dihoml4c dihoml4 dochspss dochocsp dochspocN dochocsn dochsncom dochsat dochshpncl dochlkr dochkrshp dochkrshp2 dochkrshp3 dochkrshp4 dochdmj1 dochnoncon dochnel2 dochnel cdjh df-djh djhffval djhfval djhval djhval2 djhcl djhlj djhljjN djhjlj djhj djhcom djhspss djhsumss dihsumssj djhunssN dochdmm1 djhexmid djh01 djh02 djhlsmcl djhcvat42 dihjatb dihjatc dihjatcclem1 dihjatcclem2 dihjatcclem3 dihjatcclem4 dihjatcc dihjat dihprrnlem1N dihprrnlem2 dihprrn djhlsmat dihjat1lem dihjat1 dihsmsprn dihjat2 dihjat3 dihjat4 dihjat6 dihsmsnrn dihsmatrn dihjat5N dvh4dimat dvh3dimatN dvh2dimatN dvh1dimat dvh1dim dvh4dimlem dvhdimlem dvh2dim dvh3dim dvh4dimN dvh3dim2 dvh3dim3N dochsnnz dochsatshp dochsatshpb dochsnshp dochshpsat dochkrsat dochkrsat2 dochsat0 dochkrsm dochexmidat dochexmidlem1 dochexmidlem2 dochexmidlem3 dochexmidlem4 dochexmidlem5 dochexmidlem6 dochexmidlem7 dochexmidlem8 dochexmid dochsnkrlem1 dochsnkrlem2 dochsnkrlem3 dochsnkr dochsnkr2 dochsnkr2cl dochflcl dochfl1 dochfln0 dochkr1 dochkr1OLDN
Construction of involution and inner product from a Hilbert lattice
clpoN df-lpolN lpolsetN islpolN islpoldN lpolfN lpolvN lpolconN lpolsatN lpolpolsatN dochpolN lcfl1lem lcfl1 lcfl2 lcfl3 lcfl4N lcfl5 lcfl5a lcfl6lem lcfl7lem lcfl6 lcfl7N lcfl8 lcfl8a lcfl8b lcfl9a lclkrlem1 lclkrlem2a lclkrlem2b lclkrlem2c lclkrlem2d lclkrlem2e lclkrlem2f lclkrlem2g lclkrlem2h lclkrlem2i lclkrlem2j lclkrlem2k lclkrlem2l lclkrlem2m lclkrlem2n lclkrlem2o lclkrlem2p lclkrlem2q lclkrlem2r lclkrlem2s lclkrlem2t lclkrlem2u lclkrlem2v lclkrlem2w lclkrlem2x lclkrlem2y lclkrlem2 lclkr lcfls1lem lcfls1N lcfls1c lclkrslem1 lclkrslem2 lclkrs lclkrs2 lcfrvalsnN lcfrlem1 lcfrlem2 lcfrlem3 lcfrlem4 lcfrlem5 lcfrlem6 lcfrlem7 lcfrlem8 lcfrlem9 lcf1o lcfrlem10 lcfrlem11 lcfrlem12N lcfrlem13 lcfrlem14 lcfrlem15 lcfrlem16 lcfrlem17 lcfrlem18 lcfrlem19 lcfrlem20 lcfrlem21 lcfrlem22 lcfrlem23 lcfrlem24 lcfrlem25 lcfrlem26 lcfrlem27 lcfrlem28 lcfrlem29 lcfrlem30 lcfrlem31 lcfrlem32 lcfrlem33 lcfrlem34 lcfrlem35 lcfrlem36 lcfrlem37 lcfrlem38 lcfrlem39 lcfrlem40 lcfrlem41 lcfrlem42 lcfr clcd df-lcdual lcdfval lcdval lcdval2 lcdlvec lcdlmod lcdvbase lcdvbasess lcdvbaselfl lcdvbasecl lcdvadd lcdvaddval lcdsca lcdsbase lcdsadd lcdsmul lcdvs lcdvsval lcdvscl lcdlssvscl lcdvsass lcd0 lcd1 lcdneg lcd0v lcd0v2 lcd0vvalN lcd0vcl lcd0vs lcdvs0N lcdvsub lcdvsubval lcdlss lcdlss2N lcdlsp lcdlkreqN lcdlkreq2N cmpd df-mapd mapdffval mapdfval mapdval mapdvalc mapdval2N mapdval3N mapdval4N mapdval5N mapdordlem1a mapdordlem1bN mapdordlem1 mapdordlem2 mapdord mapd11 mapddlssN mapdsn mapdsn2 mapdsn3 mapd1dim2lem1N mapdrvallem2 mapdrvallem3 mapdrval mapd1o mapdrn mapdunirnN mapdrn2 mapdcnvcl mapdcl mapdcnvid1N mapdsord mapdcl2 mapdcnvid2 mapdcnvordN mapdcnv11N mapdcv mapdincl mapdin mapdlsmcl mapdlsm mapd0 mapdcnvatN mapdat mapdspex mapdn0 mapdncol mapdindp mapdpglem1 mapdpglem2 mapdpglem2a mapdpglem3 mapdpglem4N mapdpglem5N mapdpglem6 mapdpglem8 mapdpglem9 mapdpglem10 mapdpglem11 mapdpglem12 mapdpglem13 mapdpglem14 mapdpglem15 mapdpglem16 mapdpglem17N mapdpglem18 mapdpglem19 mapdpglem20 mapdpglem21 mapdpglem22 mapdpglem23 mapdpglem30a mapdpglem30b mapdpglem25 mapdpglem26 mapdpglem27 mapdpglem29 mapdpglem28 mapdpglem30 mapdpglem31 mapdpglem24 mapdpglem32 mapdpg baerlem3lem1 baerlem5alem1 baerlem5blem1 baerlem3lem2 baerlem5alem2 baerlem5blem2 baerlem3 baerlem5a baerlem5b baerlem5amN baerlem5bmN baerlem5abmN mapdindp0 mapdindp1 mapdindp2 mapdindp3 mapdindp4 mapdhval mapdhval0 mapdhval2 mapdhcl mapdheq mapdheq2 mapdheq2biN mapdheq4lem mapdheq4 mapdh6lem1N mapdh6lem2N mapdh6aN mapdh6b0N mapdh6bN mapdh6cN mapdh6dN mapdh6eN mapdh6fN mapdh6gN mapdh6hN mapdh6iN mapdh6jN mapdh6kN mapdh6N mapdh7eN mapdh7cN mapdh7dN mapdh7fN mapdh75e mapdh75cN mapdh75d mapdh75fN chvm df-hvmap hvmapffval hvmapfval hvmapval hvmapvalvalN hvmapidN hvmap1o hvmapclN hvmap1o2 hvmapcl2 hvmaplfl hvmaplkr mapdhvmap lspindp5 hdmaplem1 hdmaplem2N hdmaplem3 hdmaplem4 mapdh8a mapdh8aa mapdh8ab mapdh8ac mapdh8ad mapdh8b mapdh8c mapdh8d0N mapdh8d mapdh8e mapdh8g mapdh8i mapdh8j mapdh8 mapdh9a mapdh9aOLDN chdma1 chdma df-hdmap1 df-hdmap hdmap1ffval hdmap1fval hdmap1vallem hdmap1val hdmap1val0 hdmap1val2 hdmap1eq hdmap1cbv hdmap1valc hdmap1cl hdmap1eq2 hdmap1eq4N hdmap1l6lem1 hdmap1l6lem2 hdmap1l6a hdmap1l6b0N hdmap1l6b hdmap1l6c hdmap1l6d hdmap1l6e hdmap1l6f hdmap1l6g hdmap1l6h hdmap1l6i hdmap1l6j hdmap1l6k hdmap1l6 hdmap1eulem hdmap1eulemOLDN hdmap1eu hdmap1euOLDN hdmapffval hdmapfval hdmapval hdmapfnN hdmapcl hdmapval2lem hdmapval2 hdmapval0 hdmapeveclem hdmapevec hdmapevec2 hdmapval3lemN hdmapval3N hdmap10lem hdmap10 hdmap11lem1 hdmap11lem2 hdmapadd hdmapeq0 hdmapnzcl hdmapneg hdmapsub hdmap11 hdmaprnlem1N hdmaprnlem3N hdmaprnlem3uN hdmaprnlem4tN hdmaprnlem4N hdmaprnlem6N hdmaprnlem7N hdmaprnlem8N hdmaprnlem9N hdmaprnlem3eN hdmaprnlem10N hdmaprnlem11N hdmaprnlem15N hdmaprnlem16N hdmaprnlem17N hdmaprnN hdmapf1oN hdmap14lem1a hdmap14lem2a hdmap14lem1 hdmap14lem2N hdmap14lem3 hdmap14lem4a hdmap14lem4 hdmap14lem6 hdmap14lem7 hdmap14lem8 hdmap14lem9 hdmap14lem10 hdmap14lem11 hdmap14lem12 hdmap14lem13 hdmap14lem14 hdmap14lem15 chg df-hgmap hgmapffval hgmapfval hgmapval hgmapfnN hgmapcl hgmapdcl hgmapvs hgmapval0 hgmapval1 hgmapadd hgmapmul hgmaprnlem1N hgmaprnlem2N hgmaprnlem3N hgmaprnlem4N hgmaprnlem5N hgmaprnN hgmap11 hgmapf1oN hgmapeq0 hdmapipcl hdmapln1 hdmaplna1 hdmaplns1 hdmaplnm1 hdmaplna2 hdmapglnm2 hdmapgln2 hdmaplkr hdmapellkr hdmapip0 hdmapip1 hdmapip0com hdmapinvlem1 hdmapinvlem2 hdmapinvlem3 hdmapinvlem4 hdmapglem5 hgmapvvlem1 hgmapvvlem2 hgmapvvlem3 hgmapvv hdmapglem7a hdmapglem7b hdmapglem7 hdmapg hdmapoc chlh df-hlhil hlhilset hlhilsca hlhilbase hlhilplus hlhilslem hlhilsbase hlhilsplus hlhilsmul hlhilsbase2 hlhilsplus2 hlhilsmul2 hlhils0 hlhils1N hlhilvsca hlhilip hlhilipval hlhilnvl hlhillvec hlhildrng hlhilsrnglem hlhilsrng hlhil0 hlhillsm hlhilocv hlhillcs hlhilphllem hlhilhillem hlathil