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

Metamath Proof Explorer

Theorem iscss

Description: The predicate "is a closed subspace" (of a pre-Hilbert space). (Contributed by NM, 7-Oct-2011) (Revised by Mario Carneiro, 13-Oct-2015)

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

Proof

Step	Hyp	Ref	Expression
1		cssval.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
2		cssval.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
3	1 2	cssval	⊢ ( 𝑊 ∈ 𝑋 → 𝐶 = { 𝑠 ∣ 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) } )
4	3	eleq2d	⊢ ( 𝑊 ∈ 𝑋 → ( 𝑆 ∈ 𝐶 ↔ 𝑆 ∈ { 𝑠 ∣ 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) } ) )
5		id	⊢ ( 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )
6		fvex	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ∈ V
7	5 6	eqeltrdi	⊢ ( 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) → 𝑆 ∈ V )
8		id	⊢ ( 𝑠 = 𝑆 → 𝑠 = 𝑆 )
9		2fveq3	⊢ ( 𝑠 = 𝑆 → ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )
10	8 9	eqeq12d	⊢ ( 𝑠 = 𝑆 → ( 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) ↔ 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) )
11	7 10	elab3	⊢ ( 𝑆 ∈ { 𝑠 ∣ 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) } ↔ 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) )
12	4 11	bitrdi	⊢ ( 𝑊 ∈ 𝑋 → ( 𝑆 ∈ 𝐶 ↔ 𝑆 = ( ⊥ ‘ ( ⊥ ‘ 𝑆 ) ) ) )