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

Definition df-ptdf 27784
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 27768 . 2  class  PtDf ( A ,  B )
4 vx . . 3  set  x
5 cr 8752 . . 3  class  RR
64cv 1631 . . . . . 6  class  x
7 cminusr 27766 . . . . . . 7  class  - r
82, 1, 7co 5874 . . . . . 6  class  ( B - r A )
9 ctimesr 27767 . . . . . 6  class  . v
106, 8, 9co 5874 . . . . 5  class  ( x . v ( B - r A ) )
11 cpv 21157 . . . . 5  class  +v
1210, 1, 11co 5874 . . . 4  class  ( ( x . v ( B - r A ) ) +v A
)
13 c1 8754 . . . . 5  class  1
14 c2 9811 . . . . 5  class  2
15 c3 9812 . . . . 5  class  3
1613, 14, 15ctp 3655 . . . 4  class  { 1 ,  2 ,  3 }
1712, 16cima 4708 . . 3  class  ( ( ( x . v ( B - r A ) ) +v A ) " {
1 ,  2 ,  3 } )
184, 5, 17cmpt 4093 . 2  class  ( x  e.  RR  |->  ( ( ( x . v ( B - r A ) ) +v A ) " {
1 ,  2 ,  3 } ) )
193, 18wceq 1632 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