Definition df-ptdf 37701

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cptdfc 37685	. 2 class PtDf(𝐴, 𝐵)
4		vx	. . 3 setvar 𝑥
5		cr 9814	. . 3 class ℝ
6	4	cv 1474	. . . . . 6 class 𝑥
7		cminusr 37683	. . . . . . 7 class -𝑟
8	2, 1, 7	co 6549	. . . . . 6 class (𝐵-𝑟𝐴)
9		ctimesr 37684	. . . . . 6 class .𝑣
10	6, 8, 9	co 6549	. . . . 5 class (𝑥.𝑣(𝐵-𝑟𝐴))
11		cpv 26824	. . . . 5 class +𝑣
12	10, 1, 11	co 6549	. . . 4 class ((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴)
13		c1 9816	. . . . 5 class 1
14		c2 10947	. . . . 5 class 2
15		c3 10948	. . . . 5 class 3
16	13, 14, 15	ctp 4129	. . . 4 class {1, 2, 3}
17	12, 16	cima 5041	. . 3 class (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3})
18	4, 5, 17	cmpt 4643	. 2 class (𝑥 ∈ ℝ ↦ (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3}))
19	3, 18	wceq 1475	1 wff PtDf(𝐴, 𝐵) = (𝑥 ∈ ℝ ↦ (((𝑥.𝑣(𝐵-𝑟𝐴)) +𝑣 𝐴) “ {1, 2, 3}))

This definition is referenced by: (None)