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

Definition df-pj 19772
Description: Define orthogonal projection onto a subspace. This is just a wrapping of df-pj1 17786, but we restrict the domain of this function to only total projection functions. (Contributed by Mario Carneiro, 16-Oct-2015.)
Assertion
Ref Expression
df-pj proj = ( ∈ V ↦ ((𝑥 ∈ (LSubSp‘) ↦ (𝑥(proj1)((ocv‘)‘𝑥))) ∩ (V × ((Base‘) ↑𝑚 (Base‘)))))
Distinct variable group:   𝑥,

Detailed syntax breakdown of Definition df-pj
StepHypRef Expression
1 cpj 19769 . 2 class proj
2 vh . . 3 setvar
3 cvv 3077 . . 3 class V
4 vx . . . . 5 setvar 𝑥
52cv 1473 . . . . . 6 class
6 clss 18660 . . . . . 6 class LSubSp
75, 6cfv 5694 . . . . 5 class (LSubSp‘)
84cv 1473 . . . . . 6 class 𝑥
9 cocv 19729 . . . . . . . 8 class ocv
105, 9cfv 5694 . . . . . . 7 class (ocv‘)
118, 10cfv 5694 . . . . . 6 class ((ocv‘)‘𝑥)
12 cpj1 17784 . . . . . . 7 class proj1
135, 12cfv 5694 . . . . . 6 class (proj1)
148, 11, 13co 6431 . . . . 5 class (𝑥(proj1)((ocv‘)‘𝑥))
154, 7, 14cmpt 4541 . . . 4 class (𝑥 ∈ (LSubSp‘) ↦ (𝑥(proj1)((ocv‘)‘𝑥)))
16 cbs 15582 . . . . . . 7 class Base
175, 16cfv 5694 . . . . . 6 class (Base‘)
18 cmap 7624 . . . . . 6 class 𝑚
1917, 17, 18co 6431 . . . . 5 class ((Base‘) ↑𝑚 (Base‘))
203, 19cxp 4930 . . . 4 class (V × ((Base‘) ↑𝑚 (Base‘)))
2115, 20cin 3443 . . 3 class ((𝑥 ∈ (LSubSp‘) ↦ (𝑥(proj1)((ocv‘)‘𝑥))) ∩ (V × ((Base‘) ↑𝑚 (Base‘))))
222, 3, 21cmpt 4541 . 2 class ( ∈ V ↦ ((𝑥 ∈ (LSubSp‘) ↦ (𝑥(proj1)((ocv‘)‘𝑥))) ∩ (V × ((Base‘) ↑𝑚 (Base‘)))))
231, 22wceq 1474 1 wff proj = ( ∈ V ↦ ((𝑥 ∈ (LSubSp‘) ↦ (𝑥(proj1)((ocv‘)‘𝑥))) ∩ (V × ((Base‘) ↑𝑚 (Base‘)))))
Colors of variables: wff setvar class
This definition is referenced by:  pjfval  19775
  Copyright terms: Public domain W3C validator