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=h∈V⟼s∈𝒫Baseh⟼x∈Baseh|∀y∈sx⋅𝑖⁡hy=0Scalar⁡h

Detailed syntax breakdown

Step Hyp Ref Expression
0 cocv classocv
1 vh setvarh
2 cvv classV
3 vs setvars
4 cbs classBase
5 1 cv setvarh
6 5 4 cfv classBaseh
7 6 cpw class𝒫Baseh
8 vx setvarx
9 vy setvary
10 3 cv setvars
11 8 cv setvarx
12 cip class⋅𝑖
13 5 12 cfv class⋅𝑖⁡h
14 9 cv setvary
15 11 14 13 co classx⋅𝑖⁡hy
16 c0g class0𝑔
17 csca classScalar
18 5 17 cfv classScalar⁡h
19 18 16 cfv class0Scalar⁡h
20 15 19 wceq wffx⋅𝑖⁡hy=0Scalar⁡h
21 20 9 10 wral wff∀y∈sx⋅𝑖⁡hy=0Scalar⁡h
22 21 8 6 crab classx∈Baseh|∀y∈sx⋅𝑖⁡hy=0Scalar⁡h
23 3 7 22 cmpt classs∈𝒫Baseh⟼x∈Baseh|∀y∈sx⋅𝑖⁡hy=0Scalar⁡h
24 1 2 23 cmpt classh∈V⟼s∈𝒫Baseh⟼x∈Baseh|∀y∈sx⋅𝑖⁡hy=0Scalar⁡h
25 0 24 wceq wffocv=h∈V⟼s∈𝒫Baseh⟼x∈Baseh|∀y∈sx⋅𝑖⁡hy=0Scalar⁡h