![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > dochoc | Structured version Visualization version GIF version |
Description: Double negative law for orthocomplement of a closed subspace. (Contributed by NM, 14-Mar-2014.) |
Ref | Expression |
---|---|
dochoc.h | ⊢ 𝐻 = (LHyp‘𝐾) |
dochoc.i | ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
dochoc.o | ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) |
Ref | Expression |
---|---|
dochoc | ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2826 | . . . 4 ⊢ (oc‘𝐾) = (oc‘𝐾) | |
2 | dochoc.h | . . . 4 ⊢ 𝐻 = (LHyp‘𝐾) | |
3 | dochoc.i | . . . 4 ⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) | |
4 | dochoc.o | . . . 4 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊) | |
5 | 1, 2, 3, 4 | dochvalr 37433 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ( ⊥ ‘𝑋) = (𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋)))) |
6 | 5 | fveq2d 6438 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ( ⊥ ‘( ⊥ ‘𝑋)) = ( ⊥ ‘(𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋))))) |
7 | hlop 35438 | . . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) | |
8 | 7 | ad2antrr 719 | . . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → 𝐾 ∈ OP) |
9 | eqid 2826 | . . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
10 | 9, 2, 3 | dihcnvcl 37347 | . . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → (◡𝐼‘𝑋) ∈ (Base‘𝐾)) |
11 | 9, 1 | opoccl 35270 | . . . . . 6 ⊢ ((𝐾 ∈ OP ∧ (◡𝐼‘𝑋) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘(◡𝐼‘𝑋)) ∈ (Base‘𝐾)) |
12 | 8, 10, 11 | syl2anc 581 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ((oc‘𝐾)‘(◡𝐼‘𝑋)) ∈ (Base‘𝐾)) |
13 | 9, 2, 3 | dihcl 37346 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((oc‘𝐾)‘(◡𝐼‘𝑋)) ∈ (Base‘𝐾)) → (𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋))) ∈ ran 𝐼) |
14 | 12, 13 | syldan 587 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → (𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋))) ∈ ran 𝐼) |
15 | 1, 2, 3, 4 | dochvalr 37433 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋))) ∈ ran 𝐼) → ( ⊥ ‘(𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋)))) = (𝐼‘((oc‘𝐾)‘(◡𝐼‘(𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋))))))) |
16 | 14, 15 | syldan 587 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ( ⊥ ‘(𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋)))) = (𝐼‘((oc‘𝐾)‘(◡𝐼‘(𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋))))))) |
17 | 9, 2, 3 | dihcnvid1 37348 | . . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((oc‘𝐾)‘(◡𝐼‘𝑋)) ∈ (Base‘𝐾)) → (◡𝐼‘(𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋)))) = ((oc‘𝐾)‘(◡𝐼‘𝑋))) |
18 | 12, 17 | syldan 587 | . . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → (◡𝐼‘(𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋)))) = ((oc‘𝐾)‘(◡𝐼‘𝑋))) |
19 | 18 | fveq2d 6438 | . . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ((oc‘𝐾)‘(◡𝐼‘(𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋))))) = ((oc‘𝐾)‘((oc‘𝐾)‘(◡𝐼‘𝑋)))) |
20 | 9, 1 | opococ 35271 | . . . . . . 7 ⊢ ((𝐾 ∈ OP ∧ (◡𝐼‘𝑋) ∈ (Base‘𝐾)) → ((oc‘𝐾)‘((oc‘𝐾)‘(◡𝐼‘𝑋))) = (◡𝐼‘𝑋)) |
21 | 8, 10, 20 | syl2anc 581 | . . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ((oc‘𝐾)‘((oc‘𝐾)‘(◡𝐼‘𝑋))) = (◡𝐼‘𝑋)) |
22 | 19, 21 | eqtrd 2862 | . . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ((oc‘𝐾)‘(◡𝐼‘(𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋))))) = (◡𝐼‘𝑋)) |
23 | 22 | fveq2d 6438 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → (𝐼‘((oc‘𝐾)‘(◡𝐼‘(𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋)))))) = (𝐼‘(◡𝐼‘𝑋))) |
24 | 2, 3 | dihcnvid2 37349 | . . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → (𝐼‘(◡𝐼‘𝑋)) = 𝑋) |
25 | 23, 24 | eqtrd 2862 | . . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → (𝐼‘((oc‘𝐾)‘(◡𝐼‘(𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋)))))) = 𝑋) |
26 | 16, 25 | eqtrd 2862 | . 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ( ⊥ ‘(𝐼‘((oc‘𝐾)‘(◡𝐼‘𝑋)))) = 𝑋) |
27 | 6, 26 | eqtrd 2862 | 1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ ran 𝐼) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1658 ∈ wcel 2166 ◡ccnv 5342 ran crn 5344 ‘cfv 6124 Basecbs 16223 occoc 16314 OPcops 35248 HLchlt 35426 LHypclh 36060 DIsoHcdih 37304 ocHcoch 37423 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-rep 4995 ax-sep 5006 ax-nul 5014 ax-pow 5066 ax-pr 5128 ax-un 7210 ax-cnex 10309 ax-resscn 10310 ax-1cn 10311 ax-icn 10312 ax-addcl 10313 ax-addrcl 10314 ax-mulcl 10315 ax-mulrcl 10316 ax-mulcom 10317 ax-addass 10318 ax-mulass 10319 ax-distr 10320 ax-i2m1 10321 ax-1ne0 10322 ax-1rid 10323 ax-rnegex 10324 ax-rrecex 10325 ax-cnre 10326 ax-pre-lttri 10327 ax-pre-lttrn 10328 ax-pre-ltadd 10329 ax-pre-mulgt0 10330 ax-riotaBAD 35029 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3or 1114 df-3an 1115 df-tru 1662 df-fal 1672 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ne 3001 df-nel 3104 df-ral 3123 df-rex 3124 df-reu 3125 df-rmo 3126 df-rab 3127 df-v 3417 df-sbc 3664 df-csb 3759 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-pss 3815 df-nul 4146 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-tp 4403 df-op 4405 df-uni 4660 df-int 4699 df-iun 4743 df-iin 4744 df-br 4875 df-opab 4937 df-mpt 4954 df-tr 4977 df-id 5251 df-eprel 5256 df-po 5264 df-so 5265 df-fr 5302 df-we 5304 df-xp 5349 df-rel 5350 df-cnv 5351 df-co 5352 df-dm 5353 df-rn 5354 df-res 5355 df-ima 5356 df-pred 5921 df-ord 5967 df-on 5968 df-lim 5969 df-suc 5970 df-iota 6087 df-fun 6126 df-fn 6127 df-f 6128 df-f1 6129 df-fo 6130 df-f1o 6131 df-fv 6132 df-riota 6867 df-ov 6909 df-oprab 6910 df-mpt2 6911 df-om 7328 df-1st 7429 df-2nd 7430 df-tpos 7618 df-undef 7665 df-wrecs 7673 df-recs 7735 df-rdg 7773 df-1o 7827 df-oadd 7831 df-er 8010 df-map 8125 df-en 8224 df-dom 8225 df-sdom 8226 df-fin 8227 df-pnf 10394 df-mnf 10395 df-xr 10396 df-ltxr 10397 df-le 10398 df-sub 10588 df-neg 10589 df-nn 11352 df-2 11415 df-3 11416 df-4 11417 df-5 11418 df-6 11419 df-n0 11620 df-z 11706 df-uz 11970 df-fz 12621 df-struct 16225 df-ndx 16226 df-slot 16227 df-base 16229 df-sets 16230 df-ress 16231 df-plusg 16319 df-mulr 16320 df-sca 16322 df-vsca 16323 df-0g 16456 df-proset 17282 df-poset 17300 df-plt 17312 df-lub 17328 df-glb 17329 df-join 17330 df-meet 17331 df-p0 17393 df-p1 17394 df-lat 17400 df-clat 17462 df-mgm 17596 df-sgrp 17638 df-mnd 17649 df-submnd 17690 df-grp 17780 df-minusg 17781 df-sbg 17782 df-subg 17943 df-cntz 18101 df-lsm 18403 df-cmn 18549 df-abl 18550 df-mgp 18845 df-ur 18857 df-ring 18904 df-oppr 18978 df-dvdsr 18996 df-unit 18997 df-invr 19027 df-dvr 19038 df-drng 19106 df-lmod 19222 df-lss 19290 df-lsp 19332 df-lvec 19463 df-oposet 35252 df-ol 35254 df-oml 35255 df-covers 35342 df-ats 35343 df-atl 35374 df-cvlat 35398 df-hlat 35427 df-llines 35574 df-lplanes 35575 df-lvols 35576 df-lines 35577 df-psubsp 35579 df-pmap 35580 df-padd 35872 df-lhyp 36064 df-laut 36065 df-ldil 36180 df-ltrn 36181 df-trl 36235 df-tendo 36831 df-edring 36833 df-disoa 37105 df-dvech 37155 df-dib 37215 df-dic 37249 df-dih 37305 df-doch 37424 |
This theorem is referenced by: dochsscl 37444 dochoccl 37445 dochord 37446 dochord2N 37447 dochord3 37448 dochn0nv 37451 dihoml4 37453 dochocsp 37455 dochocsn 37457 dochsat 37459 dochdmj1 37466 dochnoncon 37467 dochdmm1 37486 djhexmid 37487 djhlsmcl 37490 dochsatshpb 37528 dochsnkr2cl 37550 dochpolN 37566 lcfl7lem 37575 lcfl6 37576 lcfl8 37578 lcfl9a 37581 lclkrlem2e 37587 lclkrlem2j 37592 lclkrlem2s 37601 lcfrlem14 37632 lcfrlem23 37641 mapdordlem2 37713 |
Copyright terms: Public domain | W3C validator |