Theorem hlathil 40284

Description: Construction of a Hilbert space (df-hil 21018) 𝑈 from a Hilbert lattice (df-hlat 37669) 𝐾, where 𝑊 is a fixed but arbitrary hyperplane (co-atom) in 𝐾.

The Hilbert space 𝑈 is identical to the vector space ((DVecH‘𝐾)‘𝑊) (see dvhlvec 39428) 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 https://us.metamath.org/qlegif/mmql.html#what 39428.

𝑊 corresponds to the w in the proof of Theorem 13.4 of [Crawley] p. 111. Such a 𝑊 always exists since HL has lattice rank of at least 4 by df-hil 21018. 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	⊢ 𝐻 = (LHyp‘𝐾)
hlhilphllem.u	⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)
hlhilphl.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))

Assertion

Ref	Expression
hlathil	⊢ (𝜑 → 𝑈 ∈ Hil)

Proof of Theorem hlathil

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hlhilphl.h	. 2 ⊢ 𝐻 = (LHyp‘𝐾)
2		hlhilphllem.u	. 2 ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊)
3		hlhilphl.k	. 2 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
4		eqid 2736	. 2 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
5		eqid 2736	. 2 ⊢ ((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊)
6		eqid 2736	. 2 ⊢ (Base‘((DVecH‘𝐾)‘𝑊)) = (Base‘((DVecH‘𝐾)‘𝑊))
7		eqid 2736	. 2 ⊢ (+g‘((DVecH‘𝐾)‘𝑊)) = (+g‘((DVecH‘𝐾)‘𝑊))
8		eqid 2736	. 2 ⊢ ( ·𝑠 ‘((DVecH‘𝐾)‘𝑊)) = ( ·𝑠 ‘((DVecH‘𝐾)‘𝑊))
9		eqid 2736	. 2 ⊢ (Scalar‘((DVecH‘𝐾)‘𝑊)) = (Scalar‘((DVecH‘𝐾)‘𝑊))
10		eqid 2736	. 2 ⊢ (Base‘(Scalar‘((DVecH‘𝐾)‘𝑊))) = (Base‘(Scalar‘((DVecH‘𝐾)‘𝑊)))
11		eqid 2736	. 2 ⊢ (+g‘(Scalar‘((DVecH‘𝐾)‘𝑊))) = (+g‘(Scalar‘((DVecH‘𝐾)‘𝑊)))
12		eqid 2736	. 2 ⊢ (.r‘(Scalar‘((DVecH‘𝐾)‘𝑊))) = (.r‘(Scalar‘((DVecH‘𝐾)‘𝑊)))
13		eqid 2736	. 2 ⊢ (0g‘(Scalar‘((DVecH‘𝐾)‘𝑊))) = (0g‘(Scalar‘((DVecH‘𝐾)‘𝑊)))
14		eqid 2736	. 2 ⊢ (0g‘((DVecH‘𝐾)‘𝑊)) = (0g‘((DVecH‘𝐾)‘𝑊))
15		eqid 2736	. 2 ⊢ (·𝑖‘𝑈) = (·𝑖‘𝑈)
16		eqid 2736	. 2 ⊢ ((HDMap‘𝐾)‘𝑊) = ((HDMap‘𝐾)‘𝑊)
17		eqid 2736	. 2 ⊢ ((HGMap‘𝐾)‘𝑊) = ((HGMap‘𝐾)‘𝑊)
18		eqid 2736	. 2 ⊢ (𝑥 ∈ (Base‘((DVecH‘𝐾)‘𝑊)), 𝑦 ∈ (Base‘((DVecH‘𝐾)‘𝑊)) ↦ ((((HDMap‘𝐾)‘𝑊)‘𝑦)‘𝑥)) = (𝑥 ∈ (Base‘((DVecH‘𝐾)‘𝑊)), 𝑦 ∈ (Base‘((DVecH‘𝐾)‘𝑊)) ↦ ((((HDMap‘𝐾)‘𝑊)‘𝑦)‘𝑥))
19		eqid 2736	. 2 ⊢ (ocv‘𝑈) = (ocv‘𝑈)
20		eqid 2736	. 2 ⊢ (ClSubSp‘𝑈) = (ClSubSp‘𝑈)
21	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20	hlhilhillem 40283	1 ⊢ (𝜑 → 𝑈 ∈ Hil)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ∈ wcel 2105  ‘cfv 6480   ∈ cmpo 7340  Basecbs 17010  +_gcplusg 17060  ._rcmulr 17061  Scalarcsca 17063   ·_𝑠 cvsca 17064  ·_𝑖cip 17065  0_gc0g 17248  ocvcocv 20972  ClSubSpccss 20973  Hilchil 21015  HLchlt 37668  LHypclh 38303  DVecHcdvh 39397  HDMapchdma 40111  HGMapchg 40202  HLHilchlh 40251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-cnex 11029  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049  ax-pre-mulgt0 11050  ax-riotaBAD 37271

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-tp 4579  df-op 4581  df-ot 4583  df-uni 4854  df-int 4896  df-iun 4944  df-iin 4945  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-of 7596  df-om 7782  df-1st 7900  df-2nd 7901  df-tpos 8113  df-undef 8160  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-1o 8368  df-er 8570  df-map 8689  df-en 8806  df-dom 8807  df-sdom 8808  df-fin 8809  df-pnf 11113  df-mnf 11114  df-xr 11115  df-ltxr 11116  df-le 11117  df-sub 11309  df-neg 11310  df-nn 12076  df-2 12138  df-3 12139  df-4 12140  df-5 12141  df-6 12142  df-7 12143  df-8 12144  df-n0 12336  df-z 12422  df-uz 12685  df-fz 13342  df-struct 16946  df-sets 16963  df-slot 16981  df-ndx 16993  df-base 17011  df-ress 17040  df-plusg 17073  df-mulr 17074  df-starv 17075  df-sca 17076  df-vsca 17077  df-ip 17078  df-0g 17250  df-mre 17393  df-mrc 17394  df-acs 17396  df-proset 18111  df-poset 18129  df-plt 18146  df-lub 18162  df-glb 18163  df-join 18164  df-meet 18165  df-p0 18241  df-p1 18242  df-lat 18248  df-clat 18315  df-mgm 18424  df-sgrp 18473  df-mnd 18484  df-mhm 18528  df-submnd 18529  df-grp 18677  df-minusg 18678  df-sbg 18679  df-subg 18849  df-ghm 18929  df-cntz 19020  df-oppg 19047  df-lsm 19338  df-pj1 19339  df-cmn 19484  df-abl 19485  df-mgp 19817  df-ur 19834  df-ring 19881  df-oppr 19958  df-dvdsr 19979  df-unit 19980  df-invr 20010  df-dvr 20021  df-rnghom 20055  df-drng 20096  df-subrg 20128  df-staf 20212  df-srng 20213  df-lmod 20232  df-lss 20301  df-lsp 20341  df-lmhm 20391  df-lvec 20472  df-sra 20541  df-rgmod 20542  df-phl 20938  df-ocv 20975  df-css 20976  df-pj 21017  df-hil 21018  df-lsatoms 37294  df-lshyp 37295  df-lcv 37337  df-lfl 37376  df-lkr 37404  df-ldual 37442  df-oposet 37494  df-ol 37496  df-oml 37497  df-covers 37584  df-ats 37585  df-atl 37616  df-cvlat 37640  df-hlat 37669  df-llines 37817  df-lplanes 37818  df-lvols 37819  df-lines 37820  df-psubsp 37822  df-pmap 37823  df-padd 38115  df-lhyp 38307  df-laut 38308  df-ldil 38423  df-ltrn 38424  df-trl 38478  df-tgrp 39062  df-tendo 39074  df-edring 39076  df-dveca 39322  df-disoa 39348  df-dvech 39398  df-dib 39458  df-dic 39492  df-dih 39548  df-doch 39667  df-djh 39714  df-lcdual 39906  df-mapd 39944  df-hvmap 40076  df-hdmap1 40112  df-hdmap 40113  df-hgmap 40203  df-hlhil 40252

This theorem is referenced by: (None)