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