| Step |
Hyp |
Ref |
Expression |
| 1 |
|
2wlkd.p |
|- P = <" A B C "> |
| 2 |
|
2wlkd.f |
|- F = <" J K "> |
| 3 |
|
2wlkd.s |
|- ( ph -> ( A e. V /\ B e. V /\ C e. V ) ) |
| 4 |
1
|
fveq1i |
|- ( P ` 0 ) = ( <" A B C "> ` 0 ) |
| 5 |
|
s3fv0 |
|- ( A e. V -> ( <" A B C "> ` 0 ) = A ) |
| 6 |
4 5
|
eqtrid |
|- ( A e. V -> ( P ` 0 ) = A ) |
| 7 |
1
|
fveq1i |
|- ( P ` 1 ) = ( <" A B C "> ` 1 ) |
| 8 |
|
s3fv1 |
|- ( B e. V -> ( <" A B C "> ` 1 ) = B ) |
| 9 |
7 8
|
eqtrid |
|- ( B e. V -> ( P ` 1 ) = B ) |
| 10 |
1
|
fveq1i |
|- ( P ` 2 ) = ( <" A B C "> ` 2 ) |
| 11 |
|
s3fv2 |
|- ( C e. V -> ( <" A B C "> ` 2 ) = C ) |
| 12 |
10 11
|
eqtrid |
|- ( C e. V -> ( P ` 2 ) = C ) |
| 13 |
6 9 12
|
3anim123i |
|- ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) ) |
| 14 |
3 13
|
syl |
|- ( ph -> ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) ) |