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 𝐼 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 ) )