Metamath Proof Explorer


Theorem 2wlkdlem3

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

Ref Expression
Hypotheses 2wlkd.p 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2wlkd.f 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
2wlkd.s ( 𝜑 → ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) )
Assertion 2wlkdlem3 ( 𝜑 → ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 2wlkd.p 𝑃 = ⟨“ 𝐴 𝐵 𝐶 ”⟩
2 2wlkd.f 𝐹 = ⟨“ 𝐽 𝐾 ”⟩
3 2wlkd.s ( 𝜑 → ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) )
4 1 fveq1i ( 𝑃 ‘ 0 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 )
5 s3fv0 ( 𝐴𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 0 ) = 𝐴 )
6 4 5 syl5eq ( 𝐴𝑉 → ( 𝑃 ‘ 0 ) = 𝐴 )
7 1 fveq1i ( 𝑃 ‘ 1 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 )
8 s3fv1 ( 𝐵𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 1 ) = 𝐵 )
9 7 8 syl5eq ( 𝐵𝑉 → ( 𝑃 ‘ 1 ) = 𝐵 )
10 1 fveq1i ( 𝑃 ‘ 2 ) = ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 )
11 s3fv2 ( 𝐶𝑉 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ‘ 2 ) = 𝐶 )
12 10 11 syl5eq ( 𝐶𝑉 → ( 𝑃 ‘ 2 ) = 𝐶 )
13 6 9 12 3anim123i ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) → ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) )
14 3 13 syl ( 𝜑 → ( ( 𝑃 ‘ 0 ) = 𝐴 ∧ ( 𝑃 ‘ 1 ) = 𝐵 ∧ ( 𝑃 ‘ 2 ) = 𝐶 ) )