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 ( 𝐴 , 𝐵 ) = ( 𝑥 ∈ ℝ ↦ ( ( ( 𝑥 .𝑣 ( 𝐵 -𝑟 𝐴 ) ) +𝑣 𝐴 ) “ { 1 , 2 , 3 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	cptdfc	⊢ PtDf ( 𝐴 , 𝐵 )
3		vx	⊢ 𝑥
4		cr	⊢ ℝ
5	3	cv	⊢ 𝑥
6		ctimesr	⊢ .𝑣
7		cminusr	⊢ -𝑟
8	1 0 7	co	⊢ ( 𝐵 -𝑟 𝐴 )
9	5 8 6	co	⊢ ( 𝑥 .𝑣 ( 𝐵 -𝑟 𝐴 ) )
10		cpv	⊢ +𝑣
11	9 0 10	co	⊢ ( ( 𝑥 .𝑣 ( 𝐵 -𝑟 𝐴 ) ) +𝑣 𝐴 )
12		c1	⊢ 1
13		c2	⊢ 2
14		c3	⊢ 3
15	12 13 14	ctp	⊢ { 1 , 2 , 3 }
16	11 15	cima	⊢ ( ( ( 𝑥 .𝑣 ( 𝐵 -𝑟 𝐴 ) ) +𝑣 𝐴 ) “ { 1 , 2 , 3 } )
17	3 4 16	cmpt	⊢ ( 𝑥 ∈ ℝ ↦ ( ( ( 𝑥 .𝑣 ( 𝐵 -𝑟 𝐴 ) ) +𝑣 𝐴 ) “ { 1 , 2 , 3 } ) )
18	2 17	wceq	⊢ PtDf ( 𝐴 , 𝐵 ) = ( 𝑥 ∈ ℝ ↦ ( ( ( 𝑥 .𝑣 ( 𝐵 -𝑟 𝐴 ) ) +𝑣 𝐴 ) “ { 1 , 2 , 3 } ) )