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