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

Definition df-pj 16603
 Description: Define orthogonal projection onto a subspace. This is just a wrapping of df-pj1 14948, 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
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-pj
StepHypRef Expression
1 cpj 16600 . 2
2 vh . . 3
3 cvv 2788 . . 3
4 vx . . . . 5
52cv 1622 . . . . . 6
6 clss 15689 . . . . . 6
75, 6cfv 5255 . . . . 5
84cv 1622 . . . . . 6
9 cocv 16560 . . . . . . . 8
105, 9cfv 5255 . . . . . . 7
118, 10cfv 5255 . . . . . 6
12 cpj1 14946 . . . . . . 7
135, 12cfv 5255 . . . . . 6
148, 11, 13co 5858 . . . . 5
154, 7, 14cmpt 4077 . . . 4
16 cbs 13148 . . . . . . 7
175, 16cfv 5255 . . . . . 6
18 cmap 6772 . . . . . 6
1917, 17, 18co 5858 . . . . 5
203, 19cxp 4687 . . . 4
2115, 20cin 3151 . . 3
222, 3, 21cmpt 4077 . 2
231, 22wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  pjfval  16606
 Copyright terms: Public domain W3C validator