Definition df-ptdf 38680

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

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cptdfc 38664	. 2 class PtDf ( A , B )
4		vx	. . 3 setvar x
5		cr 9935	. . 3 class RR
6	4	cv 1482	. . . . . 6 class x
7		cminusr 38662	. . . . . . 7 class -r
8	2, 1, 7	co 6650	. . . . . 6 class ( B -r A )
9		ctimesr 38663	. . . . . 6 class .v
10	6, 8, 9	co 6650	. . . . 5 class ( x .v ( B -r A ) )
11		cpv 27440	. . . . 5 class +v
12	10, 1, 11	co 6650	. . . 4 class ( ( x .v ( B -r A ) ) +v A )
13		c1 9937	. . . . 5 class 1
14		c2 11070	. . . . 5 class 2
15		c3 11071	. . . . 5 class 3
16	13, 14, 15	ctp 4181	. . . 4 class { 1 , 2 , 3 }
17	12, 16	cima 5117	. . 3 class ( ( ( x .v ( B -r A ) ) +v A ) " { 1 , 2 , 3 } )
18	4, 5, 17	cmpt 4729	. 2 class ( x e. RR |-> ( ( ( x .v ( B -r A ) ) +v A ) " { 1 , 2 , 3 } ) )
19	3, 18	wceq 1483	1 wff PtDf ( A , B ) = ( x e. RR |-> ( ( ( x .v ( B -r A ) ) +v A ) " { 1 , 2 , 3 } ) )

This definition is referenced by: (None)