Metamath Proof Explorer

Theorem dochoccl

Description: A set of vectors is closed iff it equals its double orthocomplent. (Contributed by NM, 1-Jan-2015)

Ref Expression
Hypotheses dochoccl.h ⊢H=LHyp⁡K
dochoccl.i ⊢I=DIsoH⁡K⁡W
dochoccl.u ⊢U=DVecH⁡K⁡W
dochoccl.v ⊢V=BaseU
dochoccl.o ⊢⊥˙=ocH⁡K⁡W
dochoccl.k ⊢φ→K∈HL∧W∈H
dochoccl.g ⊢φ→X⊆V
Assertion dochoccl ⊢φ→X∈ran⁡I↔⊥˙⁡⊥˙⁡X=X

Proof

Step Hyp Ref Expression
1 dochoccl.h ⊢H=LHyp⁡K
2 dochoccl.i ⊢I=DIsoH⁡K⁡W
3 dochoccl.u ⊢U=DVecH⁡K⁡W
4 dochoccl.v ⊢V=BaseU
5 dochoccl.o ⊢⊥˙=ocH⁡K⁡W
6 dochoccl.k ⊢φ→K∈HL∧W∈H
7 dochoccl.g ⊢φ→X⊆V
8 1 2 5 dochoc ⊢K∈HL∧W∈H∧X∈ran⁡I→⊥˙⁡⊥˙⁡X=X
9 6 8 sylan ⊢φ∧X∈ran⁡I→⊥˙⁡⊥˙⁡X=X
10 simpr ⊢φ∧⊥˙⁡⊥˙⁡X=X→⊥˙⁡⊥˙⁡X=X
11 1 3 4 5 dochssv ⊢K∈HL∧W∈H∧X⊆V→⊥˙⁡X⊆V
12 6 7 11 syl2anc ⊢φ→⊥˙⁡X⊆V
13 1 2 3 4 5 dochcl ⊢K∈HL∧W∈H∧⊥˙⁡X⊆V→⊥˙⁡⊥˙⁡X∈ran⁡I
14 6 12 13 syl2anc ⊢φ→⊥˙⁡⊥˙⁡X∈ran⁡I
15 14 adantr ⊢φ∧⊥˙⁡⊥˙⁡X=X→⊥˙⁡⊥˙⁡X∈ran⁡I
16 10 15 eqeltrrd ⊢φ∧⊥˙⁡⊥˙⁡X=X→X∈ran⁡I
17 9 16 impbida ⊢φ→X∈ran⁡I↔⊥˙⁡⊥˙⁡X=X