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