# Metamath Proof Explorer

## Theorem dochvalr2

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

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

### Proof

Step Hyp Ref Expression
1 dochvalr2.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dochvalr2.o
3 dochvalr2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 dochvalr2.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
5 dochvalr2.n ${⊢}{N}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
6 1 3 4 dihcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\to {I}\left({X}\right)\in \mathrm{ran}{I}$
7 2 3 4 5 dochvalr
8 6 7 syldan
9 1 3 4 dihcnvid1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\to {{I}}^{-1}\left({I}\left({X}\right)\right)={X}$
10 9 fveq2d
11 10 fveq2d
12 8 11 eqtrd