This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochoccl.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dochoccl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochoccl.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochoccl.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochoccl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochoccl.g ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
Assertion dochoccl ( 𝜑 → ( 𝑋 ∈ ran 𝐼 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 dochoccl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochoccl.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 dochoccl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochoccl.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochoccl.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
6 dochoccl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 dochoccl.g ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
8 1 2 5 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
9 6 8 sylan ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
10 simpr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
11 1 3 4 5 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
12 6 7 11 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
13 1 2 3 4 5 dochcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran 𝐼 )
14 6 12 13 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran 𝐼 )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran 𝐼 )
16 10 15 eqeltrrd ⊢ ( ( 𝜑 ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) → 𝑋 ∈ ran 𝐼 )
17 9 16 impbida ⊢ ( 𝜑 → ( 𝑋 ∈ ran 𝐼 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) )