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 19947
Description: Define orthocomplement of a subspace. (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 19944 . 2 class ocv
2 vh . . 3 setvar
3 cvv 3190 . . 3 class V
4 vs . . . 4 setvar 𝑠
52cv 1479 . . . . . 6 class
6 cbs 15800 . . . . . 6 class Base
75, 6cfv 5857 . . . . 5 class (Base‘)
87cpw 4136 . . . 4 class 𝒫 (Base‘)
9 vx . . . . . . . . 9 setvar 𝑥
109cv 1479 . . . . . . . 8 class 𝑥
11 vy . . . . . . . . 9 setvar 𝑦
1211cv 1479 . . . . . . . 8 class 𝑦
13 cip 15886 . . . . . . . . 9 class ·𝑖
145, 13cfv 5857 . . . . . . . 8 class (·𝑖)
1510, 12, 14co 6615 . . . . . . 7 class (𝑥(·𝑖)𝑦)
16 csca 15884 . . . . . . . . 9 class Scalar
175, 16cfv 5857 . . . . . . . 8 class (Scalar‘)
18 c0g 16040 . . . . . . . 8 class 0g
1917, 18cfv 5857 . . . . . . 7 class (0g‘(Scalar‘))
2015, 19wceq 1480 . . . . . 6 wff (𝑥(·𝑖)𝑦) = (0g‘(Scalar‘))
214cv 1479 . . . . . 6 class 𝑠
2220, 11, 21wral 2908 . . . . 5 wff 𝑦𝑠 (𝑥(·𝑖)𝑦) = (0g‘(Scalar‘))
2322, 9, 7crab 2912 . . . 4 class {𝑥 ∈ (Base‘) ∣ ∀𝑦𝑠 (𝑥(·𝑖)𝑦) = (0g‘(Scalar‘))}
244, 8, 23cmpt 4683 . . 3 class (𝑠 ∈ 𝒫 (Base‘) ↦ {𝑥 ∈ (Base‘) ∣ ∀𝑦𝑠 (𝑥(·𝑖)𝑦) = (0g‘(Scalar‘))})
252, 3, 24cmpt 4683 . 2 class ( ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘) ↦ {𝑥 ∈ (Base‘) ∣ ∀𝑦𝑠 (𝑥(·𝑖)𝑦) = (0g‘(Scalar‘))}))
261, 25wceq 1480 1 wff ocv = ( ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘) ↦ {𝑥 ∈ (Base‘) ∣ ∀𝑦𝑠 (𝑥(·𝑖)𝑦) = (0g‘(Scalar‘))}))
Colors of variables: wff setvar class
This definition is referenced by:  ocvfval  19950
  Copyright terms: Public domain W3C validator