hdmapoc - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hdmapoc		Structured version Visualization version GIF version

Theorem hdmapoc 42733

Description: Express our constructed orthocomplement (polarity) in terms of the Hilbert space definition of orthocomplement. Lines 24 and 25 in [Holland95] p. 14. (Contributed by NM, 17-Jun-2015.)

**Hypotheses**
Ref	Expression
hdmapoc.h	⊢ 𝐻 = (LHyp‘𝐾)
hdmapoc.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
hdmapoc.v	⊢ 𝑉 = (Base‘𝑈)
hdmapoc.r	⊢ 𝑅 = (Scalar‘𝑈)
hdmapoc.z	⊢ 0 = (0_g‘𝑅)
hdmapoc.o	⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)
hdmapoc.s	⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
hdmapoc.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
hdmapoc.x	⊢ (𝜑 → 𝑋 ⊆ 𝑉)

**Assertion**
Ref	Expression
hdmapoc	⊢ (𝜑 → (𝑂‘𝑋) = {𝑦 ∈ 𝑉 ∣ ∀𝑧 ∈ 𝑋 ((𝑆‘𝑧)‘𝑦) = 0 })

Distinct variable groups: 𝑦,𝑧,𝑂 𝑧,𝑉 𝑦,𝑋,𝑧 𝜑,𝑦,𝑧 Allowed substitution hints: 𝑅(𝑦, 𝑧) 𝑆(𝑦, 𝑧) 𝑈(𝑦, 𝑧) 𝐻(𝑦, 𝑧) 𝐾(𝑦, 𝑧) 𝑉(𝑦) 𝑊(𝑦, 𝑧) 0 (𝑦, 𝑧)

