Definition df-ptdf

Description: Define the predicate PtDf , which is a utility definition used to shorten definitions and simplify proofs. (Contributed by Andrew Salmon, 15-Jul-2012)

	Ref	Expression
Assertion	df-ptdf	$$⊢PtDf\left(A,B\right)=\left(x\in ℝ⟼\left(\left(x{\cdot }_v\left(B{-}_{r}A\right)\right){+}_{v}A\right)\left[\left\{1,2,3\right\}\right]\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	cptdfc	$$classPtDf\left(A,B\right)$$
3		vx	$$setvarx$$
4		cr	$$classℝ$$
5	3	cv	$$setvarx$$
6		ctimesr	$$class{\cdot }_v$$
7		cminusr	$$class{-}_r$$
8	1 0 7	co	$$class\left(B{-}_{r}A\right)$$
9	5 8 6	co	$$class\left(x{\cdot }_v\left(B{-}_{r}A\right)\right)$$
10		cpv	$$class{+}_v$$
11	9 0 10	co	$$class\left(\left(x{\cdot }_v\left(B{-}_{r}A\right)\right){+}_{v}A\right)$$
12		c1	$$class1$$
13		c2	$$class2$$
14		c3	$$class3$$
15	12 13 14	ctp	$$class\left\{1,2,3\right\}$$
16	11 15	cima	$$class\left(\left(x{\cdot }_v\left(B{-}_{r}A\right)\right){+}_{v}A\right)\left[\left\{1,2,3\right\}\right]$$
17	3 4 16	cmpt	$$class\left(x\in ℝ⟼\left(\left(x{\cdot }_v\left(B{-}_{r}A\right)\right){+}_{v}A\right)\left[\left\{1,2,3\right\}\right]\right)$$
18	2 17	wceq	$$wffPtDf\left(A,B\right)=\left(x\in ℝ⟼\left(\left(x{\cdot }_v\left(B{-}_{r}A\right)\right){+}_{v}A\right)\left[\left\{1,2,3\right\}\right]\right)$$