Mathbox for Norm Megill < Previous   Wrap > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hlathil Unicode version

Theorem hlathil 32095
 Description: Construction of a Hilbert space (df-hil 16868) from a Hilbert lattice (df-hlat 29482) , where is a fixed but arbitrary hyperplane (co-atom) in . The Hilbert space is identical to the vector space (see dvhlvec 31240) except that it is extended with involution and inner product components. The construction of these two components is provided by Theorem 3.6 in [Holland95] p. 13, whose proof we follow loosely. An example of involution is the complex conjugate when the division ring is the field of complex numbers. The nature of the division ring we constructed is indeterminate, however, until we specialize the initial Hilbert lattice with additional conditions found by Maria Solèr in 1995 and refined by René Mayet in 1998 that result in a division ring isomorphic to . See additional discussion at http://us.metamath.org/qlegif/mmql.html#what. corresponds to the w in the proof of Theorem 13.4 of [Crawley] p. 111. Such a always exists since has lattice rank of at least 4 by df-hil 16868. It can be eliminated if we just want to show the existence of a Hilbert space, as is done in the literature. (Contributed by NM, 23-Jun-2015.)
Hypotheses
Ref Expression
hlhilphl.h
hlhilphllem.u HLHil
hlhilphl.k
Assertion
Ref Expression
hlathil

Proof of Theorem hlathil
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hlhilphl.h . 2
2 hlhilphllem.u . 2 HLHil
3 hlhilphl.k . 2
4 eqid 2401 . 2 Scalar Scalar
5 eqid 2401 . 2
6 eqid 2401 . 2
7 eqid 2401 . 2
8 eqid 2401 . 2
9 eqid 2401 . 2 Scalar Scalar
10 eqid 2401 . 2 Scalar Scalar
11 eqid 2401 . 2 Scalar Scalar
12 eqid 2401 . 2 Scalar Scalar
13 eqid 2401 . 2 Scalar Scalar
14 eqid 2401 . 2
15 eqid 2401 . 2
16 eqid 2401 . 2 HDMap HDMap
17 eqid 2401 . 2 HGMap HGMap
18 eqid 2401 . 2 HDMap HDMap
19 eqid 2401 . 2
20 eqid 2401 . 2
211, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20hlhilhillem 32094 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   wceq 1649   wcel 1721  cfv 5408   cmpt2 6036  cbs 13410   cplusg 13470  cmulr 13471  Scalarcsca 13473  cvsca 13474  cip 13475  c0g 13664  cocv 16824  ccss 16825  chs 16865  chlt 29481  clh 30114  cdvh 31209  HDMapchdma 31924  HGMapchg 32017  HLHilchlh 32066 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-cnex 8993  ax-resscn 8994  ax-1cn 8995  ax-icn 8996  ax-addcl 8997  ax-addrcl 8998  ax-mulcl 8999  ax-mulrcl 9000  ax-mulcom 9001  ax-addass 9002  ax-mulass 9003  ax-distr 9004  ax-i2m1 9005  ax-1ne0 9006  ax-1rid 9007  ax-rnegex 9008  ax-rrecex 9009  ax-cnre 9010  ax-pre-lttri 9011  ax-pre-lttrn 9012  ax-pre-ltadd 9013  ax-pre-mulgt0 9014 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-fal 1326  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-ot 3781  df-uni 3972  df-int 4007  df-iun 4051  df-iin 4052  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-of 6258  df-1st 6302  df-2nd 6303  df-tpos 6429  df-undef 6493  df-riota 6499  df-recs 6583  df-rdg 6618  df-1o 6674  df-oadd 6678  df-er 6855  df-map 6970  df-en 7060  df-dom 7061  df-sdom 7062  df-fin 7063  df-pnf 9069  df-mnf 9070  df-xr 9071  df-ltxr 9072  df-le 9073  df-sub 9239  df-neg 9240  df-nn 9947  df-2 10004  df-3 10005  df-4 10006  df-5 10007  df-6 10008  df-7 10009  df-8 10010  df-n0 10168  df-z 10229  df-uz 10435  df-fz 10990  df-struct 13412  df-ndx 13413  df-slot 13414  df-base 13415  df-sets 13416  df-ress 13417  df-plusg 13483  df-mulr 13484  df-starv 13485  df-sca 13486  df-vsca 13487  df-ip 13488  df-0g 13668  df-mre 13752  df-mrc 13753  df-acs 13755  df-poset 14344  df-plt 14356  df-lub 14372  df-glb 14373  df-join 14374  df-meet 14375  df-p0 14409  df-p1 14410  df-lat 14416  df-clat 14478  df-mnd 14631  df-mhm 14679  df-submnd 14680  df-grp 14753  df-minusg 14754  df-sbg 14755  df-subg 14882  df-ghm 14945  df-cntz 15057  df-oppg 15083  df-lsm 15211  df-pj1 15212  df-cmn 15355  df-abl 15356  df-mgp 15590  df-rng 15604  df-ur 15606  df-oppr 15669  df-dvdsr 15687  df-unit 15688  df-invr 15718  df-dvr 15729  df-rnghom 15760  df-drng 15778  df-subrg 15807  df-staf 15874  df-srng 15875  df-lmod 15893  df-lss 15950  df-lsp 15989  df-lmhm 16039  df-lvec 16116  df-sra 16185  df-rgmod 16186  df-phl 16794  df-ocv 16827  df-css 16828  df-pj 16867  df-hil 16868  df-lsatoms 29107  df-lshyp 29108  df-lcv 29150  df-lfl 29189  df-lkr 29217  df-ldual 29255  df-oposet 29307  df-ol 29309  df-oml 29310  df-covers 29397  df-ats 29398  df-atl 29429  df-cvlat 29453  df-hlat 29482  df-llines 29628  df-lplanes 29629  df-lvols 29630  df-lines 29631  df-psubsp 29633  df-pmap 29634  df-padd 29926  df-lhyp 30118  df-laut 30119  df-ldil 30234  df-ltrn 30235  df-trl 30289  df-tgrp 30873  df-tendo 30885  df-edring 30887  df-dveca 31133  df-disoa 31160  df-dvech 31210  df-dib 31270  df-dic 31304  df-dih 31360  df-doch 31479  df-djh 31526  df-lcdual 31718  df-mapd 31756  df-hvmap 31888  df-hdmap1 31925  df-hdmap 31926  df-hgmap 32018  df-hlhil 32067
 Copyright terms: Public domain W3C validator