Metamath Proof Explorer

Theorem crctcshwlkn0

Description: Cyclically shifting the indices of a circuit <. F , P >. results in a walk <. H , Q >. . (Contributed by AV, 10-Mar-2021)

Ref Expression
Hypotheses crctcsh.v 
|- V = ( Vtx ` G )
crctcsh.i 
|- I = ( iEdg ` G )
crctcsh.d 
|- ( ph -> F ( Circuits ` G ) P )
crctcsh.n 
|- N = ( # ` F )
crctcsh.s 
|- ( ph -> S e. ( 0 ..^ N ) )
crctcsh.h 
|- H = ( F cyclShift S )
crctcsh.q 
|- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
Assertion crctcshwlkn0 
|- ( ( ph /\ S =/= 0 ) -> H ( Walks ` G ) Q )

Proof

Step Hyp Ref Expression
1 crctcsh.v 
 |-  V = ( Vtx ` G )
2 crctcsh.i 
 |-  I = ( iEdg ` G )
3 crctcsh.d 
 |-  ( ph -> F ( Circuits ` G ) P )
4 crctcsh.n 
 |-  N = ( # ` F )
5 crctcsh.s 
 |-  ( ph -> S e. ( 0 ..^ N ) )
6 crctcsh.h 
 |-  H = ( F cyclShift S )
7 crctcsh.q 
 |-  Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
8 crctiswlk 
 |-  ( F ( Circuits ` G ) P -> F ( Walks ` G ) P )
9 2 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
10 3 8 9 3syl 
 |-  ( ph -> F e. Word dom I )
11 cshwcl 
 |-  ( F e. Word dom I -> ( F cyclShift S ) e. Word dom I )
12 10 11 syl 
 |-  ( ph -> ( F cyclShift S ) e. Word dom I )
13 6 12 eqeltrid 
 |-  ( ph -> H e. Word dom I )
14 13 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> H e. Word dom I )
15 3 8 syl 
 |-  ( ph -> F ( Walks ` G ) P )
16 1 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )
17 simpll 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> V /\ ( ph /\ x e. ( 0 ... N ) ) ) /\ x <_ ( N - S ) ) -> P : ( 0 ... ( # ` F ) ) --> V )
18 elfznn0 
 |-  ( x e. ( 0 ... N ) -> x e. NN0 )
19 18 adantl 
 |-  ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) -> x e. NN0 )
20 elfzonn0 
 |-  ( S e. ( 0 ..^ N ) -> S e. NN0 )
21 20 adantr 
 |-  ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) -> S e. NN0 )
22 19 21 nn0addcld 
 |-  ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) -> ( x + S ) e. NN0 )
23 22 adantr 
 |-  ( ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) /\ x <_ ( N - S ) ) -> ( x + S ) e. NN0 )
24 elfz3nn0 
 |-  ( x e. ( 0 ... N ) -> N e. NN0 )
25 4 24 eqeltrrid 
 |-  ( x e. ( 0 ... N ) -> ( # ` F ) e. NN0 )
26 25 ad2antlr 
 |-  ( ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) /\ x <_ ( N - S ) ) -> ( # ` F ) e. NN0 )
27 elfzelz 
 |-  ( x e. ( 0 ... N ) -> x e. ZZ )
28 27 zred 
 |-  ( x e. ( 0 ... N ) -> x e. RR )
29 28 adantl 
 |-  ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) -> x e. RR )
30 elfzoelz 
 |-  ( S e. ( 0 ..^ N ) -> S e. ZZ )
31 30 zred 
 |-  ( S e. ( 0 ..^ N ) -> S e. RR )
32 31 adantr 
 |-  ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) -> S e. RR )
33 elfzel2 
 |-  ( x e. ( 0 ... N ) -> N e. ZZ )
34 33 zred 
 |-  ( x e. ( 0 ... N ) -> N e. RR )
35 34 adantl 
 |-  ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) -> N e. RR )
36 leaddsub 
 |-  ( ( x e. RR /\ S e. RR /\ N e. RR ) -> ( ( x + S ) <_ N <-> x <_ ( N - S ) ) )
37 29 32 35 36 syl3anc 
 |-  ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) -> ( ( x + S ) <_ N <-> x <_ ( N - S ) ) )
38 37 biimpar 
 |-  ( ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) /\ x <_ ( N - S ) ) -> ( x + S ) <_ N )
