Theorem hlathil 41909

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

The Hilbert space 𝑈 is identical to the vector space ((DVecH‘𝐾)‘𝑊) (see dvhlvec 41053) 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 41053.

𝑊 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 21724. 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 2733	. 2 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
5		eqid 2733	. 2 ⊢ ((DVecH‘𝐾)‘𝑊) = ((DVecH‘𝐾)‘𝑊)
6		eqid 2733	. 2 ⊢ (Base‘((DVecH‘𝐾)‘𝑊)) = (Base‘((DVecH‘𝐾)‘𝑊))
7		eqid 2733	. 2 ⊢ (+g‘((DVecH‘𝐾)‘𝑊)) = (+g‘((DVecH‘𝐾)‘𝑊))
8		eqid 2733	. 2 ⊢ ( ·𝑠 ‘((DVecH‘𝐾)‘𝑊)) = ( ·𝑠 ‘((DVecH‘𝐾)‘𝑊))
9		eqid 2733	. 2 ⊢ (Scalar‘((DVecH‘𝐾)‘𝑊)) = (Scalar‘((DVecH‘𝐾)‘𝑊))
10		eqid 2733	. 2 ⊢ (Base‘(Scalar‘((DVecH‘𝐾)‘𝑊))) = (Base‘(Scalar‘((DVecH‘𝐾)‘𝑊)))
11		eqid 2733	. 2 ⊢ (+g‘(Scalar‘((DVecH‘𝐾)‘𝑊))) = (+g‘(Scalar‘((DVecH‘𝐾)‘𝑊)))
12		eqid 2733	. 2 ⊢ (.r‘(Scalar‘((DVecH‘𝐾)‘𝑊))) = (.r‘(Scalar‘((DVecH‘𝐾)‘𝑊)))
13		eqid 2733	. 2 ⊢ (0g‘(Scalar‘((DVecH‘𝐾)‘𝑊))) = (0g‘(Scalar‘((DVecH‘𝐾)‘𝑊)))
14		eqid 2733	. 2 ⊢ (0g‘((DVecH‘𝐾)‘𝑊)) = (0g‘((DVecH‘𝐾)‘𝑊))
15		eqid 2733	. 2 ⊢ (·𝑖‘𝑈) = (·𝑖‘𝑈)
16		eqid 2733	. 2 ⊢ ((HDMap‘𝐾)‘𝑊) = ((HDMap‘𝐾)‘𝑊)
17		eqid 2733	. 2 ⊢ ((HGMap‘𝐾)‘𝑊) = ((HGMap‘𝐾)‘𝑊)
18		eqid 2733	. 2 ⊢ (𝑥 ∈ (Base‘((DVecH‘𝐾)‘𝑊)), 𝑦 ∈ (Base‘((DVecH‘𝐾)‘𝑊)) ↦ ((((HDMap‘𝐾)‘𝑊)‘𝑦)‘𝑥)) = (𝑥 ∈ (Base‘((DVecH‘𝐾)‘𝑊)), 𝑦 ∈ (Base‘((DVecH‘𝐾)‘𝑊)) ↦ ((((HDMap‘𝐾)‘𝑊)‘𝑦)‘𝑥))
19		eqid 2733	. 2 ⊢ (ocv‘𝑈) = (ocv‘𝑈)
20		eqid 2733	. 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 41908	1 ⊢ (𝜑 → 𝑈 ∈ Hil)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1535   ∈ wcel 2104  ‘cfv 6559   ∈ cmpo 7428  Basecbs 17235  +_gcplusg 17288  ._rcmulr 17289  Scalarcsca 17291   ·_𝑠 cvsca 17292  ·_𝑖cip 17293  0_gc0g 17476  ocvcocv 21678  ClSubSpccss 21679  Hilchil 21721  HLchlt 39293  LHypclh 39928  DVecHcdvh 41022  HDMapchdma 41736  HGMapchg 41827  HLHilchlh 41876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1963  ax-7 2003  ax-8 2106  ax-9 2114  ax-10 2137  ax-11 2153  ax-12 2173  ax-ext 2704  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7748  ax-cnex 11203  ax-resscn 11204  ax-1cn 11205  ax-icn 11206  ax-addcl 11207  ax-addrcl 11208  ax-mulcl 11209  ax-mulrcl 11210  ax-mulcom 11211  ax-addass 11212  ax-mulass 11213  ax-distr 11214  ax-i2m1 11215  ax-1ne0 11216  ax-1rid 11217  ax-rnegex 11218  ax-rrecex 11219  ax-cnre 11220  ax-pre-lttri 11221  ax-pre-lttrn 11222  ax-pre-ltadd 11223  ax-pre-mulgt0 11224  ax-riotaBAD 38896

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1538  df-fal 1548  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2536  df-eu 2565  df-clab 2711  df-cleq 2725  df-clel 2812  df-nfc 2888  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3479  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-ot 4640  df-uni 4916  df-int 4955  df-iun 5001  df-iin 5002  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6318  df-ord 6384  df-on 6385  df-lim 6386  df-suc 6387  df-iota 6511  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-of 7692  df-om 7882  df-1st 8008  df-2nd 8009  df-tpos 8245  df-undef 8292  df-frecs 8300  df-wrecs 8331  df-recs 8405  df-rdg 8444  df-1o 8500  df-2o 8501  df-er 8739  df-map 8862  df-en 8980  df-dom 8981  df-sdom 8982  df-fin 8983  df-pnf 11289  df-mnf 11290  df-xr 11291  df-ltxr 11292  df-le 11293  df-sub 11486  df-neg 11487  df-nn 12259  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-7 12326  df-8 12327  df-n0 12519  df-z 12606  df-uz 12871  df-fz 13539  df-struct 17171  df-sets 17188  df-slot 17206  df-ndx 17218  df-base 17236  df-ress 17265  df-plusg 17301  df-mulr 17302  df-starv 17303  df-sca 17304  df-vsca 17305  df-ip 17306  df-0g 17478  df-mre 17621  df-mrc 17622  df-acs 17624  df-proset 18342  df-poset 18360  df-plt 18377  df-lub 18393  df-glb 18394  df-join 18395  df-meet 18396  df-p0 18472  df-p1 18473  df-lat 18479  df-clat 18546  df-mgm 18655  df-sgrp 18734  df-mnd 18750  df-mhm 18795  df-submnd 18796  df-grp 18953  df-minusg 18954  df-sbg 18955  df-subg 19140  df-ghm 19230  df-cntz 19334  df-oppg 19363  df-lsm 19655  df-pj1 19656  df-cmn 19801  df-abl 19802  df-mgp 20139  df-rng 20157  df-ur 20186  df-ring 20239  df-oppr 20337  df-dvdsr 20360  df-unit 20361  df-invr 20391  df-dvr 20404  df-rhm 20475  df-nzr 20516  df-subrg 20574  df-rlreg 20693  df-domn 20694  df-drng 20730  df-staf 20839  df-srng 20840  df-lmod 20859  df-lss 20930  df-lsp 20970  df-lmhm 21021  df-lvec 21102  df-sra 21172  df-rgmod 21173  df-phl 21644  df-ocv 21681  df-css 21682  df-pj 21723  df-hil 21724  df-lsatoms 38919  df-lshyp 38920  df-lcv 38962  df-lfl 39001  df-lkr 39029  df-ldual 39067  df-oposet 39119  df-ol 39121  df-oml 39122  df-covers 39209  df-ats 39210  df-atl 39241  df-cvlat 39265  df-hlat 39294  df-llines 39442  df-lplanes 39443  df-lvols 39444  df-lines 39445  df-psubsp 39447  df-pmap 39448  df-padd 39740  df-lhyp 39932  df-laut 39933  df-ldil 40048  df-ltrn 40049  df-trl 40103  df-tgrp 40687  df-tendo 40699  df-edring 40701  df-dveca 40947  df-disoa 40973  df-dvech 41023  df-dib 41083  df-dic 41117  df-dih 41173  df-doch 41292  df-djh 41339  df-lcdual 41531  df-mapd 41569  df-hvmap 41701  df-hdmap1 41737  df-hdmap 41738  df-hgmap 41828  df-hlhil 41877

This theorem is referenced by: (None)