Theorem cssi

Description: Property of a closed subspace (of a pre-Hilbert space). (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	cssval.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
	cssval.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
Assertion	cssi	⊢ ( 𝑆 ∈ 𝐶 → 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cssval.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
2		cssval.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
3		elfvdm	⊢ ( 𝑆 ∈ ( ClSubSp ‘ 𝑊 ) → 𝑊 ∈ dom ClSubSp )
4	3 2	eleq2s	⊢ ( 𝑆 ∈ 𝐶 → 𝑊 ∈ dom ClSubSp )
5	1 2	iscss	⊢ ( 𝑊 ∈ dom ClSubSp → ( 𝑆 ∈ 𝐶 ↔ 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) )
6	4 5	syl	⊢ ( 𝑆 ∈ 𝐶 → ( 𝑆 ∈ 𝐶 ↔ 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) )
7	6	ibi	⊢ ( 𝑆 ∈ 𝐶 → 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )