Metamath Proof Explorer

Theorem dochvalr2

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

Ref Expression
Hypotheses dochvalr2.b ⊢B=BaseK
dochvalr2.o ⊢⊥˙=oc⁡K
dochvalr2.h ⊢H=LHyp⁡K
dochvalr2.i ⊢I=DIsoH⁡K⁡W
dochvalr2.n ⊢N=ocH⁡K⁡W
Assertion dochvalr2 ⊢K∈HL∧W∈H∧X∈B→N⁡I⁡X=I⁡⊥˙⁡X

Proof

Step Hyp Ref Expression
1 dochvalr2.b ⊢B=BaseK
2 dochvalr2.o ⊢⊥˙=oc⁡K
3 dochvalr2.h ⊢H=LHyp⁡K
4 dochvalr2.i ⊢I=DIsoH⁡K⁡W
5 dochvalr2.n ⊢N=ocH⁡K⁡W
6 1 3 4 dihcl ⊢K∈HL∧W∈H∧X∈B→I⁡X∈ran⁡I
7 2 3 4 5 dochvalr ⊢K∈HL∧W∈H∧I⁡X∈ran⁡I→N⁡I⁡X=I⁡⊥˙⁡I-1⁡I⁡X
8 6 7 syldan ⊢K∈HL∧W∈H∧X∈B→N⁡I⁡X=I⁡⊥˙⁡I-1⁡I⁡X
9 1 3 4 dihcnvid1 ⊢K∈HL∧W∈H∧X∈B→I-1⁡I⁡X=X
10 9 fveq2d ⊢K∈HL∧W∈H∧X∈B→⊥˙⁡I-1⁡I⁡X=⊥˙⁡X
11 10 fveq2d ⊢K∈HL∧W∈H∧X∈B→I⁡⊥˙⁡I-1⁡I⁡X=I⁡⊥˙⁡X
12 8 11 eqtrd ⊢K∈HL∧W∈H∧X∈B→N⁡I⁡X=I⁡⊥˙⁡X