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

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 ‘ ℎ ) ) } ) )