Metamath Proof Explorer


Theorem 2wlkdlem3

Description: Lemma 3 for 2wlkd . (Contributed by AV, 14-Feb-2021)

Ref Expression
Hypotheses 2wlkd.p
|- P = <" A B C ">
2wlkd.f
|- F = <" J K ">
2wlkd.s
|- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )
Assertion 2wlkdlem3
|- ( ph -> ( ( P ` 0 ) = A /\ ( P ` 1 ) = B /\ ( P ` 2 ) = C ) )

Proof

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