MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ocv Structured version   Visualization version   GIF version

Definition df-ocv 21090
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
StepHypRef Expression
1 cocv 21087 . 2 class ocv
2 vh . . 3 setvar β„Ž
3 cvv 3447 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1541 . . . . . 6 class β„Ž
6 cbs 17091 . . . . . 6 class Base
75, 6cfv 6500 . . . . 5 class (Baseβ€˜β„Ž)
87cpw 4564 . . . 4 class 𝒫 (Baseβ€˜β„Ž)
9 vx . . . . . . . . 9 setvar π‘₯
109cv 1541 . . . . . . . 8 class π‘₯
11 vy . . . . . . . . 9 setvar 𝑦
1211cv 1541 . . . . . . . 8 class 𝑦
13 cip 17146 . . . . . . . . 9 class ·𝑖
145, 13cfv 6500 . . . . . . . 8 class (Β·π‘–β€˜β„Ž)
1510, 12, 14co 7361 . . . . . . 7 class (π‘₯(Β·π‘–β€˜β„Ž)𝑦)
16 csca 17144 . . . . . . . . 9 class Scalar
175, 16cfv 6500 . . . . . . . 8 class (Scalarβ€˜β„Ž)
18 c0g 17329 . . . . . . . 8 class 0g
1917, 18cfv 6500 . . . . . . 7 class (0gβ€˜(Scalarβ€˜β„Ž))
2015, 19wceq 1542 . . . . . 6 wff (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = (0gβ€˜(Scalarβ€˜β„Ž))
214cv 1541 . . . . . 6 class 𝑠
2220, 11, 21wral 3061 . . . . 5 wff βˆ€π‘¦ ∈ 𝑠 (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = (0gβ€˜(Scalarβ€˜β„Ž))
2322, 9, 7crab 3406 . . . 4 class {π‘₯ ∈ (Baseβ€˜β„Ž) ∣ βˆ€π‘¦ ∈ 𝑠 (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = (0gβ€˜(Scalarβ€˜β„Ž))}
244, 8, 23cmpt 5192 . . 3 class (𝑠 ∈ 𝒫 (Baseβ€˜β„Ž) ↦ {π‘₯ ∈ (Baseβ€˜β„Ž) ∣ βˆ€π‘¦ ∈ 𝑠 (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = (0gβ€˜(Scalarβ€˜β„Ž))})
252, 3, 24cmpt 5192 . 2 class (β„Ž ∈ V ↦ (𝑠 ∈ 𝒫 (Baseβ€˜β„Ž) ↦ {π‘₯ ∈ (Baseβ€˜β„Ž) ∣ βˆ€π‘¦ ∈ 𝑠 (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = (0gβ€˜(Scalarβ€˜β„Ž))}))
261, 25wceq 1542 1 wff ocv = (β„Ž ∈ V ↦ (𝑠 ∈ 𝒫 (Baseβ€˜β„Ž) ↦ {π‘₯ ∈ (Baseβ€˜β„Ž) ∣ βˆ€π‘¦ ∈ 𝑠 (π‘₯(Β·π‘–β€˜β„Ž)𝑦) = (0gβ€˜(Scalarβ€˜β„Ž))}))
Colors of variables: wff setvar class
This definition is referenced by:  ocvfval  21093
  Copyright terms: Public domain W3C validator