Metamath Proof Explorer


Theorem eleclclwwlknlem1

Description: Lemma 1 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 eleclclwwlknlem1 K 0 N X W Y W X = Y cyclShift K m 0 N Z = Y cyclShift m n 0 N Z = X cyclShift n

Proof

Step Hyp Ref Expression
1 erclwwlkn1.w W = N ClWWalksN G
2 eqid Vtx G = Vtx G
3 2 clwwlknbp Y N ClWWalksN G Y Word Vtx G Y = N
4 3 1 eleq2s Y W Y Word Vtx G Y = N
5 4 adantl X W Y W Y Word Vtx G Y = N
6 5 adantl K 0 N X W Y W Y Word Vtx G Y = N
7 6 adantr K 0 N X W Y W X = Y cyclShift K m 0 N Z = Y cyclShift m Y Word Vtx G Y = N
8 simpl K 0 N X W Y W K 0 N
9 8 adantr K 0 N X W Y W X = Y cyclShift K m 0 N Z = Y cyclShift m K 0 N
10 simpl X = Y cyclShift K m 0 N Z = Y cyclShift m X = Y cyclShift K
11 10 adantl K 0 N X W Y W X = Y cyclShift K m 0 N Z = Y cyclShift m X = Y cyclShift K
12 simprr K 0 N X W Y W X = Y cyclShift K m 0 N Z = Y cyclShift m m 0 N Z = Y cyclShift m
13 9 11 12 3jca K 0 N X W Y W X = Y cyclShift K m 0 N Z = Y cyclShift m K 0 N X = Y cyclShift K m 0 N Z = Y cyclShift m
14 2cshwcshw Y Word Vtx G Y = N K 0 N X = Y cyclShift K m 0 N Z = Y cyclShift m n 0 N Z = X cyclShift n
15 7 13 14 sylc K 0 N X W Y W X = Y cyclShift K m 0 N Z = Y cyclShift m n 0 N Z = X cyclShift n
16 15 ex K 0 N X W Y W X = Y cyclShift K m 0 N Z = Y cyclShift m n 0 N Z = X cyclShift n