Metamath Proof Explorer


Definition df-ocv

Description: Define the orthocomplement function in a given set (which usually is a pre-Hilbert space): it associates with a subset its orthogonal subset (which in the case of a closed linear subspace is its orthocomplement). (Contributed by NM, 7-Oct-2011)

Ref Expression
Assertion df-ocv ocv = ( ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ ) ↦ { 𝑥 ∈ ( Base ‘ ) ∣ ∀ 𝑦𝑠 ( 𝑥 ( ·𝑖 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cocv ocv
1 vh
2 cvv V
3 vs 𝑠
4 cbs Base
5 1 cv
6 5 4 cfv ( Base ‘ )
7 6 cpw 𝒫 ( Base ‘ )
8 vx 𝑥
9 vy 𝑦
10 3 cv 𝑠
11 8 cv 𝑥
12 cip ·𝑖
13 5 12 cfv ( ·𝑖 )
14 9 cv 𝑦
15 11 14 13 co ( 𝑥 ( ·𝑖 ) 𝑦 )
16 c0g 0g
17 csca Scalar
18 5 17 cfv ( Scalar ‘ )
19 18 16 cfv ( 0g ‘ ( Scalar ‘ ) )
20 15 19 wceq ( 𝑥 ( ·𝑖 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ ) )
21 20 9 10 wral 𝑦𝑠 ( 𝑥 ( ·𝑖 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ ) )
22 21 8 6 crab { 𝑥 ∈ ( Base ‘ ) ∣ ∀ 𝑦𝑠 ( 𝑥 ( ·𝑖 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ ) ) }
23 3 7 22 cmpt ( 𝑠 ∈ 𝒫 ( Base ‘ ) ↦ { 𝑥 ∈ ( Base ‘ ) ∣ ∀ 𝑦𝑠 ( 𝑥 ( ·𝑖 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ ) ) } )
24 1 2 23 cmpt ( ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ ) ↦ { 𝑥 ∈ ( Base ‘ ) ∣ ∀ 𝑦𝑠 ( 𝑥 ( ·𝑖 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ ) ) } ) )
25 0 24 wceq ocv = ( ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ ) ↦ { 𝑥 ∈ ( Base ‘ ) ∣ ∀ 𝑦𝑠 ( 𝑥 ( ·𝑖 ) 𝑦 ) = ( 0g ‘ ( Scalar ‘ ) ) } ) )