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 ⊢ Base K = Base K
10 9 1 2 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ Base K
11 9 4 opoccl ⊢ K ∈ OP ∧ I -1 ⁡ X ∈ Base K → oc ⁡ K ⁡ I -1 ⁡ X ∈ Base K
12 8 10 11 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → oc ⁡ K ⁡ I -1 ⁡ X ∈ Base K
13 9 1 2 dihcl ⊢ K ∈ HL ∧ W ∈ H ∧ oc ⁡ K ⁡ I -1 ⁡ X ∈ Base K → 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 ∈ Base K → 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 ∈ Base K → 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