Theorem cssval

Description: The set of closed subspaces 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	cssval	⊢ ( 𝑊 ∈ 𝑋 → 𝐶 = { 𝑠 ∣ 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		cssval.o	⊢ ⊥ = ( ocv ‘ 𝑊 )
2		cssval.c	⊢ 𝐶 = ( ClSubSp ‘ 𝑊 )
3		elex	⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
4		fveq2	⊢ ( 𝑤 = 𝑊 → ( ocv ‘ 𝑤 ) = ( ocv ‘ 𝑊 ) )
5	4 1	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( ocv ‘ 𝑤 ) = ⊥ )
6	5	fveq1d	⊢ ( 𝑤 = 𝑊 → ( ( ocv ‘ 𝑤 ) ‘ 𝑠 ) = ( ⊥ ‘ 𝑠 ) )
7	5 6	fveq12d	⊢ ( 𝑤 = 𝑊 → ( ( ocv ‘ 𝑤 ) ‘ ( ( ocv ‘ 𝑤 ) ‘ 𝑠 ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) )
8	7	eqeq2d	⊢ ( 𝑤 = 𝑊 → ( 𝑠 = ( ( ocv ‘ 𝑤 ) ‘ ( ( ocv ‘ 𝑤 ) ‘ 𝑠 ) ) ↔ 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) ) )
9	8	abbidv	⊢ ( 𝑤 = 𝑊 → { 𝑠 ∣ 𝑠 = ( ( ocv ‘ 𝑤 ) ‘ ( ( ocv ‘ 𝑤 ) ‘ 𝑠 ) ) } = { 𝑠 ∣ 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) } )
10		df-css	⊢ ClSubSp = ( 𝑤 ∈ V ↦ { 𝑠 ∣ 𝑠 = ( ( ocv ‘ 𝑤 ) ‘ ( ( ocv ‘ 𝑤 ) ‘ 𝑠 ) ) } )
11		fvex	⊢ ( Base ‘ 𝑊 ) ∈ V
12	11	pwex	⊢ 𝒫 ( Base ‘ 𝑊 ) ∈ V
13		id	⊢ ( 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) → 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) )
14		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
15	14 1	ocvss	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) ⊆ ( Base ‘ 𝑊 )
16		fvex	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) ∈ V
17	16	elpw	⊢ ( ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) ∈ 𝒫 ( Base ‘ 𝑊 ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) ⊆ ( Base ‘ 𝑊 ) )
18	15 17	mpbir	⊢ ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) ∈ 𝒫 ( Base ‘ 𝑊 )
19	13 18	eqeltrdi	⊢ ( 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) → 𝑠 ∈ 𝒫 ( Base ‘ 𝑊 ) )
20	19	abssi	⊢ { 𝑠 ∣ 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) } ⊆ 𝒫 ( Base ‘ 𝑊 )
21	12 20	ssexi	⊢ { 𝑠 ∣ 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) } ∈ V
22	9 10 21	fvmpt	⊢ ( 𝑊 ∈ V → ( ClSubSp ‘ 𝑊 ) = { 𝑠 ∣ 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) } )
23	2 22	syl5eq	⊢ ( 𝑊 ∈ V → 𝐶 = { 𝑠 ∣ 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) } )
24	3 23	syl	⊢ ( 𝑊 ∈ 𝑋 → 𝐶 = { 𝑠 ∣ 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) } )