Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlhilocv | Structured version Visualization version GIF version |
Description: The orthocomplement for the final constructed Hilbert space. (Contributed by NM, 23-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) |
Ref | Expression |
---|---|
hlhil0.h | ⊢ 𝐻 = (LHyp‘𝐾) |
hlhil0.l | ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊) |
hlhil0.u | ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) |
hlhil0.k | ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
hlhilocv.v | ⊢ 𝑉 = (Base‘𝐿) |
hlhilocv.n | ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊) |
hlhilocv.o | ⊢ 𝑂 = (ocv‘𝑈) |
hlhilocv.x | ⊢ (𝜑 → 𝑋 ⊆ 𝑉) |
Ref | Expression |
---|---|
hlhilocv | ⊢ (𝜑 → (𝑂‘𝑋) = (𝑁‘𝑋)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlhil0.h | . . . . 5 ⊢ 𝐻 = (LHyp‘𝐾) | |
2 | hlhil0.u | . . . . 5 ⊢ 𝑈 = ((HLHil‘𝐾)‘𝑊) | |
3 | hlhil0.k | . . . . 5 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | |
4 | hlhil0.l | . . . . 5 ⊢ 𝐿 = ((DVecH‘𝐾)‘𝑊) | |
5 | hlhilocv.v | . . . . 5 ⊢ 𝑉 = (Base‘𝐿) | |
6 | 1, 2, 3, 4, 5 | hlhilbase 40253 | . . . 4 ⊢ (𝜑 → 𝑉 = (Base‘𝑈)) |
7 | rabeq 3418 | . . . 4 ⊢ (𝑉 = (Base‘𝑈) → {𝑦 ∈ 𝑉 ∣ ∀𝑧 ∈ 𝑋 (𝑦(·𝑖‘𝑈)𝑧) = (0g‘(Scalar‘𝑈))} = {𝑦 ∈ (Base‘𝑈) ∣ ∀𝑧 ∈ 𝑋 (𝑦(·𝑖‘𝑈)𝑧) = (0g‘(Scalar‘𝑈))}) | |
8 | 6, 7 | syl 17 | . . 3 ⊢ (𝜑 → {𝑦 ∈ 𝑉 ∣ ∀𝑧 ∈ 𝑋 (𝑦(·𝑖‘𝑈)𝑧) = (0g‘(Scalar‘𝑈))} = {𝑦 ∈ (Base‘𝑈) ∣ ∀𝑧 ∈ 𝑋 (𝑦(·𝑖‘𝑈)𝑧) = (0g‘(Scalar‘𝑈))}) |
9 | eqid 2737 | . . . . . . 7 ⊢ ((HDMap‘𝐾)‘𝑊) = ((HDMap‘𝐾)‘𝑊) | |
10 | 3 | ad2antrr 724 | . . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑉) ∧ 𝑧 ∈ 𝑋) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
11 | eqid 2737 | . . . . . . 7 ⊢ (·𝑖‘𝑈) = (·𝑖‘𝑈) | |
12 | simplr 767 | . . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑉) ∧ 𝑧 ∈ 𝑋) → 𝑦 ∈ 𝑉) | |
13 | hlhilocv.x | . . . . . . . . 9 ⊢ (𝜑 → 𝑋 ⊆ 𝑉) | |
14 | 13 | adantr 482 | . . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → 𝑋 ⊆ 𝑉) |
15 | 14 | sselda 3936 | . . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑉) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑉) |
16 | 1, 4, 5, 9, 2, 10, 11, 12, 15 | hlhilipval 40270 | . . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑉) ∧ 𝑧 ∈ 𝑋) → (𝑦(·𝑖‘𝑈)𝑧) = ((((HDMap‘𝐾)‘𝑊)‘𝑧)‘𝑦)) |
17 | eqid 2737 | . . . . . . . . 9 ⊢ (Scalar‘𝐿) = (Scalar‘𝐿) | |
18 | eqid 2737 | . . . . . . . . 9 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈) | |
19 | eqid 2737 | . . . . . . . . 9 ⊢ (0g‘(Scalar‘𝐿)) = (0g‘(Scalar‘𝐿)) | |
20 | 1, 4, 17, 2, 18, 3, 19 | hlhils0 40266 | . . . . . . . 8 ⊢ (𝜑 → (0g‘(Scalar‘𝐿)) = (0g‘(Scalar‘𝑈))) |
21 | 20 | eqcomd 2743 | . . . . . . 7 ⊢ (𝜑 → (0g‘(Scalar‘𝑈)) = (0g‘(Scalar‘𝐿))) |
22 | 21 | ad2antrr 724 | . . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑉) ∧ 𝑧 ∈ 𝑋) → (0g‘(Scalar‘𝑈)) = (0g‘(Scalar‘𝐿))) |
23 | 16, 22 | eqeq12d 2753 | . . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑉) ∧ 𝑧 ∈ 𝑋) → ((𝑦(·𝑖‘𝑈)𝑧) = (0g‘(Scalar‘𝑈)) ↔ ((((HDMap‘𝐾)‘𝑊)‘𝑧)‘𝑦) = (0g‘(Scalar‘𝐿)))) |
24 | 23 | ralbidva 3169 | . . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (∀𝑧 ∈ 𝑋 (𝑦(·𝑖‘𝑈)𝑧) = (0g‘(Scalar‘𝑈)) ↔ ∀𝑧 ∈ 𝑋 ((((HDMap‘𝐾)‘𝑊)‘𝑧)‘𝑦) = (0g‘(Scalar‘𝐿)))) |
25 | 24 | rabbidva 3411 | . . 3 ⊢ (𝜑 → {𝑦 ∈ 𝑉 ∣ ∀𝑧 ∈ 𝑋 (𝑦(·𝑖‘𝑈)𝑧) = (0g‘(Scalar‘𝑈))} = {𝑦 ∈ 𝑉 ∣ ∀𝑧 ∈ 𝑋 ((((HDMap‘𝐾)‘𝑊)‘𝑧)‘𝑦) = (0g‘(Scalar‘𝐿))}) |
26 | 8, 25 | eqtr3d 2779 | . 2 ⊢ (𝜑 → {𝑦 ∈ (Base‘𝑈) ∣ ∀𝑧 ∈ 𝑋 (𝑦(·𝑖‘𝑈)𝑧) = (0g‘(Scalar‘𝑈))} = {𝑦 ∈ 𝑉 ∣ ∀𝑧 ∈ 𝑋 ((((HDMap‘𝐾)‘𝑊)‘𝑧)‘𝑦) = (0g‘(Scalar‘𝐿))}) |
27 | 13, 6 | sseqtrd 3976 | . . 3 ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝑈)) |
28 | eqid 2737 | . . . 4 ⊢ (Base‘𝑈) = (Base‘𝑈) | |
29 | eqid 2737 | . . . 4 ⊢ (0g‘(Scalar‘𝑈)) = (0g‘(Scalar‘𝑈)) | |
30 | hlhilocv.o | . . . 4 ⊢ 𝑂 = (ocv‘𝑈) | |
31 | 28, 11, 18, 29, 30 | ocvval 20978 | . . 3 ⊢ (𝑋 ⊆ (Base‘𝑈) → (𝑂‘𝑋) = {𝑦 ∈ (Base‘𝑈) ∣ ∀𝑧 ∈ 𝑋 (𝑦(·𝑖‘𝑈)𝑧) = (0g‘(Scalar‘𝑈))}) |
32 | 27, 31 | syl 17 | . 2 ⊢ (𝜑 → (𝑂‘𝑋) = {𝑦 ∈ (Base‘𝑈) ∣ ∀𝑧 ∈ 𝑋 (𝑦(·𝑖‘𝑈)𝑧) = (0g‘(Scalar‘𝑈))}) |
33 | hlhilocv.n | . . 3 ⊢ 𝑁 = ((ocH‘𝐾)‘𝑊) | |
34 | 1, 4, 5, 17, 19, 33, 9, 3, 13 | hdmapoc 40248 | . 2 ⊢ (𝜑 → (𝑁‘𝑋) = {𝑦 ∈ 𝑉 ∣ ∀𝑧 ∈ 𝑋 ((((HDMap‘𝐾)‘𝑊)‘𝑧)‘𝑦) = (0g‘(Scalar‘𝐿))}) |
35 | 26, 32, 34 | 3eqtr4d 2787 | 1 ⊢ (𝜑 → (𝑂‘𝑋) = (𝑁‘𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1541 ∈ wcel 2106 ∀wral 3062 {crab 3404 ⊆ wss 3902 ‘cfv 6484 (class class class)co 7342 Basecbs 17010 Scalarcsca 17063 ·𝑖cip 17065 0gc0g 17248 ocvcocv 20971 HLchlt 37666 LHypclh 38301 DVecHcdvh 39395 ocHcoch 39664 HDMapchdma 40109 HLHilchlh 40249 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-rep 5234 ax-sep 5248 ax-nul 5255 ax-pow 5313 ax-pr 5377 ax-un 7655 ax-cnex 11033 ax-resscn 11034 ax-1cn 11035 ax-icn 11036 ax-addcl 11037 ax-addrcl 11038 ax-mulcl 11039 ax-mulrcl 11040 ax-mulcom 11041 ax-addass 11042 ax-mulass 11043 ax-distr 11044 ax-i2m1 11045 ax-1ne0 11046 ax-1rid 11047 ax-rnegex 11048 ax-rrecex 11049 ax-cnre 11050 ax-pre-lttri 11051 ax-pre-lttrn 11052 ax-pre-ltadd 11053 ax-pre-mulgt0 11054 ax-riotaBAD 37269 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3444 df-sbc 3732 df-csb 3848 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3921 df-nul 4275 df-if 4479 df-pw 4554 df-sn 4579 df-pr 4581 df-tp 4583 df-op 4585 df-ot 4587 df-uni 4858 df-int 4900 df-iun 4948 df-iin 4949 df-br 5098 df-opab 5160 df-mpt 5181 df-tr 5215 df-id 5523 df-eprel 5529 df-po 5537 df-so 5538 df-fr 5580 df-we 5582 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6243 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6436 df-fun 6486 df-fn 6487 df-f 6488 df-f1 6489 df-fo 6490 df-f1o 6491 df-fv 6492 df-riota 7298 df-ov 7345 df-oprab 7346 df-mpo 7347 df-of 7600 df-om 7786 df-1st 7904 df-2nd 7905 df-tpos 8117 df-undef 8164 df-frecs 8172 df-wrecs 8203 df-recs 8277 df-rdg 8316 df-1o 8372 df-er 8574 df-map 8693 df-en 8810 df-dom 8811 df-sdom 8812 df-fin 8813 df-pnf 11117 df-mnf 11118 df-xr 11119 df-ltxr 11120 df-le 11121 df-sub 11313 df-neg 11314 df-nn 12080 df-2 12142 df-3 12143 df-4 12144 df-5 12145 df-6 12146 df-7 12147 df-8 12148 df-n0 12340 df-z 12426 df-uz 12689 df-fz 13346 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-submnd 18529 df-grp 18677 df-minusg 18678 df-sbg 18679 df-subg 18849 df-cntz 19020 df-oppg 19047 df-lsm 19338 df-cmn 19484 df-abl 19485 df-mgp 19816 df-ur 19833 df-ring 19880 df-oppr 19957 df-dvdsr 19978 df-unit 19979 df-invr 20009 df-dvr 20020 df-drng 20095 df-lmod 20231 df-lss 20300 df-lsp 20340 df-lvec 20471 df-ocv 20974 df-lsatoms 37292 df-lshyp 37293 df-lcv 37335 df-lfl 37374 df-lkr 37402 df-ldual 37440 df-oposet 37492 df-ol 37494 df-oml 37495 df-covers 37582 df-ats 37583 df-atl 37614 df-cvlat 37638 df-hlat 37667 df-llines 37815 df-lplanes 37816 df-lvols 37817 df-lines 37818 df-psubsp 37820 df-pmap 37821 df-padd 38113 df-lhyp 38305 df-laut 38306 df-ldil 38421 df-ltrn 38422 df-trl 38476 df-tgrp 39060 df-tendo 39072 df-edring 39074 df-dveca 39320 df-disoa 39346 df-dvech 39396 df-dib 39456 df-dic 39490 df-dih 39546 df-doch 39665 df-djh 39712 df-lcdual 39904 df-mapd 39942 df-hvmap 40074 df-hdmap1 40110 df-hdmap 40111 df-hlhil 40250 |
This theorem is referenced by: hlhillcs 40279 hlhilhillem 40281 |
Copyright terms: Public domain | W3C validator |