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 ( A , B ) = ( x e. RR |-> ( ( ( x .v ( B -r A ) ) +v A ) " { 1 , 2 , 3 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	cptdfc	|- PtDf ( A , B )
3		vx	|- x
4		cr	|- RR
5	3	cv	|- x
6		ctimesr	|- .v
7		cminusr	|- -r
8	1 0 7	co	|- ( B -r A )
9	5 8 6	co	|- ( x .v ( B -r A ) )
10		cpv	|- +v
11	9 0 10	co	|- ( ( x .v ( B -r A ) ) +v A )
12		c1	|- 1
13		c2	|- 2
14		c3	|- 3
15	12 13 14	ctp	|- { 1 , 2 , 3 }
16	11 15	cima	|- ( ( ( x .v ( B -r A ) ) +v A ) " { 1 , 2 , 3 } )
17	3 4 16	cmpt	|- ( x e. RR |-> ( ( ( x .v ( B -r A ) ) +v A ) " { 1 , 2 , 3 } ) )
18	2 17	wceq	|- PtDf ( A , B ) = ( x e. RR |-> ( ( ( x .v ( B -r A ) ) +v A ) " { 1 , 2 , 3 } ) )