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

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝑊 ∈ V → 𝐶 = { 𝑠 ∣ 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) } )
24 3 23 syl ⊢ ( 𝑊 ∈ 𝑋 → 𝐶 = { 𝑠 ∣ 𝑠 = ( ⊥ ‘ ( ⊥ ‘ 𝑠 ) ) } )