Definition df-ocv 21974

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.)

Assertion

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

Distinct variable group:   ℎ,𝑠,𝑥,𝑦

Detailed syntax breakdown of Definition df-ocv

Step	Hyp	Ref	Expression
1		cocv 21971	. 2 class ocv
2		vh	. . 3 setvar ℎ
3		cvv 3450	. . 3 class V
4		vs	. . . 4 setvar 𝑠
5	2	cv 1568	. . . . . 6 class ℎ
6		cbs 17392	. . . . . 6 class Base
7	5, 6	cfv 6538	. . . . 5 class (Base‘ℎ)
8	7	cpw 4556	. . . 4 class 𝒫 (Base‘ℎ)
9		vx	. . . . . . . . 9 setvar 𝑥
10	9	cv 1568	. . . . . . . 8 class 𝑥
11		vy	. . . . . . . . 9 setvar 𝑦
12	11	cv 1568	. . . . . . . 8 class 𝑦
13		cip 17438	. . . . . . . . 9 class ·𝑖
14	5, 13	cfv 6538	. . . . . . . 8 class (·𝑖‘ℎ)
15	10, 12, 14	co 7420	. . . . . . 7 class (𝑥(·𝑖‘ℎ)𝑦)
16		csca 17436	. . . . . . . . 9 class Scalar
17	5, 16	cfv 6538	. . . . . . . 8 class (Scalar‘ℎ)
18		c0g 17615	. . . . . . . 8 class 0g
19	17, 18	cfv 6538	. . . . . . 7 class (0g‘(Scalar‘ℎ))
20	15, 19	wceq 1569	. . . . . 6 wff (𝑥(·𝑖‘ℎ)𝑦) = (0g‘(Scalar‘ℎ))
21	4	cv 1568	. . . . . 6 class 𝑠
22	20, 11, 21	wral 3076	. . . . 5 wff ∀𝑦 ∈ 𝑠 (𝑥(·𝑖‘ℎ)𝑦) = (0g‘(Scalar‘ℎ))
23	22, 9, 7	crab 3412	. . . 4 class {𝑥 ∈ (Base‘ℎ) ∣ ∀𝑦 ∈ 𝑠 (𝑥(·𝑖‘ℎ)𝑦) = (0g‘(Scalar‘ℎ))}
24	4, 8, 23	cmpt 5185	. . 3 class (𝑠 ∈ 𝒫 (Base‘ℎ) ↦ {𝑥 ∈ (Base‘ℎ) ∣ ∀𝑦 ∈ 𝑠 (𝑥(·𝑖‘ℎ)𝑦) = (0g‘(Scalar‘ℎ))})
25	2, 3, 24	cmpt 5185	. 2 class (ℎ ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘ℎ) ↦ {𝑥 ∈ (Base‘ℎ) ∣ ∀𝑦 ∈ 𝑠 (𝑥(·𝑖‘ℎ)𝑦) = (0g‘(Scalar‘ℎ))}))
26	1, 25	wceq 1569	1 wff ocv = (ℎ ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘ℎ) ↦ {𝑥 ∈ (Base‘ℎ) ∣ ∀𝑦 ∈ 𝑠 (𝑥(·𝑖‘ℎ)𝑦) = (0g‘(Scalar‘ℎ))}))

This definition is used by:  ocvfval  21977