# Metamath Proof Explorer

## Theorem dochoc

Description: Double negative law for orthocomplement of a closed subspace. (Contributed by NM, 14-Mar-2014)

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

### Proof

Step Hyp Ref Expression
1 dochoc.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 dochoc.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
3 dochoc.o
4 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
5 4 1 2 3 dochvalr
6 5 fveq2d
7 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
8 7 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {K}\in \mathrm{OP}$
9 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
10 9 1 2 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}}$
11 9 4 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {{I}}^{-1}\left({X}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\in {\mathrm{Base}}_{{K}}$
12 8 10 11 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to \mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\in {\mathrm{Base}}_{{K}}$
13 9 1 2 dihcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\in {\mathrm{Base}}_{{K}}\right)\to {I}\left(\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\right)\in \mathrm{ran}{I}$
14 12 13 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {I}\left(\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\right)\in \mathrm{ran}{I}$
15 4 1 2 3 dochvalr
16 14 15 syldan
17 9 1 2 dihcnvid1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\in {\mathrm{Base}}_{{K}}\right)\to {{I}}^{-1}\left({I}\left(\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\right)\right)=\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)$
18 12 17 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {{I}}^{-1}\left({I}\left(\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\right)\right)=\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)$
19 18 fveq2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to \mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({I}\left(\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\right)\right)\right)=\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\right)$
20 9 4 opococ ${⊢}\left({K}\in \mathrm{OP}\wedge {{I}}^{-1}\left({X}\right)\in {\mathrm{Base}}_{{K}}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\right)={{I}}^{-1}\left({X}\right)$
21 8 10 20 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to \mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\right)={{I}}^{-1}\left({X}\right)$
22 19 21 eqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to \mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({I}\left(\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\right)\right)\right)={{I}}^{-1}\left({X}\right)$
23 22 fveq2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {I}\left(\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({I}\left(\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\right)\right)\right)\right)={I}\left({{I}}^{-1}\left({X}\right)\right)$
24 1 2 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}$
25 23 24 eqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in \mathrm{ran}{I}\right)\to {I}\left(\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({I}\left(\mathrm{oc}\left({K}\right)\left({{I}}^{-1}\left({X}\right)\right)\right)\right)\right)\right)={X}$
26 16 25 eqtrd
27 6 26 eqtrd