Metamath Proof Explorer


Theorem eleclclwwlknlem2

Description: Lemma 2 for eleclclwwlkn . (Contributed by Alexander van der Vekens, 11-May-2018) (Revised by AV, 30-Apr-2021)

Ref Expression
Hypothesis erclwwlkn1.w W = N ClWWalksN G
Assertion eleclclwwlknlem2 k 0 N X = x cyclShift k X W x W m 0 N Y = x cyclShift m n 0 N Y = X cyclShift n

Proof

Step Hyp Ref Expression
1 erclwwlkn1.w W = N ClWWalksN G
2 simpl k 0 N X = x cyclShift k k 0 N
3 2 anim1i k 0 N X = x cyclShift k X W x W k 0 N X W x W
4 3 adantr k 0 N X = x cyclShift k X W x W m 0 N Y = x cyclShift m k 0 N X W x W
5 simpr k 0 N X = x cyclShift k X = x cyclShift k
6 5 adantr k 0 N X = x cyclShift k X W x W X = x cyclShift k
7 6 anim1i k 0 N X = x cyclShift k X W x W m 0 N Y = x cyclShift m X = x cyclShift k m 0 N Y = x cyclShift m
8 1 eleclclwwlknlem1 k 0 N X W x W X = x cyclShift k m 0 N Y = x cyclShift m n 0 N Y = X cyclShift n
9 4 7 8 sylc k 0 N X = x cyclShift k X W x W m 0 N Y = x cyclShift m n 0 N Y = X cyclShift n
10 eqid Vtx G = Vtx G
11 10 clwwlknbp x N ClWWalksN G x Word Vtx G x = N
12 11 1 eleq2s x W x Word Vtx G x = N
13 fznn0sub2 k 0 N N k 0 N
14 oveq1 x = N x k = N k
15 14 eleq1d x = N x k 0 N N k 0 N
16 13 15 syl5ibr x = N k 0 N x k 0 N
17 16 adantl x Word Vtx G x = N k 0 N x k 0 N
18 12 17 syl x W k 0 N x k 0 N
19 18 adantl X W x W k 0 N x k 0 N
20 19 com12 k 0 N X W x W x k 0 N
21 20 adantr k 0 N X = x cyclShift k X W x W x k 0 N
22 21 imp k 0 N X = x cyclShift k X W x W x k 0 N
23 22 adantr k 0 N X = x cyclShift k X W x W n 0 N Y = X cyclShift n x k 0 N
24 simpr k 0 N X = x cyclShift k X W x W X W x W
25 24 ancomd k 0 N X = x cyclShift k X W x W x W X W
26 25 adantr k 0 N X = x cyclShift k X W x W n 0 N Y = X cyclShift n x W X W
27 23 26 jca k 0 N X = x cyclShift k X W x W n 0 N Y = X cyclShift n x k 0 N x W X W
28 simpll x Word Vtx G x = N k 0 N x Word Vtx G
29 oveq2 N = x 0 N = 0 x
30 29 eleq2d N = x k 0 N k 0 x
31 30 eqcoms x = N k 0 N k 0 x
32 31 adantl x Word Vtx G x = N k 0 N k 0 x
33 32 biimpa x Word Vtx G x = N k 0 N k 0 x
34 28 33 jca x Word Vtx G x = N k 0 N x Word Vtx G k 0 x
35 34 ex x Word Vtx G x = N k 0 N x Word Vtx G k 0 x
36 12 35 syl x W k 0 N x Word Vtx G k 0 x
37 36 adantl X W x W k 0 N x Word Vtx G k 0 x
38 37 com12 k 0 N X W x W x Word Vtx G k 0 x
39 38 adantr k 0 N X = x cyclShift k X W x W x Word Vtx G k 0 x
40 39 imp k 0 N X = x cyclShift k X W x W x Word Vtx G k 0 x
41 5 eqcomd k 0 N X = x cyclShift k x cyclShift k = X
42 41 adantr k 0 N X = x cyclShift k X W x W x cyclShift k = X
43 oveq1 X = x cyclShift k X cyclShift x k = x cyclShift k cyclShift x k
44 43 eqcoms x cyclShift k = X X cyclShift x k = x cyclShift k cyclShift x k
45 elfzelz k 0 x k
46 2cshwid x Word Vtx G k x cyclShift k cyclShift x k = x
47 45 46 sylan2 x Word Vtx G k 0 x x cyclShift k cyclShift x k = x
48 44 47 sylan9eqr x Word Vtx G k 0 x x cyclShift k = X X cyclShift x k = x
49 40 42 48 syl2anc k 0 N X = x cyclShift k X W x W X cyclShift x k = x
50 49 eqcomd k 0 N X = x cyclShift k X W x W x = X cyclShift x k
51 50 anim1i k 0 N X = x cyclShift k X W x W n 0 N Y = X cyclShift n x = X cyclShift x k n 0 N Y = X cyclShift n
52 1 eleclclwwlknlem1 x k 0 N x W X W x = X cyclShift x k n 0 N Y = X cyclShift n m 0 N Y = x cyclShift m
53 27 51 52 sylc k 0 N X = x cyclShift k X W x W n 0 N Y = X cyclShift n m 0 N Y = x cyclShift m
54 9 53 impbida k 0 N X = x cyclShift k X W x W m 0 N Y = x cyclShift m n 0 N Y = X cyclShift n