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

Definition df-pj 16922
 Description: Define orthogonal projection onto a subspace. This is just a wrapping of df-pj1 15263, 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 16919 . 2
2 vh . . 3
3 cvv 2948 . . 3
4 vx . . . . 5
52cv 1651 . . . . . 6
6 clss 16000 . . . . . 6
75, 6cfv 5446 . . . . 5
84cv 1651 . . . . . 6
9 cocv 16879 . . . . . . . 8
105, 9cfv 5446 . . . . . . 7
118, 10cfv 5446 . . . . . 6
12 cpj1 15261 . . . . . . 7
135, 12cfv 5446 . . . . . 6
148, 11, 13co 6073 . . . . 5
154, 7, 14cmpt 4258 . . . 4
16 cbs 13461 . . . . . . 7
175, 16cfv 5446 . . . . . 6
18 cmap 7010 . . . . . 6
1917, 17, 18co 6073 . . . . 5
203, 19cxp 4868 . . . 4
2115, 20cin 3311 . . 3
222, 3, 21cmpt 4258 . 2
231, 22wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  pjfval  16925
 Copyright terms: Public domain W3C validator