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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cocv class ocv
1 vh setvar h
2 cvv class V
3 vs setvar s
4 cbs class Base
5 1 cv setvar h
6 5 4 cfv class Base h
7 6 cpw class 𝒫 Base h
8 vx setvar x
9 vy setvar y
10 3 cv setvar s
11 8 cv setvar x
12 cip class ⋅ 𝑖
13 5 12 cfv class ⋅ 𝑖 ⁡ h
14 9 cv setvar y
15 11 14 13 co class x ⋅ 𝑖 ⁡ h y
16 c0g class 0 𝑔
17 csca class Scalar
18 5 17 cfv class Scalar ⁡ h
19 18 16 cfv class 0 Scalar ⁡ h
20 15 19 wceq wff x ⋅ 𝑖 ⁡ h y = 0 Scalar ⁡ h
21 20 9 10 wral wff ∀ y ∈ s x ⋅ 𝑖 ⁡ h y = 0 Scalar ⁡ h
22 21 8 6 crab class x ∈ Base h | ∀ y ∈ s x ⋅ 𝑖 ⁡ h y = 0 Scalar ⁡ h
23 3 7 22 cmpt class s ∈ 𝒫 Base h ⟼ x ∈ Base h | ∀ y ∈ s x ⋅ 𝑖 ⁡ h y = 0 Scalar ⁡ h
24 1 2 23 cmpt class h ∈ V ⟼ s ∈ 𝒫 Base h ⟼ x ∈ Base h | ∀ y ∈ s x ⋅ 𝑖 ⁡ h y = 0 Scalar ⁡ h
25 0 24 wceq wff ocv = h ∈ V ⟼ s ∈ 𝒫 Base h ⟼ x ∈ Base h | ∀ y ∈ s x ⋅ 𝑖 ⁡ h y = 0 Scalar ⁡ h