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

Metamath Proof Explorer

Theorem ocvcss

Description: The orthocomplement of any set is a closed subspace. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses cssss.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
cssss.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
ocvcss.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
Assertion ocvcss ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 cssss.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 cssss.c ⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
3 ocvcss.o ⊢ ⊥ = ( ocv ‘ 𝑊 )
4 1 3 ocvocv ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )
5 3 ocv2ss ⊢ ( 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) ⊆ ( ⊥ ‘ 𝑆 ) )
6 4 5 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) ⊆ ( ⊥ ‘ 𝑆 ) )
7 1 3 ocvss ⊢ ( ⊥ ‘ 𝑆 ) ⊆ 𝑉
8 7 a1i ⊢ ( 𝑆 ⊆ 𝑉 → ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 )
9 1 2 3 iscss2 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( ⊥ ‘ 𝑆 ) ⊆ 𝑉 ) → ( ( ⊥ ‘ 𝑆 ) ∈ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) ⊆ ( ⊥ ‘ 𝑆 ) ) )
10 8 9 sylan2 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ( ⊥ ‘ 𝑆 ) ∈ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) ⊆ ( ⊥ ‘ 𝑆 ) ) )
11 6 10 mpbird ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐶 )