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

Definition df-pj 19258
 Description: Define orthogonal projection onto a subspace. This is just a wrapping of df-pj1 17282, 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 19255 . 2
2 vh . . 3
3 cvv 3082 . . 3
4 vx . . . . 5
52cv 1437 . . . . . 6
6 clss 18148 . . . . . 6
75, 6cfv 5599 . . . . 5
84cv 1437 . . . . . 6
9 cocv 19215 . . . . . . . 8
105, 9cfv 5599 . . . . . . 7
118, 10cfv 5599 . . . . . 6
12 cpj1 17280 . . . . . . 7
135, 12cfv 5599 . . . . . 6
148, 11, 13co 6303 . . . . 5
154, 7, 14cmpt 4480 . . . 4
16 cbs 15114 . . . . . . 7
175, 16cfv 5599 . . . . . 6
18 cmap 7478 . . . . . 6
1917, 17, 18co 6303 . . . . 5
203, 19cxp 4849 . . . 4
2115, 20cin 3436 . . 3
222, 3, 21cmpt 4480 . 2
231, 22wceq 1438 1
 Colors of variables: wff setvar class This definition is referenced by:  pjfval  19261
 Copyright terms: Public domain W3C validator