Metamath Proof Explorer


Theorem 3wlkdlem8

Description: Lemma 8 for 3wlkd . (Contributed by Alexander van der Vekens, 12-Nov-2017) (Revised by AV, 7-Feb-2021)

Ref Expression
Hypotheses 3wlkd.p P = ⟨“ ABCD ”⟩
3wlkd.f F = ⟨“ JKL ”⟩
3wlkd.s φ A V B V C V D V
3wlkd.n φ A B A C B C B D C D
3wlkd.e φ A B I J B C I K C D I L
Assertion 3wlkdlem8 φ F 0 = J F 1 = K F 2 = L

Proof

Step Hyp Ref Expression
1 3wlkd.p P = ⟨“ ABCD ”⟩
2 3wlkd.f F = ⟨“ JKL ”⟩
3 3wlkd.s φ A V B V C V D V
4 3wlkd.n φ A B A C B C B D C D
5 3wlkd.e φ A B I J B C I K C D I L
6 1 2 3 4 5 3wlkdlem7 φ J V K V L V
7 s3fv0 J V ⟨“ JKL ”⟩ 0 = J
8 s3fv1 K V ⟨“ JKL ”⟩ 1 = K
9 s3fv2 L V ⟨“ JKL ”⟩ 2 = L
10 7 8 9 3anim123i J V K V L V ⟨“ JKL ”⟩ 0 = J ⟨“ JKL ”⟩ 1 = K ⟨“ JKL ”⟩ 2 = L
11 6 10 syl φ ⟨“ JKL ”⟩ 0 = J ⟨“ JKL ”⟩ 1 = K ⟨“ JKL ”⟩ 2 = L
12 2 fveq1i F 0 = ⟨“ JKL ”⟩ 0
13 12 eqeq1i F 0 = J ⟨“ JKL ”⟩ 0 = J
14 2 fveq1i F 1 = ⟨“ JKL ”⟩ 1
15 14 eqeq1i F 1 = K ⟨“ JKL ”⟩ 1 = K
16 2 fveq1i F 2 = ⟨“ JKL ”⟩ 2
17 16 eqeq1i F 2 = L ⟨“ JKL ”⟩ 2 = L
18 13 15 17 3anbi123i F 0 = J F 1 = K F 2 = L ⟨“ JKL ”⟩ 0 = J ⟨“ JKL ”⟩ 1 = K ⟨“ JKL ”⟩ 2 = L
19 11 18 sylibr φ F 0 = J F 1 = K F 2 = L