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