39 38 4 breqtrdi 
 |-  ( ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) /\ x <_ ( N - S ) ) -> ( x + S ) <_ ( # ` F ) )
40 23 26 39 3jca 
 |-  ( ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) /\ x <_ ( N - S ) ) -> ( ( x + S ) e. NN0 /\ ( # ` F ) e. NN0 /\ ( x + S ) <_ ( # ` F ) ) )
41 5 40 sylanl1 
 |-  ( ( ( ph /\ x e. ( 0 ... N ) ) /\ x <_ ( N - S ) ) -> ( ( x + S ) e. NN0 /\ ( # ` F ) e. NN0 /\ ( x + S ) <_ ( # ` F ) ) )
42 elfz2nn0 
 |-  ( ( x + S ) e. ( 0 ... ( # ` F ) ) <-> ( ( x + S ) e. NN0 /\ ( # ` F ) e. NN0 /\ ( x + S ) <_ ( # ` F ) ) )
43 41 42 sylibr 
 |-  ( ( ( ph /\ x e. ( 0 ... N ) ) /\ x <_ ( N - S ) ) -> ( x + S ) e. ( 0 ... ( # ` F ) ) )
44 43 adantll 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> V /\ ( ph /\ x e. ( 0 ... N ) ) ) /\ x <_ ( N - S ) ) -> ( x + S ) e. ( 0 ... ( # ` F ) ) )
45 17 44 ffvelrnd 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> V /\ ( ph /\ x e. ( 0 ... N ) ) ) /\ x <_ ( N - S ) ) -> ( P ` ( x + S ) ) e. V )
46 simpll 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> V /\ ( ph /\ x e. ( 0 ... N ) ) ) /\ -. x <_ ( N - S ) ) -> P : ( 0 ... ( # ` F ) ) --> V )
47 elfzoel2 
 |-  ( S e. ( 0 ..^ N ) -> N e. ZZ )
48 zaddcl 
 |-  ( ( x e. ZZ /\ S e. ZZ ) -> ( x + S ) e. ZZ )
49 48 adantrr 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> ( x + S ) e. ZZ )
50 simprr 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> N e. ZZ )
51 49 50 zsubcld 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> ( ( x + S ) - N ) e. ZZ )
52 51 adantr 
 |-  ( ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) /\ -. x <_ ( N - S ) ) -> ( ( x + S ) - N ) e. ZZ )
53 zsubcl 
 |-  ( ( N e. ZZ /\ S e. ZZ ) -> ( N - S ) e. ZZ )
54 53 ancoms 
 |-  ( ( S e. ZZ /\ N e. ZZ ) -> ( N - S ) e. ZZ )
55 54 zred 
 |-  ( ( S e. ZZ /\ N e. ZZ ) -> ( N - S ) e. RR )
56 zre 
 |-  ( x e. ZZ -> x e. RR )
57 ltnle 
 |-  ( ( ( N - S ) e. RR /\ x e. RR ) -> ( ( N - S ) < x <-> -. x <_ ( N - S ) ) )
58 55 56 57 syl2anr 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> ( ( N - S ) < x <-> -. x <_ ( N - S ) ) )
59 zre 
 |-  ( N e. ZZ -> N e. RR )
60 59 adantl 
 |-  ( ( S e. ZZ /\ N e. ZZ ) -> N e. RR )
61 zre 
 |-  ( S e. ZZ -> S e. RR )
62 61 adantr 
 |-  ( ( S e. ZZ /\ N e. ZZ ) -> S e. RR )
63 56 adantr 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> x e. RR )
64 ltsubadd 
 |-  ( ( N e. RR /\ S e. RR /\ x e. RR ) -> ( ( N - S ) < x <-> N < ( x + S ) ) )
65 60 62 63 64 syl2an23an 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> ( ( N - S ) < x <-> N < ( x + S ) ) )
66 60 adantl 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> N e. RR )
67 49 zred 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> ( x + S ) e. RR )
68 66 67 posdifd 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> ( N < ( x + S ) <-> 0 < ( ( x + S ) - N ) ) )
69 0red 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> 0 e. RR )
70 51 zred 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> ( ( x + S ) - N ) e. RR )
71 ltle 
 |-  ( ( 0 e. RR /\ ( ( x + S ) - N ) e. RR ) -> ( 0 < ( ( x + S ) - N ) -> 0 <_ ( ( x + S ) - N ) ) )
72 69 70 71 syl2anc 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> ( 0 < ( ( x + S ) - N ) -> 0 <_ ( ( x + S ) - N ) ) )
73 68 72 sylbid 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> ( N < ( x + S ) -> 0 <_ ( ( x + S ) - N ) ) )
74 65 73 sylbid 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> ( ( N - S ) < x -> 0 <_ ( ( x + S ) - N ) ) )
75 58 74 sylbird 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> ( -. x <_ ( N - S ) -> 0 <_ ( ( x + S ) - N ) ) )
76 75 imp 
 |-  ( ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) /\ -. x <_ ( N - S ) ) -> 0 <_ ( ( x + S ) - N ) )
77 52 76 jca 
 |-  ( ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) /\ -. x <_ ( N - S ) ) -> ( ( ( x + S ) - N ) e. ZZ /\ 0 <_ ( ( x + S ) - N ) ) )
78 77 exp31 
 |-  ( x e. ZZ -> ( ( S e. ZZ /\ N e. ZZ ) -> ( -. x <_ ( N - S ) -> ( ( ( x + S ) - N ) e. ZZ /\ 0 <_ ( ( x + S ) - N ) ) ) ) )
79 78 27 syl11 
 |-  ( ( S e. ZZ /\ N e. ZZ ) -> ( x e. ( 0 ... N ) -> ( -. x <_ ( N - S ) -> ( ( ( x + S ) - N ) e. ZZ /\ 0 <_ ( ( x + S ) - N ) ) ) ) )
80 30 47 79 syl2anc 
 |-  ( S e. ( 0 ..^ N ) -> ( x e. ( 0 ... N ) -> ( -. x <_ ( N - S ) -> ( ( ( x + S ) - N ) e. ZZ /\ 0 <_ ( ( x + S ) - N ) ) ) ) )
81 80 imp31 
 |-  ( ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) /\ -. x <_ ( N - S ) ) -> ( ( ( x + S ) - N ) e. ZZ /\ 0 <_ ( ( x + S ) - N ) ) )
82 elnn0z 
 |-  ( ( ( x + S ) - N ) e. NN0 <-> ( ( ( x + S ) - N ) e. ZZ /\ 0 <_ ( ( x + S ) - N ) ) )
83 81 82 sylibr 
 |-  ( ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) /\ -. x <_ ( N - S ) ) -> ( ( x + S ) - N ) e. NN0 )
84 25 ad2antlr 
 |-  ( ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) /\ -. x <_ ( N - S ) ) -> ( # ` F ) e. NN0 )
85 elfzo0 
 |-  ( S e. ( 0 ..^ N ) <-> ( S e. NN0 /\ N e. NN /\ S < N ) )
86 elfz2nn0 
 |-  ( x e. ( 0 ... N ) <-> ( x e. NN0 /\ N e. NN0 /\ x <_ N ) )
87 nn0re 
 |-  ( S e. NN0 -> S e. RR )
88 87 3ad2ant1 
 |-  ( ( S e. NN0 /\ N e. NN /\ S < N ) -> S e. RR )
89 nn0re 
 |-  ( x e. NN0 -> x e. RR )
90 89 3ad2ant1 
 |-  ( ( x e. NN0 /\ N e. NN0 /\ x <_ N ) -> x e. RR )
91 88 90 anim12ci 
 |-  ( ( ( S e. NN0 /\ N e. NN /\ S < N ) /\ ( x e. NN0 /\ N e. NN0 /\ x <_ N ) ) -> ( x e. RR /\ S e. RR ) )
92 nnre 
 |-  ( N e. NN -> N e. RR )
93 92 92 jca 
 |-  ( N e. NN -> ( N e. RR /\ N e. RR ) )
94 93 3ad2ant2 
 |-  ( ( S e. NN0 /\ N e. NN /\ S < N ) -> ( N e. RR /\ N e. RR ) )
95 94 adantr 
 |-  ( ( ( S e. NN0 /\ N e. NN /\ S < N ) /\ ( x e. NN0 /\ N e. NN0 /\ x <_ N ) ) -> ( N e. RR /\ N e. RR ) )
96 91 95 jca 
 |-  ( ( ( S e. NN0 /\ N e. NN /\ S < N ) /\ ( x e. NN0 /\ N e. NN0 /\ x <_ N ) ) -> ( ( x e. RR /\ S e. RR ) /\ ( N e. RR /\ N e. RR ) ) )
97 simpr3 
 |-  ( ( ( S e. NN0 /\ N e. NN /\ S < N ) /\ ( x e. NN0 /\ N e. NN0 /\ x <_ N ) ) -> x <_ N )
98 ltle 
 |-  ( ( S e. RR /\ N e. RR ) -> ( S < N -> S <_ N ) )
99 87 92 98 syl2an 
 |-  ( ( S e. NN0 /\ N e. NN ) -> ( S < N -> S <_ N ) )
100 99 3impia 
 |-  ( ( S e. NN0 /\ N e. NN /\ S < N ) -> S <_ N )
101 100 adantr 
 |-  ( ( ( S e. NN0 /\ N e. NN /\ S < N ) /\ ( x e. NN0 /\ N e. NN0 /\ x <_ N ) ) -> S <_ N )
102 96 97 101 jca32 
 |-  ( ( ( S e. NN0 /\ N e. NN /\ S < N ) /\ ( x e. NN0 /\ N e. NN0 /\ x <_ N ) ) -> ( ( ( x e. RR /\ S e. RR ) /\ ( N e. RR /\ N e. RR ) ) /\ ( x <_ N /\ S <_ N ) ) )
103 85 86 102 syl2anb 
 |-  ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) -> ( ( ( x e. RR /\ S e. RR ) /\ ( N e. RR /\ N e. RR ) ) /\ ( x <_ N /\ S <_ N ) ) )
104 le2add 
 |-  ( ( ( x e. RR /\ S e. RR ) /\ ( N e. RR /\ N e. RR ) ) -> ( ( x <_ N /\ S <_ N ) -> ( x + S ) <_ ( N + N ) ) )
105 104 imp 
 |-  ( ( ( ( x e. RR /\ S e. RR ) /\ ( N e. RR /\ N e. RR ) ) /\ ( x <_ N /\ S <_ N ) ) -> ( x + S ) <_ ( N + N ) )
106 103 105 syl 
 |-  ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) -> ( x + S ) <_ ( N + N ) )
107 67 66 66 3jca 
 |-  ( ( x e. ZZ /\ ( S e. ZZ /\ N e. ZZ ) ) -> ( ( x + S ) e. RR /\ N e. RR /\ N e. RR ) )
108 107 ex 
 |-  ( x e. ZZ -> ( ( S e. ZZ /\ N e. ZZ ) -> ( ( x + S ) e. RR /\ N e. RR /\ N e. RR ) ) )
109 108 27 syl11 
 |-  ( ( S e. ZZ /\ N e. ZZ ) -> ( x e. ( 0 ... N ) -> ( ( x + S ) e. RR /\ N e. RR /\ N e. RR ) ) )
110 30 47 109 syl2anc 
 |-  ( S e. ( 0 ..^ N ) -> ( x e. ( 0 ... N ) -> ( ( x + S ) e. RR /\ N e. RR /\ N e. RR ) ) )
111 110 imp 
 |-  ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) -> ( ( x + S ) e. RR /\ N e. RR /\ N e. RR ) )
112 lesubadd 
 |-  ( ( ( x + S ) e. RR /\ N e. RR /\ N e. RR ) -> ( ( ( x + S ) - N ) <_ N <-> ( x + S ) <_ ( N + N ) ) )
113 111 112 syl 
 |-  ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) -> ( ( ( x + S ) - N ) <_ N <-> ( x + S ) <_ ( N + N ) ) )
114 106 113 mpbird 
 |-  ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) -> ( ( x + S ) - N ) <_ N )
115 114 adantr 
 |-  ( ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) /\ -. x <_ ( N - S ) ) -> ( ( x + S ) - N ) <_ N )
116 115 4 breqtrdi 
 |-  ( ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) /\ -. x <_ ( N - S ) ) -> ( ( x + S ) - N ) <_ ( # ` F ) )
117 83 84 116 3jca 
 |-  ( ( ( S e. ( 0 ..^ N ) /\ x e. ( 0 ... N ) ) /\ -. x <_ ( N - S ) ) -> ( ( ( x + S ) - N ) e. NN0 /\ ( # ` F ) e. NN0 /\ ( ( x + S ) - N ) <_ ( # ` F ) ) )
118 5 117 sylanl1 
 |-  ( ( ( ph /\ x e. ( 0 ... N ) ) /\ -. x <_ ( N - S ) ) -> ( ( ( x + S ) - N ) e. NN0 /\ ( # ` F ) e. NN0 /\ ( ( x + S ) - N ) <_ ( # ` F ) ) )
119 elfz2nn0 
 |-  ( ( ( x + S ) - N ) e. ( 0 ... ( # ` F ) ) <-> ( ( ( x + S ) - N ) e. NN0 /\ ( # ` F ) e. NN0 /\ ( ( x + S ) - N ) <_ ( # ` F ) ) )
120 118 119 sylibr 
 |-  ( ( ( ph /\ x e. ( 0 ... N ) ) /\ -. x <_ ( N - S ) ) -> ( ( x + S ) - N ) e. ( 0 ... ( # ` F ) ) )
121 120 adantll 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> V /\ ( ph /\ x e. ( 0 ... N ) ) ) /\ -. x <_ ( N - S ) ) -> ( ( x + S ) - N ) e. ( 0 ... ( # ` F ) ) )
122 46 121 ffvelrnd 
 |-  ( ( ( P : ( 0 ... ( # ` F ) ) --> V /\ ( ph /\ x e. ( 0 ... N ) ) ) /\ -. x <_ ( N - S ) ) -> ( P ` ( ( x + S ) - N ) ) e. V )
123 45 122 ifclda 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> V /\ ( ph /\ x e. ( 0 ... N ) ) ) -> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) e. V )
124 123 exp32 
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> ( ph -> ( x e. ( 0 ... N ) -> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) e. V ) ) )
125 16 124 syl 
 |-  ( F ( Walks ` G ) P -> ( ph -> ( x e. ( 0 ... N ) -> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) e. V ) ) )
126 15 125 mpcom 
 |-  ( ph -> ( x e. ( 0 ... N ) -> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) e. V ) )
127 126 imp 
 |-  ( ( ph /\ x e. ( 0 ... N ) ) -> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) e. V )
128 127 7 fmptd 
 |-  ( ph -> Q : ( 0 ... N ) --> V )
129 1 2 3 4 5 6 crctcshlem2 
 |-  ( ph -> ( # ` H ) = N )
130 129 oveq2d 
 |-  ( ph -> ( 0 ... ( # ` H ) ) = ( 0 ... N ) )
131 130 feq2d 
 |-  ( ph -> ( Q : ( 0 ... ( # ` H ) ) --> V <-> Q : ( 0 ... N ) --> V ) )
132 128 131 mpbird 
 |-  ( ph -> Q : ( 0 ... ( # ` H ) ) --> V )
133 132 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> Q : ( 0 ... ( # ` H ) ) --> V )
134 1 2 wlkprop 
 |-  ( F ( Walks ` G ) P -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) )
135 3 8 134 3syl 
 |-  ( ph -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) )
136 135 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) )
137 4 eqcomi 
 |-  ( # ` F ) = N
138 137 oveq2i 
 |-  ( 0 ..^ ( # ` F ) ) = ( 0 ..^ N )
139 138 raleqi 
 |-  ( A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) <-> A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) )
140 fzo1fzo0n0 
 |-  ( S e. ( 1 ..^ N ) <-> ( S e. ( 0 ..^ N ) /\ S =/= 0 ) )
141 140 simplbi2 
 |-  ( S e. ( 0 ..^ N ) -> ( S =/= 0 -> S e. ( 1 ..^ N ) ) )
142 5 141 syl 
 |-  ( ph -> ( S =/= 0 -> S e. ( 1 ..^ N ) ) )
143 142 imp 
 |-  ( ( ph /\ S =/= 0 ) -> S e. ( 1 ..^ N ) )
144 143 ad2antlr 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( ph /\ S =/= 0 ) ) /\ A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) -> S e. ( 1 ..^ N ) )
145 simplll 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( ph /\ S =/= 0 ) ) /\ A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) -> F e. Word dom I )
146 wkslem1 
 |-  ( i = k -> ( if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) <-> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
147 146 cbvralvw 
 |-  ( A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) <-> A. k e. ( 0 ..^ N ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
148 147 biimpi 
 |-  ( A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> A. k e. ( 0 ..^ N ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
149 148 adantl 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( ph /\ S =/= 0 ) ) /\ A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) -> A. k e. ( 0 ..^ N ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
150 crctprop 
 |-  ( F ( Circuits ` G ) P -> ( F ( Trails ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
151 137 fveq2i 
 |-  ( P ` ( # ` F ) ) = ( P ` N )
152 151 eqeq2i 
 |-  ( ( P ` 0 ) = ( P ` ( # ` F ) ) <-> ( P ` 0 ) = ( P ` N ) )
153 152 biimpi 
 |-  ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( P ` 0 ) = ( P ` N ) )
154 153 eqcomd 
 |-  ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( P ` N ) = ( P ` 0 ) )
155 154 adantl 
 |-  ( ( F ( Trails ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( P ` N ) = ( P ` 0 ) )
156 3 150 155 3syl 
 |-  ( ph -> ( P ` N ) = ( P ` 0 ) )
157 156 ad2antrl 
 |-  ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( ph /\ S =/= 0 ) ) -> ( P ` N ) = ( P ` 0 ) )
158 157 adantr 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( ph /\ S =/= 0 ) ) /\ A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) -> ( P ` N ) = ( P ` 0 ) )
159 144 7 6 4 145 149 158 crctcshwlkn0lem7 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( ph /\ S =/= 0 ) ) /\ A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) -> A. j e. ( 0 ..^ N ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )
160 129 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` H ) ) = ( 0 ..^ N ) )
161 160 raleqdv 
 |-  ( ph -> ( A. j e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> A. j e. ( 0 ..^ N ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) )
162 161 ad2antrl 
 |-  ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( ph /\ S =/= 0 ) ) -> ( A. j e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> A. j e. ( 0 ..^ N ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) )
163 162 adantr 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( ph /\ S =/= 0 ) ) /\ A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) -> ( A. j e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) <-> A. j e. ( 0 ..^ N ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) )
164 159 163 mpbird 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( ph /\ S =/= 0 ) ) /\ A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) -> A. j e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )
165 164 ex 
 |-  ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( ph /\ S =/= 0 ) ) -> ( A. i e. ( 0 ..^ N ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> A. j e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) )
166 139 165 syl5bi 
 |-  ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( ph /\ S =/= 0 ) ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> A. j e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) )
167 166 ex 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) -> ( ( ph /\ S =/= 0 ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> A. j e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) ) )
168 167 com23 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> ( ( ph /\ S =/= 0 ) -> A. j e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) ) )
169 168 3impia 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) -> ( ( ph /\ S =/= 0 ) -> A. j e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) )
170 136 169 mpcom 
 |-  ( ( ph /\ S =/= 0 ) -> A. j e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) )
171 14 133 170 3jca 
 |-  ( ( ph /\ S =/= 0 ) -> ( H e. Word dom I /\ Q : ( 0 ... ( # ` H ) ) --> V /\ A. j e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) )
172 1 2 3 4 5 6 7 crctcshlem3 
 |-  ( ph -> ( G e. _V /\ H e. _V /\ Q e. _V ) )
173 172 adantr 
 |-  ( ( ph /\ S =/= 0 ) -> ( G e. _V /\ H e. _V /\ Q e. _V ) )
174 1 2 iswlk 
 |-  ( ( G e. _V /\ H e. _V /\ Q e. _V ) -> ( H ( Walks ` G ) Q <-> ( H e. Word dom I /\ Q : ( 0 ... ( # ` H ) ) --> V /\ A. j e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) ) )
175 173 174 syl 
 |-  ( ( ph /\ S =/= 0 ) -> ( H ( Walks ` G ) Q <-> ( H e. Word dom I /\ Q : ( 0 ... ( # ` H ) ) --> V /\ A. j e. ( 0 ..^ ( # ` H ) ) if- ( ( Q ` j ) = ( Q ` ( j + 1 ) ) , ( I ` ( H ` j ) ) = { ( Q ` j ) } , { ( Q ` j ) , ( Q ` ( j + 1 ) ) } C_ ( I ` ( H ` j ) ) ) ) ) )
176 171 175 mpbird 
 |-  ( ( ph /\ S =/= 0 ) -> H ( Walks ` G ) Q )