Mathbox for Andrew Salmon < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ptdf Structured version   Visualization version   GIF version

Definition df-ptdf 41553
 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(𝐴, 𝐵) = (𝑥 ∈ ℝ ↦ (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3}))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Detailed syntax breakdown of Definition df-ptdf
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cptdfc 41537 . 2 class PtDf(𝐴, 𝐵)
4 vx . . 3 setvar 𝑥
5 cr 10574 . . 3 class
64cv 1537 . . . . . 6 class 𝑥
7 cminusr 41535 . . . . . . 7 class -𝑟
82, 1, 7co 7150 . . . . . 6 class (𝐵-𝑟𝐴)
9 ctimesr 41536 . . . . . 6 class .𝑣
106, 8, 9co 7150 . . . . 5 class (𝑥.𝑣(𝐵-𝑟𝐴))
11 cpv 28467 . . . . 5 class +𝑣
1210, 1, 11co 7150 . . . 4 class ((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴)
13 c1 10576 . . . . 5 class 1
14 c2 11729 . . . . 5 class 2
15 c3 11730 . . . . 5 class 3
1613, 14, 15ctp 4526 . . . 4 class {1, 2, 3}
1712, 16cima 5527 . . 3 class (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3})
184, 5, 17cmpt 5112 . 2 class (𝑥 ∈ ℝ ↦ (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3}))
193, 18wceq 1538 1 wff PtDf(𝐴, 𝐵) = (𝑥 ∈ ℝ ↦ (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3}))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator