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

Metamath Proof Explorer

Theorem iscss2

Description: It is sufficient to prove that the double orthocomplement is a subset of the target set to show that the 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	iscss2	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑆 ∈ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		cssss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		cssss.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
3		ocvcss.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
4	3 2	iscss	⊢ ( 𝑊 ∈ PreHil → ( 𝑆 ∈ 𝐶 ↔ 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) )
5	4	adantr	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑆 ∈ 𝐶 ↔ 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) )
6	1 3	ocvocv	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )
7		eqss	⊢ ( 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ↔ ( 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ∧ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ 𝑆 ) )
8	7	baib	⊢ ( 𝑆 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → ( 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ 𝑆 ) )
9	6 8	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ 𝑆 ) )
10	5 9	bitrd	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑆 ∈ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ⊆ 𝑆 ) )