# Metamath Proof Explorer

## Theorem dochocss

Description: Double negative law for orthocomplement of an arbitrary set of vectors. (Contributed by NM, 16-Apr-2014)

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

### Proof

Step Hyp Ref Expression
1 dochss.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dochss.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 dochss.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
4 dochss.o
5 ssintub ${⊢}{X}\subseteq \bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}$
6 eqid ${⊢}\mathrm{DIsoH}\left({K}\right)\left({W}\right)=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
7 1 6 2 3 4 dochcl
8 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
9 8 1 6 4 dochvalr
10 7 9 syldan
11 8 1 6 2 3 4 dochval2
12 11 fveq2d
13 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
14 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
15 13 1 6 2 14 dihf11 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{DIsoH}\left({K}\right)\left({W}\right):{\mathrm{Base}}_{{K}}\underset{1-1}{⟶}\mathrm{LSubSp}\left({U}\right)$
16 15 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \mathrm{DIsoH}\left({K}\right)\left({W}\right):{\mathrm{Base}}_{{K}}\underset{1-1}{⟶}\mathrm{LSubSp}\left({U}\right)$
17 f1f1orn ${⊢}\mathrm{DIsoH}\left({K}\right)\left({W}\right):{\mathrm{Base}}_{{K}}\underset{1-1}{⟶}\mathrm{LSubSp}\left({U}\right)\to \mathrm{DIsoH}\left({K}\right)\left({W}\right):{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}\mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
18 16 17 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \mathrm{DIsoH}\left({K}\right)\left({W}\right):{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}\mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
19 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
20 19 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to {K}\in \mathrm{OP}$
21 simpl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
22 ssrab2 ${⊢}\left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\subseteq \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
23 22 a1i ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\subseteq \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
24 eqid ${⊢}\mathrm{1.}\left({K}\right)=\mathrm{1.}\left({K}\right)$
25 24 1 6 2 3 dih1 ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{DIsoH}\left({K}\right)\left({W}\right)\left(\mathrm{1.}\left({K}\right)\right)={V}$
26 25 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \mathrm{DIsoH}\left({K}\right)\left({W}\right)\left(\mathrm{1.}\left({K}\right)\right)={V}$
27 f1fn ${⊢}\mathrm{DIsoH}\left({K}\right)\left({W}\right):{\mathrm{Base}}_{{K}}\underset{1-1}{⟶}\mathrm{LSubSp}\left({U}\right)\to \mathrm{DIsoH}\left({K}\right)\left({W}\right)Fn{\mathrm{Base}}_{{K}}$
28 16 27 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \mathrm{DIsoH}\left({K}\right)\left({W}\right)Fn{\mathrm{Base}}_{{K}}$
29 13 24 op1cl ${⊢}{K}\in \mathrm{OP}\to \mathrm{1.}\left({K}\right)\in {\mathrm{Base}}_{{K}}$
30 20 29 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \mathrm{1.}\left({K}\right)\in {\mathrm{Base}}_{{K}}$
31 fnfvelrn ${⊢}\left(\mathrm{DIsoH}\left({K}\right)\left({W}\right)Fn{\mathrm{Base}}_{{K}}\wedge \mathrm{1.}\left({K}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{DIsoH}\left({K}\right)\left({W}\right)\left(\mathrm{1.}\left({K}\right)\right)\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
32 28 30 31 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \mathrm{DIsoH}\left({K}\right)\left({W}\right)\left(\mathrm{1.}\left({K}\right)\right)\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
33 26 32 eqeltrrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to {V}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
34 simpr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to {X}\subseteq {V}$
35 sseq2 ${⊢}{z}={V}\to \left({X}\subseteq {z}↔{X}\subseteq {V}\right)$
36 35 elrab ${⊢}{V}\in \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}↔\left({V}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)\wedge {X}\subseteq {V}\right)$
37 33 34 36 sylanbrc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to {V}\in \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}$
38 37 ne0d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\ne \varnothing$
39 1 6 dihintcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left(\left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\subseteq \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)\wedge \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\ne \varnothing \right)\right)\to \bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
40 21 23 38 39 syl12anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
41 f1ocnvdm ${⊢}\left(\mathrm{DIsoH}\left({K}\right)\left({W}\right):{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}\mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)\wedge \bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)\right)\to {\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\in {\mathrm{Base}}_{{K}}$
42 18 40 41 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to {\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\in {\mathrm{Base}}_{{K}}$
43 13 8 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left({\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\right)\in {\mathrm{Base}}_{{K}}$
44 20 42 43 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{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\right)\in {\mathrm{Base}}_{{K}}$
45 f1ocnvfv1 ${⊢}\left(\mathrm{DIsoH}\left({K}\right)\left({W}\right):{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}\mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)\wedge \mathrm{oc}\left({K}\right)\left({\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\right)\in {\mathrm{Base}}_{{K}}\right)\to {\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\mathrm{DIsoH}\left({K}\right)\left({W}\right)\left(\mathrm{oc}\left({K}\right)\left({\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\right)\right)\right)=\mathrm{oc}\left({K}\right)\left({\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\right)$
46 18 44 45 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to {\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\mathrm{DIsoH}\left({K}\right)\left({W}\right)\left(\mathrm{oc}\left({K}\right)\left({\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\right)\right)\right)=\mathrm{oc}\left({K}\right)\left({\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\right)$
47 12 46 eqtrd
48 47 fveq2d
49 13 8 opococ ${⊢}\left({K}\in \mathrm{OP}\wedge {\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\right)\right)={\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)$
50 20 42 49 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{oc}\left({K}\right)\left({\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\right)\right)={\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)$
51 48 50 eqtrd
52 51 fveq2d
53 f1ocnvfv2 ${⊢}\left(\mathrm{DIsoH}\left({K}\right)\left({W}\right):{\mathrm{Base}}_{{K}}\underset{1-1 onto}{⟶}\mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)\wedge \bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)\right)\to \mathrm{DIsoH}\left({K}\right)\left({W}\right)\left({\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\right)=\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}$
54 18 40 53 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\subseteq {V}\right)\to \mathrm{DIsoH}\left({K}\right)\left({W}\right)\left({\mathrm{DIsoH}\left({K}\right)\left({W}\right)}^{-1}\left(\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}\right)\right)=\bigcap \left\{{z}\in \mathrm{ran}\mathrm{DIsoH}\left({K}\right)\left({W}\right)|{X}\subseteq {z}\right\}$
55 10 52 54 3eqtrrd
56 5 55 sseqtrid