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 ∧ 𝑆 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐶 )