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 e. ( 0 ... N ) /\ X = ( x cyclShift k ) ) /\ ( X e. W /\ x e. W ) ) -> ( E. m e. ( 0 ... N ) Y = ( x cyclShift m ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) )

Proof

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