Users' Mathboxes Mathbox for Andrew Salmon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ptdf Unicode version

Definition df-ptdf 27681
Description: Define the predicate  PtDf, which is a utility definition used to shorten definitions and simplify proofs. (Contributed by Andrew Salmon, 15-Jul-2012.)
Assertion
Ref Expression
df-ptdf  |-  PtDf ( A ,  B )  =  ( x  e.  RR  |->  ( ( ( x . v ( B - r A ) ) +v A
) " { 1 ,  2 ,  3 } ) )
Distinct variable groups:    x, A    x, B

Detailed syntax breakdown of Definition df-ptdf
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2cptdfc 27665 . 2  class  PtDf ( A ,  B )
4 vx . . 3  set  x
5 cr 8736 . . 3  class  RR
64cv 1622 . . . . . 6  class  x
7 cminusr 27663 . . . . . . 7  class  - r
82, 1, 7co 5858 . . . . . 6  class  ( B - r A )
9 ctimesr 27664 . . . . . 6  class  . v
106, 8, 9co 5858 . . . . 5  class  ( x . v ( B - r A ) )
11 cpv 21141 . . . . 5  class  +v
1210, 1, 11co 5858 . . . 4  class  ( ( x . v ( B - r A ) ) +v A
)
13 c1 8738 . . . . 5  class  1
14 c2 9795 . . . . 5  class  2
15 c3 9796 . . . . 5  class  3
1613, 14, 15ctp 3642 . . . 4  class  { 1 ,  2 ,  3 }
1712, 16cima 4692 . . 3  class  ( ( ( x . v ( B - r A ) ) +v A ) " {
1 ,  2 ,  3 } )
184, 5, 17cmpt 4077 . 2  class  ( x  e.  RR  |->  ( ( ( x . v ( B - r A ) ) +v A ) " {
1 ,  2 ,  3 } ) )
193, 18wceq 1623 1  wff  PtDf ( A ,  B )  =  ( x  e.  RR  |->  ( ( ( x . v ( B - r A ) ) +v A
) " { 1 ,  2 ,  3 } ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator