# Metamath Proof Explorer

## Theorem dochvalr

Description: Orthocomplement of a closed subspace. (Contributed by NM, 14-Mar-2014)

Ref Expression
Hypotheses dochvalr.o
dochvalr.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dochvalr.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dochvalr.n ${⊢}{N}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
Assertion dochvalr

### Proof

Step Hyp Ref Expression
1 dochvalr.o
2 dochvalr.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dochvalr.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
4 dochvalr.n ${⊢}{N}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
5 eqid ${⊢}\mathrm{DVecH}\left({K}\right)\left({W}\right)=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
6 eqid ${⊢}{\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}={\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}$
7 2 5 3 6 dihrnss ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {X}\subseteq {\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}$
8 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
9 eqid ${⊢}\mathrm{glb}\left({K}\right)=\mathrm{glb}\left({K}\right)$
10 8 9 1 2 3 5 6 4 dochval
11 7 10 syldan
12 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
13 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
14 13 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {K}\in \mathrm{Lat}$
15 hlclat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{CLat}$
16 15 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {K}\in \mathrm{CLat}$
17 ssrab2 ${⊢}\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\subseteq {\mathrm{Base}}_{{K}}$
18 8 9 clatglbcl ${⊢}\left({K}\in \mathrm{CLat}\wedge \left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\subseteq {\mathrm{Base}}_{{K}}\right)\to \mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right)\in {\mathrm{Base}}_{{K}}$
19 16 17 18 sylancl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to \mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right)\in {\mathrm{Base}}_{{K}}$
20 8 2 3 dihcnvcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {{I}}^{-1}\left({X}\right)\in {\mathrm{Base}}_{{K}}$
21 17 a1i ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to \left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\subseteq {\mathrm{Base}}_{{K}}$
22 ssid ${⊢}{X}\subseteq {X}$
23 2 3 dihcnvid2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {I}\left({{I}}^{-1}\left({X}\right)\right)={X}$
24 22 23 sseqtrrid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {X}\subseteq {I}\left({{I}}^{-1}\left({X}\right)\right)$
25 fveq2 ${⊢}{y}={{I}}^{-1}\left({X}\right)\to {I}\left({y}\right)={I}\left({{I}}^{-1}\left({X}\right)\right)$
26 25 sseq2d ${⊢}{y}={{I}}^{-1}\left({X}\right)\to \left({X}\subseteq {I}\left({y}\right)↔{X}\subseteq {I}\left({{I}}^{-1}\left({X}\right)\right)\right)$
27 26 elrab ${⊢}{{I}}^{-1}\left({X}\right)\in \left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}↔\left({{I}}^{-1}\left({X}\right)\in {\mathrm{Base}}_{{K}}\wedge {X}\subseteq {I}\left({{I}}^{-1}\left({X}\right)\right)\right)$
28 20 24 27 sylanbrc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {{I}}^{-1}\left({X}\right)\in \left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}$
29 8 12 9 clatglble ${⊢}\left({K}\in \mathrm{CLat}\wedge \left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\subseteq {\mathrm{Base}}_{{K}}\wedge {{I}}^{-1}\left({X}\right)\in \left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right)\to \mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right){\le }_{{K}}{{I}}^{-1}\left({X}\right)$
30 16 21 28 29 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to \mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right){\le }_{{K}}{{I}}^{-1}\left({X}\right)$
31 fveq2 ${⊢}{y}={z}\to {I}\left({y}\right)={I}\left({z}\right)$
32 31 sseq2d ${⊢}{y}={z}\to \left({X}\subseteq {I}\left({y}\right)↔{X}\subseteq {I}\left({z}\right)\right)$
33 32 elrab ${⊢}{z}\in \left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}↔\left({z}\in {\mathrm{Base}}_{{K}}\wedge {X}\subseteq {I}\left({z}\right)\right)$
34 23 adantr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\wedge {z}\in {\mathrm{Base}}_{{K}}\right)\to {I}\left({{I}}^{-1}\left({X}\right)\right)={X}$
35 34 sseq1d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\wedge {z}\in {\mathrm{Base}}_{{K}}\right)\to \left({I}\left({{I}}^{-1}\left({X}\right)\right)\subseteq {I}\left({z}\right)↔{X}\subseteq {I}\left({z}\right)\right)$
36 simpll ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\wedge {z}\in {\mathrm{Base}}_{{K}}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
37 20 adantr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\wedge {z}\in {\mathrm{Base}}_{{K}}\right)\to {{I}}^{-1}\left({X}\right)\in {\mathrm{Base}}_{{K}}$
38 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\wedge {z}\in {\mathrm{Base}}_{{K}}\right)\to {z}\in {\mathrm{Base}}_{{K}}$
39 8 12 2 3 dihord ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {{I}}^{-1}\left({X}\right)\in {\mathrm{Base}}_{{K}}\wedge {z}\in {\mathrm{Base}}_{{K}}\right)\to \left({I}\left({{I}}^{-1}\left({X}\right)\right)\subseteq {I}\left({z}\right)↔{{I}}^{-1}\left({X}\right){\le }_{{K}}{z}\right)$
40 36 37 38 39 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\wedge {z}\in {\mathrm{Base}}_{{K}}\right)\to \left({I}\left({{I}}^{-1}\left({X}\right)\right)\subseteq {I}\left({z}\right)↔{{I}}^{-1}\left({X}\right){\le }_{{K}}{z}\right)$
41 35 40 bitr3d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\wedge {z}\in {\mathrm{Base}}_{{K}}\right)\to \left({X}\subseteq {I}\left({z}\right)↔{{I}}^{-1}\left({X}\right){\le }_{{K}}{z}\right)$
42 41 biimpd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\wedge {z}\in {\mathrm{Base}}_{{K}}\right)\to \left({X}\subseteq {I}\left({z}\right)\to {{I}}^{-1}\left({X}\right){\le }_{{K}}{z}\right)$
43 42 expimpd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to \left(\left({z}\in {\mathrm{Base}}_{{K}}\wedge {X}\subseteq {I}\left({z}\right)\right)\to {{I}}^{-1}\left({X}\right){\le }_{{K}}{z}\right)$
44 33 43 syl5bi ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to \left({z}\in \left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\to {{I}}^{-1}\left({X}\right){\le }_{{K}}{z}\right)$
45 44 ralrimiv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to \forall {z}\in \left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\phantom{\rule{.4em}{0ex}}{{I}}^{-1}\left({X}\right){\le }_{{K}}{z}$
46 8 12 9 clatleglb ${⊢}\left({K}\in \mathrm{CLat}\wedge {{I}}^{-1}\left({X}\right)\in {\mathrm{Base}}_{{K}}\wedge \left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\subseteq {\mathrm{Base}}_{{K}}\right)\to \left({{I}}^{-1}\left({X}\right){\le }_{{K}}\mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right)↔\forall {z}\in \left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\phantom{\rule{.4em}{0ex}}{{I}}^{-1}\left({X}\right){\le }_{{K}}{z}\right)$
47 16 20 21 46 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to \left({{I}}^{-1}\left({X}\right){\le }_{{K}}\mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right)↔\forall {z}\in \left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\phantom{\rule{.4em}{0ex}}{{I}}^{-1}\left({X}\right){\le }_{{K}}{z}\right)$
48 45 47 mpbird ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {{I}}^{-1}\left({X}\right){\le }_{{K}}\mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right)$
49 8 12 14 19 20 30 48 latasymd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to \mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right)={{I}}^{-1}\left({X}\right)$
50 49 fveq2d
51 50 fveq2d
52 11 51 eqtrd