Metamath Proof Explorer

Theorem dochcl

Description: Closure of subspace orthocomplement for DVecH vector space. (Contributed by NM, 9-Mar-2014)

Ref Expression
Hypotheses dochcl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dochcl.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
dochcl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dochcl.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
dochcl.o
Assertion dochcl

Proof

Step Hyp Ref Expression
1 dochcl.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dochcl.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
3 dochcl.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 dochcl.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 dochcl.o
6 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
7 eqid ${⊢}\mathrm{glb}\left({K}\right)=\mathrm{glb}\left({K}\right)$
8 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
9 6 7 8 1 2 3 4 5 dochval
10 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
11 10 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to {K}\in \mathrm{OP}$
12 hlclat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{CLat}$
13 12 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to {K}\in \mathrm{CLat}$
14 ssrab2 ${⊢}\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\subseteq {\mathrm{Base}}_{{K}}$
15 6 7 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}}$
16 13 14 15 sylancl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\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}}$
17 6 8 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge \mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right)\right)\in {\mathrm{Base}}_{{K}}$
18 11 16 17 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right)\right)\in {\mathrm{Base}}_{{K}}$
19 6 1 2 dihcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \mathrm{oc}\left({K}\right)\left(\mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right)\right)\in {\mathrm{Base}}_{{K}}\right)\to {I}\left(\mathrm{oc}\left({K}\right)\left(\mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right)\right)\right)\in \mathrm{ran}{I}$
20 18 19 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to {I}\left(\mathrm{oc}\left({K}\right)\left(\mathrm{glb}\left({K}\right)\left(\left\{{y}\in {\mathrm{Base}}_{{K}}|{X}\subseteq {I}\left({y}\right)\right\}\right)\right)\right)\in \mathrm{ran}{I}$
21 9 20 eqeltrd