Metamath Proof Explorer


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 } ) )