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=LHyp⁡K
dochoc.i ⊢I=DIsoH⁡K⁡W
dochoc.o ⊢⊥˙=ocH⁡K⁡W
Assertion dochoc ⊢K∈HL∧W∈H∧X∈ran⁡I→⊥˙⁡⊥˙⁡X=X

Proof

Step Hyp Ref Expression
1 dochoc.h ⊢H=LHyp⁡K
2 dochoc.i ⊢I=DIsoH⁡K⁡W
3 dochoc.o ⊢⊥˙=ocH⁡K⁡W
4 eqid ⊢oc⁡K=oc⁡K
5 4 1 2 3 dochvalr ⊢K∈HL∧W∈H∧X∈ran⁡I→⊥˙⁡X=I⁡oc⁡K⁡I-1⁡X
6 5 fveq2d ⊢K∈HL∧W∈H∧X∈ran⁡I→⊥˙⁡⊥˙⁡X=⊥˙⁡I⁡oc⁡K⁡I-1⁡X
7 hlop ⊢K∈HL→K∈OP
8 7 ad2antrr ⊢K∈HL∧W∈H∧X∈ran⁡I→K∈OP
9 eqid ⊢BaseK=BaseK
10 9 1 2 dihcnvcl ⊢K∈HL∧W∈H∧X∈ran⁡I→I-1⁡X∈BaseK
11 9 4 opoccl ⊢K∈OP∧I-1⁡X∈BaseK→oc⁡K⁡I-1⁡X∈BaseK
12 8 10 11 syl2anc ⊢K∈HL∧W∈H∧X∈ran⁡I→oc⁡K⁡I-1⁡X∈BaseK
13 9 1 2 dihcl ⊢K∈HL∧W∈H∧oc⁡K⁡I-1⁡X∈BaseK→I⁡oc⁡K⁡I-1⁡X∈ran⁡I
14 12 13 syldan ⊢K∈HL∧W∈H∧X∈ran⁡I→I⁡oc⁡K⁡I-1⁡X∈ran⁡I
15 4 1 2 3 dochvalr ⊢K∈HL∧W∈H∧I⁡oc⁡K⁡I-1⁡X∈ran⁡I→⊥˙⁡I⁡oc⁡K⁡I-1⁡X=I⁡oc⁡K⁡I-1⁡I⁡oc⁡K⁡I-1⁡X
16 14 15 syldan ⊢K∈HL∧W∈H∧X∈ran⁡I→⊥˙⁡I⁡oc⁡K⁡I-1⁡X=I⁡oc⁡K⁡I-1⁡I⁡oc⁡K⁡I-1⁡X
17 9 1 2 dihcnvid1 ⊢K∈HL∧W∈H∧oc⁡K⁡I-1⁡X∈BaseK→I-1⁡I⁡oc⁡K⁡I-1⁡X=oc⁡K⁡I-1⁡X
18 12 17 syldan ⊢K∈HL∧W∈H∧X∈ran⁡I→I-1⁡I⁡oc⁡K⁡I-1⁡X=oc⁡K⁡I-1⁡X
19 18 fveq2d ⊢K∈HL∧W∈H∧X∈ran⁡I→oc⁡K⁡I-1⁡I⁡oc⁡K⁡I-1⁡X=oc⁡K⁡oc⁡K⁡I-1⁡X
20 9 4 opococ ⊢K∈OP∧I-1⁡X∈BaseK→oc⁡K⁡oc⁡K⁡I-1⁡X=I-1⁡X
21 8 10 20 syl2anc ⊢K∈HL∧W∈H∧X∈ran⁡I→oc⁡K⁡oc⁡K⁡I-1⁡X=I-1⁡X
22 19 21 eqtrd ⊢K∈HL∧W∈H∧X∈ran⁡I→oc⁡K⁡I-1⁡I⁡oc⁡K⁡I-1⁡X=I-1⁡X
23 22 fveq2d ⊢K∈HL∧W∈H∧X∈ran⁡I→I⁡oc⁡K⁡I-1⁡I⁡oc⁡K⁡I-1⁡X=I⁡I-1⁡X
24 1 2 dihcnvid2 ⊢K∈HL∧W∈H∧X∈ran⁡I→I⁡I-1⁡X=X
25 23 24 eqtrd ⊢K∈HL∧W∈H∧X∈ran⁡I→I⁡oc⁡K⁡I-1⁡I⁡oc⁡K⁡I-1⁡X=X
26 16 25 eqtrd ⊢K∈HL∧W∈H∧X∈ran⁡I→⊥˙⁡I⁡oc⁡K⁡I-1⁡X=X
27 6 26 eqtrd ⊢K∈HL∧W∈H∧X∈ran⁡I→⊥˙⁡⊥˙⁡X=X