**Proof of Theorem hdmapoc**
Step	Hyp	Ref	Expression
1		hdmapoc.k	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		hdmapoc.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ⊆ 𝑉)
3		hdmapoc.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
4		hdmapoc.u	. . . . . . . 8 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
5		hdmapoc.v	. . . . . . . 8 ⊢ 𝑉 = (Base‘𝑈)
6		hdmapoc.o	. . . . . . . 8 ⊢ 𝑂 = ((ocH‘𝐾)‘𝑊)
7	3, 4, 5, 6	dochssv 42157	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (𝑂‘𝑋) ⊆ 𝑉)
8	1, 2, 7	syl2anc 595	. . . . . 6 ⊢ (𝜑 → (𝑂‘𝑋) ⊆ 𝑉)
9	8	sseld 3935	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ (𝑂‘𝑋) → 𝑦 ∈ 𝑉))
10	9	pm4.71rd 571	. . . 4 ⊢ (𝜑 → (𝑦 ∈ (𝑂‘𝑋) ↔ (𝑦 ∈ 𝑉 ∧ 𝑦 ∈ (𝑂‘𝑋))))
11		eqid 2762	. . . . . . . . 9 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
12		eqid 2762	. . . . . . . . 9 ⊢ (LSpan‘𝑈) = (LSpan‘𝑈)
13	3, 4, 1	dvhlmod 41912	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ LMod)
14	13	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → 𝑈 ∈ LMod)
15	3, 4, 5, 11, 6	dochlss 42156	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (𝑂‘𝑋) ∈ (LSubSp‘𝑈))
16	1, 2, 15	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → (𝑂‘𝑋) ∈ (LSubSp‘𝑈))
17	16	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (𝑂‘𝑋) ∈ (LSubSp‘𝑈))
18		simpr 489	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → 𝑦 ∈ 𝑉)
19	5, 11, 12, 14, 17, 18	ellspsn5b 21127	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (𝑦 ∈ (𝑂‘𝑋) ↔ ((LSpan‘𝑈)‘{𝑦}) ⊆ (𝑂‘𝑋)))
20		eqid 2762	. . . . . . . . 9 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
21	1	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
22	3, 4, 5, 12, 20	dihlsprn 42133	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑦 ∈ 𝑉) → ((LSpan‘𝑈)‘{𝑦}) ∈ ran ((DIsoH‘𝐾)‘𝑊))
23	21, 18, 22	syl2anc 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → ((LSpan‘𝑈)‘{𝑦}) ∈ ran ((DIsoH‘𝐾)‘𝑊))
24	3, 20, 4, 5, 6	dochcl 42155	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ⊆ 𝑉) → (𝑂‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊))
25	1, 2, 24	syl2anc 595	. . . . . . . . . 10 ⊢ (𝜑 → (𝑂‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊))
26	25	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (𝑂‘𝑋) ∈ ran ((DIsoH‘𝐾)‘𝑊))
27	3, 20, 6, 21, 23, 26	dochord 42172	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (((LSpan‘𝑈)‘{𝑦}) ⊆ (𝑂‘𝑋) ↔ (𝑂‘(𝑂‘𝑋)) ⊆ (𝑂‘((LSpan‘𝑈)‘{𝑦}))))
28	18	snssd 4751	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → {𝑦} ⊆ 𝑉)
29	3, 4, 6, 5, 12, 21, 28	dochocsp 42181	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (𝑂‘((LSpan‘𝑈)‘{𝑦})) = (𝑂‘{𝑦}))
30	29	sseq2d 3968	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → ((𝑂‘(𝑂‘𝑋)) ⊆ (𝑂‘((LSpan‘𝑈)‘{𝑦})) ↔ (𝑂‘(𝑂‘𝑋)) ⊆ (𝑂‘{𝑦})))
31	2	adantr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → 𝑋 ⊆ 𝑉)
32	3, 20, 4, 5, 6	dochcl 42155	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑦} ⊆ 𝑉) → (𝑂‘{𝑦}) ∈ ran ((DIsoH‘𝐾)‘𝑊))
33	21, 28, 32	syl2anc 595	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (𝑂‘{𝑦}) ∈ ran ((DIsoH‘𝐾)‘𝑊))
34	3, 4, 5, 20, 6, 21, 31, 33	dochsscl 42170	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (𝑋 ⊆ (𝑂‘{𝑦}) ↔ (𝑂‘(𝑂‘𝑋)) ⊆ (𝑂‘{𝑦})))
35	30, 34	bitr4d 285	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → ((𝑂‘(𝑂‘𝑋)) ⊆ (𝑂‘((LSpan‘𝑈)‘{𝑦})) ↔ 𝑋 ⊆ (𝑂‘{𝑦})))
36	19, 27, 35	3bitrd 308	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (𝑦 ∈ (𝑂‘𝑋) ↔ 𝑋 ⊆ (𝑂‘{𝑦})))
37		dfss3 3925	. . . . . . 7 ⊢ (𝑋 ⊆ (𝑂‘{𝑦}) ↔ ∀𝑧 ∈ 𝑋 𝑧 ∈ (𝑂‘{𝑦}))
38	36, 37	bitrdi 290	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (𝑦 ∈ (𝑂‘𝑋) ↔ ∀𝑧 ∈ 𝑋 𝑧 ∈ (𝑂‘{𝑦})))
39		hdmapoc.r	. . . . . . . . 9 ⊢ 𝑅 = (Scalar‘𝑈)
40		hdmapoc.z	. . . . . . . . 9 ⊢ 0 = (0_g‘𝑅)
41		hdmapoc.s	. . . . . . . . 9 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
42	1	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑉) ∧ 𝑧 ∈ 𝑋) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
43	31	sselda 3936	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑉) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑉)
44		simplr 780	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑉) ∧ 𝑧 ∈ 𝑋) → 𝑦 ∈ 𝑉)
45	3, 6, 4, 5, 39, 40, 41, 42, 43, 44	hdmapellkr 42716	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑉) ∧ 𝑧 ∈ 𝑋) → (((𝑆‘𝑧)‘𝑦) = 0 ↔ 𝑦 ∈ (𝑂‘{𝑧})))
46	3, 6, 4, 5, 42, 44, 43	dochsncom 42184	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑉) ∧ 𝑧 ∈ 𝑋) → (𝑦 ∈ (𝑂‘{𝑧}) ↔ 𝑧 ∈ (𝑂‘{𝑦})))
47	45, 46	bitrd 282	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑉) ∧ 𝑧 ∈ 𝑋) → (((𝑆‘𝑧)‘𝑦) = 0 ↔ 𝑧 ∈ (𝑂‘{𝑦})))
48	47	ralbidva 3185	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (∀𝑧 ∈ 𝑋 ((𝑆‘𝑧)‘𝑦) = 0 ↔ ∀𝑧 ∈ 𝑋 𝑧 ∈ (𝑂‘{𝑦})))
49	38, 48	bitr4d 285	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉) → (𝑦 ∈ (𝑂‘𝑋) ↔ ∀𝑧 ∈ 𝑋 ((𝑆‘𝑧)‘𝑦) = 0 ))
50	49	pm5.32da 589	. . . 4 ⊢ (𝜑 → ((𝑦 ∈ 𝑉 ∧ 𝑦 ∈ (𝑂‘𝑋)) ↔ (𝑦 ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑋 ((𝑆‘𝑧)‘𝑦) = 0 )))
51	10, 50	bitrd 282	. . 3 ⊢ (𝜑 → (𝑦 ∈ (𝑂‘𝑋) ↔ (𝑦 ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑋 ((𝑆‘𝑧)‘𝑦) = 0 )))
52	51	eqabdv 2895	. 2 ⊢ (𝜑 → (𝑂‘𝑋) = {𝑦 ∣ (𝑦 ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑋 ((𝑆‘𝑧)‘𝑦) = 0 )})
53		df-rab 3416	. 2 ⊢ {𝑦 ∈ 𝑉 ∣ ∀𝑧 ∈ 𝑋 ((𝑆‘𝑧)‘𝑦) = 0 } = {𝑦 ∣ (𝑦 ∈ 𝑉 ∧ ∀𝑧 ∈ 𝑋 ((𝑆‘𝑧)‘𝑦) = 0 )}
54	52, 53	eqtr4di 2815	1 ⊢ (𝜑 → (𝑂‘𝑋) = {𝑦 ∈ 𝑉 ∣ ∀𝑧 ∈ 𝑋 ((𝑆‘𝑧)‘𝑦) = 0 })

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 400 = wceq 1569 ∈ wcel 2142 {cab 2740 ∀wral 3078 {crab 3415 ⊆ wss 3904 {csn 4588 ran crn 5661 ‘cfv 6536 Basecbs 17275 Scalarcsca 17319 0_gc0g 17498 LModclmod 20992 LSubSpclss 21063 LSpanclspn 21103 HLchlt 40152 LHypclh 40786 DVecHcdvh 41880 DIsoHcdih 42030 ocHcoch 42149 HDMapchdma 42594

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-riotaBAD 39755

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-ot 4597 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7676 df-om 7861 df-1st 7984 df-2nd 7985 df-tpos 8220 df-undef 8267 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-2o 8452 df-er 8692 df-map 8824 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-nn 12240 df-2 12309 df-3 12310 df-4 12311 df-5 12312 df-6 12313 df-n0 12511 df-z 12598 df-uz 12869 df-fz 13542 df-struct 17213 df-sets 17230 df-slot 17248 df-ndx 17260 df-base 17276 df-ress 17297 df-plusg 17329 df-mulr 17330 df-sca 17332 df-vsca 17333 df-0g 17500 df-mre 17644 df-mrc 17645 df-acs 17647 df-proset 18356 df-poset 18375 df-plt 18390 df-lub 18406 df-glb 18407 df-join 18408 df-meet 18409 df-p0 18485 df-p1 18486 df-lat 18494 df-clat 18561 df-mgm 18704 df-sgrp 18783 df-mnd 18799 df-submnd 18848 df-grp 19009 df-minusg 19010 df-sbg 19011 df-subg 19195 df-cntz 19393 df-oppg 19422 df-lsm 19712 df-cmn 19858 df-abl 19859 df-mgp 20223 df-rng 20237 df-ur 20270 df-ring 20323 df-oppr 20426 df-dvdsr 20446 df-unit 20447 df-invr 20477 df-dvr 20490 df-nzr 20621 df-rlreg 20804 df-domn 20805 df-drng 20840 df-lmod 20994 df-lss 21064 df-lsp 21104 df-lvec 21235 df-lsatoms 39778 df-lshyp 39779 df-lcv 39821 df-lfl 39860 df-lkr 39888 df-ldual 39926 df-oposet 39978 df-ol 39980 df-oml 39981 df-covers 40068 df-ats 40069 df-atl 40100 df-cvlat 40124 df-hlat 40153 df-llines 40300 df-lplanes 40301 df-lvols 40302 df-lines 40303 df-psubsp 40305 df-pmap 40306 df-padd 40598 df-lhyp 40790 df-laut 40791 df-ldil 40906 df-ltrn 40907 df-trl 40961 df-tgrp 41545 df-tendo 41557 df-edring 41559 df-dveca 41805 df-disoa 41831 df-dvech 41881 df-dib 41941 df-dic 41975 df-dih 42031 df-doch 42150 df-djh 42197 df-lcdual 42389 df-mapd 42427 df-hvmap 42559 df-hdmap1 42595 df-hdmap 42596

This theorem is used by: hlhilocv 42759

W3C validator