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 = Base U
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 = Base U
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