Metamath Proof Explorer

Theorem eucrct2eupth

Description: Removing one edge ( I( FJ ) ) from a graph G with an Eulerian circuit <. F , P >. results in a graph S with an Eulerian path <. H , Q >. . (Contributed by AV, 17-Mar-2021) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022)

Ref Expression
Hypotheses eucrct2eupth1.v 
|- V = ( Vtx ` G )
eucrct2eupth1.i 
|- I = ( iEdg ` G )
eucrct2eupth1.d 
|- ( ph -> F ( EulerPaths ` G ) P )
eucrct2eupth1.c 
|- ( ph -> F ( Circuits ` G ) P )
eucrct2eupth1.s 
|- ( Vtx ` S ) = V
eucrct2eupth.n 
|- ( ph -> N = ( # ` F ) )
eucrct2eupth.j 
|- ( ph -> J e. ( 0 ..^ N ) )
eucrct2eupth.e 
|- ( ph -> ( iEdg ` S ) = ( I |` ( F " ( ( 0 ..^ N ) \ { J } ) ) ) )
eucrct2eupth.k 
|- K = ( J + 1 )
eucrct2eupth.h 
|- H = ( ( F cyclShift K ) prefix ( N - 1 ) )
eucrct2eupth.q 
|- Q = ( x e. ( 0 ..^ N ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) )
Assertion eucrct2eupth 
|- ( ph -> H ( EulerPaths ` S ) Q )

Proof

Step Hyp Ref Expression
1 eucrct2eupth1.v 
 |-  V = ( Vtx ` G )
2 eucrct2eupth1.i 
 |-  I = ( iEdg ` G )
3 eucrct2eupth1.d 
 |-  ( ph -> F ( EulerPaths ` G ) P )
4 eucrct2eupth1.c 
 |-  ( ph -> F ( Circuits ` G ) P )
5 eucrct2eupth1.s 
 |-  ( Vtx ` S ) = V
6 eucrct2eupth.n 
 |-  ( ph -> N = ( # ` F ) )
7 eucrct2eupth.j 
 |-  ( ph -> J e. ( 0 ..^ N ) )
8 eucrct2eupth.e 
 |-  ( ph -> ( iEdg ` S ) = ( I |` ( F " ( ( 0 ..^ N ) \ { J } ) ) ) )
9 eucrct2eupth.k 
 |-  K = ( J + 1 )
10 eucrct2eupth.h 
 |-  H = ( ( F cyclShift K ) prefix ( N - 1 ) )
11 eucrct2eupth.q 
 |-  Q = ( x e. ( 0 ..^ N ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) )
12 3 adantl 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> F ( EulerPaths ` G ) P )
13 9 eqcomi 
 |-  ( J + 1 ) = K
14 13 oveq2i 
 |-  ( F cyclShift ( J + 1 ) ) = ( F cyclShift K )
15 oveq1 
 |-  ( J = ( N - 1 ) -> ( J + 1 ) = ( ( N - 1 ) + 1 ) )
16 elfzo0 
 |-  ( J e. ( 0 ..^ N ) <-> ( J e. NN0 /\ N e. NN /\ J < N ) )
17 nncn 
 |-  ( N e. NN -> N e. CC )
18 17 3ad2ant2 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> N e. CC )
19 16 18 sylbi 
 |-  ( J e. ( 0 ..^ N ) -> N e. CC )
20 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
21 7 19 20 3syl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
22 15 21 sylan9eq 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( J + 1 ) = N )
23 22 oveq2d 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( F cyclShift ( J + 1 ) ) = ( F cyclShift N ) )
24 6 oveq2d 
 |-  ( ph -> ( F cyclShift N ) = ( F cyclShift ( # ` F ) ) )
25 crctiswlk 
 |-  ( F ( Circuits ` G ) P -> F ( Walks ` G ) P )
26 2 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
27 25 26 syl 
 |-  ( F ( Circuits ` G ) P -> F e. Word dom I )
28 4 27 syl 
 |-  ( ph -> F e. Word dom I )
29 cshwn 
 |-  ( F e. Word dom I -> ( F cyclShift ( # ` F ) ) = F )
30 28 29 syl 
 |-  ( ph -> ( F cyclShift ( # ` F ) ) = F )
31 24 30 eqtrd 
 |-  ( ph -> ( F cyclShift N ) = F )
32 31 adantl 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( F cyclShift N ) = F )
33 23 32 eqtrd 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( F cyclShift ( J + 1 ) ) = F )
34 14 33 eqtr3id 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( F cyclShift K ) = F )
35 eqid 
 |-  ( # ` F ) = ( # ` F )
36 1 2 4 35 crctcshlem1 
 |-  ( ph -> ( # ` F ) e. NN0 )
37 fz0sn0fz1 
 |-  ( ( # ` F ) e. NN0 -> ( 0 ... ( # ` F ) ) = ( { 0 } u. ( 1 ... ( # ` F ) ) ) )
38 36 37 syl 
 |-  ( ph -> ( 0 ... ( # ` F ) ) = ( { 0 } u. ( 1 ... ( # ` F ) ) ) )
39 38 eleq2d 
 |-  ( ph -> ( x e. ( 0 ... ( # ` F ) ) <-> x e. ( { 0 } u. ( 1 ... ( # ` F ) ) ) ) )
40 elun 
 |-  ( x e. ( { 0 } u. ( 1 ... ( # ` F ) ) ) <-> ( x e. { 0 } \/ x e. ( 1 ... ( # ` F ) ) ) )
41 39 40 bitrdi 
 |-  ( ph -> ( x e. ( 0 ... ( # ` F ) ) <-> ( x e. { 0 } \/ x e. ( 1 ... ( # ` F ) ) ) ) )
42 elsni 
 |-  ( x e. { 0 } -> x = 0 )
43 0le0 
 |-  0 <_ 0
44 42 43 eqbrtrdi 
 |-  ( x e. { 0 } -> x <_ 0 )
45 44 adantl 
 |-  ( ( ph /\ x e. { 0 } ) -> x <_ 0 )
46 45 iftrued 
 |-  ( ( ph /\ x e. { 0 } ) -> if ( x <_ 0 , ( P ` ( x + N ) ) , ( P ` ( ( x + N ) - N ) ) ) = ( P ` ( x + N ) ) )
47 6 fveq2d 
 |-  ( ph -> ( P ` N ) = ( P ` ( # ` F ) ) )
48 crctprop 
 |-  ( F ( Circuits ` G ) P -> ( F ( Trails ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
49 simpr 
 |-  ( ( F ( Trails ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( P ` 0 ) = ( P ` ( # ` F ) ) )
50 49 eqcomd 
 |-  ( ( F ( Trails ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( P ` ( # ` F ) ) = ( P ` 0 ) )
51 4 48 50 3syl 
 |-  ( ph -> ( P ` ( # ` F ) ) = ( P ` 0 ) )
52 47 51 eqtrd 
 |-  ( ph -> ( P ` N ) = ( P ` 0 ) )
53 52 adantr 
 |-  ( ( ph /\ x = 0 ) -> ( P ` N ) = ( P ` 0 ) )
54 oveq1 
 |-  ( x = 0 -> ( x + N ) = ( 0 + N ) )
55 7 19 syl 
 |-  ( ph -> N e. CC )
56 55 addlidd 
 |-  ( ph -> ( 0 + N ) = N )
57 54 56 sylan9eqr 
 |-  ( ( ph /\ x = 0 ) -> ( x + N ) = N )
58 57 fveq2d 
 |-  ( ( ph /\ x = 0 ) -> ( P ` ( x + N ) ) = ( P ` N ) )
59 fveq2 
 |-  ( x = 0 -> ( P ` x ) = ( P ` 0 ) )
60 59 adantl 
 |-  ( ( ph /\ x = 0 ) -> ( P ` x ) = ( P ` 0 ) )
61 53 58 60 3eqtr4d 
 |-  ( ( ph /\ x = 0 ) -> ( P ` ( x + N ) ) = ( P ` x ) )
62 42 61 sylan2 
 |-  ( ( ph /\ x e. { 0 } ) -> ( P ` ( x + N ) ) = ( P ` x ) )
63 46 62 eqtrd 
 |-  ( ( ph /\ x e. { 0 } ) -> if ( x <_ 0 , ( P ` ( x + N ) ) , ( P ` ( ( x + N ) - N ) ) ) = ( P ` x ) )
64 63 ex 
 |-  ( ph -> ( x e. { 0 } -> if ( x <_ 0 , ( P ` ( x + N ) ) , ( P ` ( ( x + N ) - N ) ) ) = ( P ` x ) ) )
65 elfznn 
 |-  ( x e. ( 1 ... ( # ` F ) ) -> x e. NN )
66 nnnle0 
 |-  ( x e. NN -> -. x <_ 0 )
67 65 66 syl 
 |-  ( x e. ( 1 ... ( # ` F ) ) -> -. x <_ 0 )
68 67 adantl 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` F ) ) ) -> -. x <_ 0 )
69 68 iffalsed 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` F ) ) ) -> if ( x <_ 0 , ( P ` ( x + N ) ) , ( P ` ( ( x + N ) - N ) ) ) = ( P ` ( ( x + N ) - N ) ) )
70 65 nncnd 
 |-  ( x e. ( 1 ... ( # ` F ) ) -> x e. CC )
71 70 adantl 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` F ) ) ) -> x e. CC )
72 55 adantr 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` F ) ) ) -> N e. CC )
73 71 72 pncand 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` F ) ) ) -> ( ( x + N ) - N ) = x )
74 73 fveq2d 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` F ) ) ) -> ( P ` ( ( x + N ) - N ) ) = ( P ` x ) )
75 69 74 eqtrd 
 |-  ( ( ph /\ x e. ( 1 ... ( # ` F ) ) ) -> if ( x <_ 0 , ( P ` ( x + N ) ) , ( P ` ( ( x + N ) - N ) ) ) = ( P ` x ) )
76 75 ex 
 |-  ( ph -> ( x e. ( 1 ... ( # ` F ) ) -> if ( x <_ 0 , ( P ` ( x + N ) ) , ( P ` ( ( x + N ) - N ) ) ) = ( P ` x ) ) )
77 64 76 jaod 
 |-  ( ph -> ( ( x e. { 0 } \/ x e. ( 1 ... ( # ` F ) ) ) -> if ( x <_ 0 , ( P ` ( x + N ) ) , ( P ` ( ( x + N ) - N ) ) ) = ( P ` x ) ) )
78 41 77 sylbid 
 |-  ( ph -> ( x e. ( 0 ... ( # ` F ) ) -> if ( x <_ 0 , ( P ` ( x + N ) ) , ( P ` ( ( x + N ) - N ) ) ) = ( P ` x ) ) )
79 78 imp 
 |-  ( ( ph /\ x e. ( 0 ... ( # ` F ) ) ) -> if ( x <_ 0 , ( P ` ( x + N ) ) , ( P ` ( ( x + N ) - N ) ) ) = ( P ` x ) )
80 79 mpteq2dva 
 |-  ( ph -> ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ 0 , ( P ` ( x + N ) ) , ( P ` ( ( x + N ) - N ) ) ) ) = ( x e. ( 0 ... ( # ` F ) ) |-> ( P ` x ) ) )
81 80 adantl 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ 0 , ( P ` ( x + N ) ) , ( P ` ( ( x + N ) - N ) ) ) ) = ( x e. ( 0 ... ( # ` F ) ) |-> ( P ` x ) ) )
82 9 oveq2i 
 |-  ( N - K ) = ( N - ( J + 1 ) )
83 15 oveq2d 
 |-  ( J = ( N - 1 ) -> ( N - ( J + 1 ) ) = ( N - ( ( N - 1 ) + 1 ) ) )
84 21 oveq2d 
 |-  ( ph -> ( N - ( ( N - 1 ) + 1 ) ) = ( N - N ) )
85 55 subidd 
 |-  ( ph -> ( N - N ) = 0 )
86 84 85 eqtrd 
 |-  ( ph -> ( N - ( ( N - 1 ) + 1 ) ) = 0 )
87 83 86 sylan9eq 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( N - ( J + 1 ) ) = 0 )
88 82 87 eqtrid 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( N - K ) = 0 )
89 88 breq2d 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( x <_ ( N - K ) <-> x <_ 0 ) )
90 9 oveq2i 
 |-  ( x + K ) = ( x + ( J + 1 ) )
91 90 fveq2i 
 |-  ( P ` ( x + K ) ) = ( P ` ( x + ( J + 1 ) ) )
92 15 oveq2d 
 |-  ( J = ( N - 1 ) -> ( x + ( J + 1 ) ) = ( x + ( ( N - 1 ) + 1 ) ) )
93 21 oveq2d 
 |-  ( ph -> ( x + ( ( N - 1 ) + 1 ) ) = ( x + N ) )
94 92 93 sylan9eq 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( x + ( J + 1 ) ) = ( x + N ) )
95 94 fveq2d 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( P ` ( x + ( J + 1 ) ) ) = ( P ` ( x + N ) ) )
96 91 95 eqtrid 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( P ` ( x + K ) ) = ( P ` ( x + N ) ) )
97 90 oveq1i 
 |-  ( ( x + K ) - N ) = ( ( x + ( J + 1 ) ) - N )
98 97 fveq2i 
 |-  ( P ` ( ( x + K ) - N ) ) = ( P ` ( ( x + ( J + 1 ) ) - N ) )
99 92 oveq1d 
 |-  ( J = ( N - 1 ) -> ( ( x + ( J + 1 ) ) - N ) = ( ( x + ( ( N - 1 ) + 1 ) ) - N ) )
100 93 oveq1d 
 |-  ( ph -> ( ( x + ( ( N - 1 ) + 1 ) ) - N ) = ( ( x + N ) - N ) )
101 99 100 sylan9eq 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( ( x + ( J + 1 ) ) - N ) = ( ( x + N ) - N ) )
102 101 fveq2d 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( P ` ( ( x + ( J + 1 ) ) - N ) ) = ( P ` ( ( x + N ) - N ) ) )
103 98 102 eqtrid 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( P ` ( ( x + K ) - N ) ) = ( P ` ( ( x + N ) - N ) ) )
104 89 96 103 ifbieq12d 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) = if ( x <_ 0 , ( P ` ( x + N ) ) , ( P ` ( ( x + N ) - N ) ) ) )
105 104 mpteq2dv 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) = ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ 0 , ( P ` ( x + N ) ) , ( P ` ( ( x + N ) - N ) ) ) ) )
106 4 25 syl 
 |-  ( ph -> F ( Walks ` G ) P )
107 1 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )
108 ffn 
 |-  ( P : ( 0 ... ( # ` F ) ) --> V -> P Fn ( 0 ... ( # ` F ) ) )
109 106 107 108 3syl 
 |-  ( ph -> P Fn ( 0 ... ( # ` F ) ) )
110 109 adantl 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> P Fn ( 0 ... ( # ` F ) ) )
111 dffn5 
 |-  ( P Fn ( 0 ... ( # ` F ) ) <-> P = ( x e. ( 0 ... ( # ` F ) ) |-> ( P ` x ) ) )
112 110 111 sylib 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> P = ( x e. ( 0 ... ( # ` F ) ) |-> ( P ` x ) ) )
113 81 105 112 3eqtr4d 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) = P )
114 12 34 113 3brtr4d 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( F cyclShift K ) ( EulerPaths ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) )
115 4 adantl 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> F ( Circuits ` G ) P )
116 115 34 113 3brtr4d 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( F cyclShift K ) ( Circuits ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) )
117 elfzolt3 
 |-  ( J e. ( 0 ..^ N ) -> 0 < N )
118 7 117 syl 
 |-  ( ph -> 0 < N )
119 elfzoelz 
 |-  ( J e. ( 0 ..^ N ) -> J e. ZZ )
120 7 119 syl 
 |-  ( ph -> J e. ZZ )
121 120 peano2zd 
 |-  ( ph -> ( J + 1 ) e. ZZ )
122 9 121 eqeltrid 
 |-  ( ph -> K e. ZZ )
123 cshwlen 
 |-  ( ( F e. Word dom I /\ K e. ZZ ) -> ( # ` ( F cyclShift K ) ) = ( # ` F ) )
124 123 eqcomd 
 |-  ( ( F e. Word dom I /\ K e. ZZ ) -> ( # ` F ) = ( # ` ( F cyclShift K ) ) )
125 28 122 124 syl2anc 
 |-  ( ph -> ( # ` F ) = ( # ` ( F cyclShift K ) ) )
126 6 125 eqtrd 
 |-  ( ph -> N = ( # ` ( F cyclShift K ) ) )
127 118 126 breqtrd 
 |-  ( ph -> 0 < ( # ` ( F cyclShift K ) ) )
128 127 adantl 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> 0 < ( # ` ( F cyclShift K ) ) )
129 126 adantl 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> N = ( # ` ( F cyclShift K ) ) )
130 129 oveq1d 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( N - 1 ) = ( ( # ` ( F cyclShift K ) ) - 1 ) )
131 8 adantl 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( iEdg ` S ) = ( I |` ( F " ( ( 0 ..^ N ) \ { J } ) ) ) )
132 28 6 7 3jca 
 |-  ( ph -> ( F e. Word dom I /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) )
133 132 adantl 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( F e. Word dom I /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) )
134 cshimadifsn0 
 |-  ( ( F e. Word dom I /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) -> ( F " ( ( 0 ..^ N ) \ { J } ) ) = ( ( F cyclShift ( J + 1 ) ) " ( 0 ..^ ( N - 1 ) ) ) )
135 133 134 syl 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( F " ( ( 0 ..^ N ) \ { J } ) ) = ( ( F cyclShift ( J + 1 ) ) " ( 0 ..^ ( N - 1 ) ) ) )
136 14 imaeq1i 
 |-  ( ( F cyclShift ( J + 1 ) ) " ( 0 ..^ ( N - 1 ) ) ) = ( ( F cyclShift K ) " ( 0 ..^ ( N - 1 ) ) )
137 135 136 eqtrdi 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( F " ( ( 0 ..^ N ) \ { J } ) ) = ( ( F cyclShift K ) " ( 0 ..^ ( N - 1 ) ) ) )
138 137 reseq2d 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( I |` ( F " ( ( 0 ..^ N ) \ { J } ) ) ) = ( I |` ( ( F cyclShift K ) " ( 0 ..^ ( N - 1 ) ) ) ) )
139 131 138 eqtrd 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( iEdg ` S ) = ( I |` ( ( F cyclShift K ) " ( 0 ..^ ( N - 1 ) ) ) ) )
140 eqid 
 |-  ( ( F cyclShift K ) prefix ( N - 1 ) ) = ( ( F cyclShift K ) prefix ( N - 1 ) )
141 eqid 
 |-  ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) |` ( 0 ... ( N - 1 ) ) ) = ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) |` ( 0 ... ( N - 1 ) ) )
142 1 2 114 116 5 128 130 139 140 141 eucrct2eupth1 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> ( ( F cyclShift K ) prefix ( N - 1 ) ) ( EulerPaths ` S ) ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) |` ( 0 ... ( N - 1 ) ) ) )
143 10 a1i 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> H = ( ( F cyclShift K ) prefix ( N - 1 ) ) )
144 fzossfz 
 |-  ( 0 ..^ N ) C_ ( 0 ... N )
145 6 oveq2d 
 |-  ( ph -> ( 0 ... N ) = ( 0 ... ( # ` F ) ) )
146 144 145 sseqtrid 
 |-  ( ph -> ( 0 ..^ N ) C_ ( 0 ... ( # ` F ) ) )
147 146 resmptd 
 |-  ( ph -> ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) |` ( 0 ..^ N ) ) = ( x e. ( 0 ..^ N ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) )
148 elfzoel2 
 |-  ( J e. ( 0 ..^ N ) -> N e. ZZ )
149 fzoval 
 |-  ( N e. ZZ -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
150 7 148 149 3syl 
 |-  ( ph -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
151 150 reseq2d 
 |-  ( ph -> ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) |` ( 0 ..^ N ) ) = ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) |` ( 0 ... ( N - 1 ) ) ) )
152 147 151 eqtr3d 
 |-  ( ph -> ( x e. ( 0 ..^ N ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) = ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) |` ( 0 ... ( N - 1 ) ) ) )
153 11 152 eqtrid 
 |-  ( ph -> Q = ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) |` ( 0 ... ( N - 1 ) ) ) )
154 153 adantl 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> Q = ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) |` ( 0 ... ( N - 1 ) ) ) )
155 142 143 154 3brtr4d 
 |-  ( ( J = ( N - 1 ) /\ ph ) -> H ( EulerPaths ` S ) Q )
156 4 adantl 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> F ( Circuits ` G ) P )
157 peano2nn0 
 |-  ( J e. NN0 -> ( J + 1 ) e. NN0 )
158 157 3ad2ant1 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( J + 1 ) e. NN0 )
159 158 adantr 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ -. J = ( N - 1 ) ) -> ( J + 1 ) e. NN0 )
160 simpl2 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ -. J = ( N - 1 ) ) -> N e. NN )
161 1cnd 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> 1 e. CC )
162 nn0cn 
 |-  ( J e. NN0 -> J e. CC )
163 162 3ad2ant1 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> J e. CC )
164 18 161 163 subadd2d 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( ( N - 1 ) = J <-> ( J + 1 ) = N ) )
165 eqcom 
 |-  ( J = ( N - 1 ) <-> ( N - 1 ) = J )
166 eqcom 
 |-  ( N = ( J + 1 ) <-> ( J + 1 ) = N )
167 164 165 166 3bitr4g 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( J = ( N - 1 ) <-> N = ( J + 1 ) ) )
168 167 necon3bbid 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( -. J = ( N - 1 ) <-> N =/= ( J + 1 ) ) )
169 157 nn0red 
 |-  ( J e. NN0 -> ( J + 1 ) e. RR )
170 169 3ad2ant1 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( J + 1 ) e. RR )
171 nnre 
 |-  ( N e. NN -> N e. RR )
172 171 3ad2ant2 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> N e. RR )
173 nn0z 
 |-  ( J e. NN0 -> J e. ZZ )
174 nnz 
 |-  ( N e. NN -> N e. ZZ )
175 zltp1le 
 |-  ( ( J e. ZZ /\ N e. ZZ ) -> ( J < N <-> ( J + 1 ) <_ N ) )
176 173 174 175 syl2an 
 |-  ( ( J e. NN0 /\ N e. NN ) -> ( J < N <-> ( J + 1 ) <_ N ) )
177 176 biimp3a 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( J + 1 ) <_ N )
178 170 172 177 leltned 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( ( J + 1 ) < N <-> N =/= ( J + 1 ) ) )
179 178 biimprd 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( N =/= ( J + 1 ) -> ( J + 1 ) < N ) )
180 168 179 sylbid 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( -. J = ( N - 1 ) -> ( J + 1 ) < N ) )
181 180 imp 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ -. J = ( N - 1 ) ) -> ( J + 1 ) < N )
182 159 160 181 3jca 
 |-  ( ( ( J e. NN0 /\ N e. NN /\ J < N ) /\ -. J = ( N - 1 ) ) -> ( ( J + 1 ) e. NN0 /\ N e. NN /\ ( J + 1 ) < N ) )
183 182 ex 
 |-  ( ( J e. NN0 /\ N e. NN /\ J < N ) -> ( -. J = ( N - 1 ) -> ( ( J + 1 ) e. NN0 /\ N e. NN /\ ( J + 1 ) < N ) ) )
184 16 183 sylbi 
 |-  ( J e. ( 0 ..^ N ) -> ( -. J = ( N - 1 ) -> ( ( J + 1 ) e. NN0 /\ N e. NN /\ ( J + 1 ) < N ) ) )
185 elfzo0 
 |-  ( ( J + 1 ) e. ( 0 ..^ N ) <-> ( ( J + 1 ) e. NN0 /\ N e. NN /\ ( J + 1 ) < N ) )
186 184 185 imbitrrdi 
 |-  ( J e. ( 0 ..^ N ) -> ( -. J = ( N - 1 ) -> ( J + 1 ) e. ( 0 ..^ N ) ) )
187 7 186 syl 
 |-  ( ph -> ( -. J = ( N - 1 ) -> ( J + 1 ) e. ( 0 ..^ N ) ) )
188 187 impcom 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( J + 1 ) e. ( 0 ..^ N ) )
189 9 a1i 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> K = ( J + 1 ) )
190 6 eqcomd 
 |-  ( ph -> ( # ` F ) = N )
191 190 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ N ) )
192 191 adantl 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( 0 ..^ ( # ` F ) ) = ( 0 ..^ N ) )
193 188 189 192 3eltr4d 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> K e. ( 0 ..^ ( # ` F ) ) )
194 eqid 
 |-  ( F cyclShift K ) = ( F cyclShift K )
195 eqid 
 |-  ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) = ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) )
196 3 adantl 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> F ( EulerPaths ` G ) P )
197 1 2 156 35 193 194 195 196 eucrctshift 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( ( F cyclShift K ) ( EulerPaths ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) /\ ( F cyclShift K ) ( Circuits ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) ) )
198 simprl 
 |-  ( ( ( -. J = ( N - 1 ) /\ ph ) /\ ( ( F cyclShift K ) ( EulerPaths ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) /\ ( F cyclShift K ) ( Circuits ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) ) ) -> ( F cyclShift K ) ( EulerPaths ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) )
199 simprr 
 |-  ( ( ( -. J = ( N - 1 ) /\ ph ) /\ ( ( F cyclShift K ) ( EulerPaths ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) /\ ( F cyclShift K ) ( Circuits ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) ) ) -> ( F cyclShift K ) ( Circuits ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) )
200 127 ad2antlr 
 |-  ( ( ( -. J = ( N - 1 ) /\ ph ) /\ ( ( F cyclShift K ) ( EulerPaths ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) /\ ( F cyclShift K ) ( Circuits ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) ) ) -> 0 < ( # ` ( F cyclShift K ) ) )
201 126 oveq1d 
 |-  ( ph -> ( N - 1 ) = ( ( # ` ( F cyclShift K ) ) - 1 ) )
202 201 ad2antlr 
 |-  ( ( ( -. J = ( N - 1 ) /\ ph ) /\ ( ( F cyclShift K ) ( EulerPaths ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) /\ ( F cyclShift K ) ( Circuits ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) ) ) -> ( N - 1 ) = ( ( # ` ( F cyclShift K ) ) - 1 ) )
203 8 adantl 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( iEdg ` S ) = ( I |` ( F " ( ( 0 ..^ N ) \ { J } ) ) ) )
204 132 adantl 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( F e. Word dom I /\ N = ( # ` F ) /\ J e. ( 0 ..^ N ) ) )
205 204 134 syl 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( F " ( ( 0 ..^ N ) \ { J } ) ) = ( ( F cyclShift ( J + 1 ) ) " ( 0 ..^ ( N - 1 ) ) ) )
206 205 136 eqtrdi 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( F " ( ( 0 ..^ N ) \ { J } ) ) = ( ( F cyclShift K ) " ( 0 ..^ ( N - 1 ) ) ) )
207 206 reseq2d 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( I |` ( F " ( ( 0 ..^ N ) \ { J } ) ) ) = ( I |` ( ( F cyclShift K ) " ( 0 ..^ ( N - 1 ) ) ) ) )
208 203 207 eqtrd 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( iEdg ` S ) = ( I |` ( ( F cyclShift K ) " ( 0 ..^ ( N - 1 ) ) ) ) )
209 208 adantr 
 |-  ( ( ( -. J = ( N - 1 ) /\ ph ) /\ ( ( F cyclShift K ) ( EulerPaths ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) /\ ( F cyclShift K ) ( Circuits ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) ) ) -> ( iEdg ` S ) = ( I |` ( ( F cyclShift K ) " ( 0 ..^ ( N - 1 ) ) ) ) )
210 eqid 
 |-  ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) |` ( 0 ... ( N - 1 ) ) ) = ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) |` ( 0 ... ( N - 1 ) ) )
211 1 2 198 199 5 200 202 209 140 210 eucrct2eupth1 
 |-  ( ( ( -. J = ( N - 1 ) /\ ph ) /\ ( ( F cyclShift K ) ( EulerPaths ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) /\ ( F cyclShift K ) ( Circuits ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) ) ) -> ( ( F cyclShift K ) prefix ( N - 1 ) ) ( EulerPaths ` S ) ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) |` ( 0 ... ( N - 1 ) ) ) )
212 10 a1i 
 |-  ( ( ( -. J = ( N - 1 ) /\ ph ) /\ ( ( F cyclShift K ) ( EulerPaths ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) /\ ( F cyclShift K ) ( Circuits ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) ) ) -> H = ( ( F cyclShift K ) prefix ( N - 1 ) ) )
213 190 oveq1d 
 |-  ( ph -> ( ( # ` F ) - K ) = ( N - K ) )
214 213 breq2d 
 |-  ( ph -> ( x <_ ( ( # ` F ) - K ) <-> x <_ ( N - K ) ) )
215 214 adantl 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( x <_ ( ( # ` F ) - K ) <-> x <_ ( N - K ) ) )
216 190 oveq2d 
 |-  ( ph -> ( ( x + K ) - ( # ` F ) ) = ( ( x + K ) - N ) )
217 216 fveq2d 
 |-  ( ph -> ( P ` ( ( x + K ) - ( # ` F ) ) ) = ( P ` ( ( x + K ) - N ) ) )
218 217 adantl 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( P ` ( ( x + K ) - ( # ` F ) ) ) = ( P ` ( ( x + K ) - N ) ) )
219 215 218 ifbieq2d 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) = if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) )
220 219 mpteq2dv 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) = ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) )
221 150 eqcomd 
 |-  ( ph -> ( 0 ... ( N - 1 ) ) = ( 0 ..^ N ) )
222 221 adantl 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( 0 ... ( N - 1 ) ) = ( 0 ..^ N ) )
223 220 222 reseq12d 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) |` ( 0 ... ( N - 1 ) ) ) = ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) |` ( 0 ..^ N ) ) )
224 6 adantl 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> N = ( # ` F ) )
225 224 oveq2d 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( 0 ... N ) = ( 0 ... ( # ` F ) ) )
226 144 225 sseqtrid 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( 0 ..^ N ) C_ ( 0 ... ( # ` F ) ) )
227 226 resmptd 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) |` ( 0 ..^ N ) ) = ( x e. ( 0 ..^ N ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) )
228 223 227 eqtrd 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) |` ( 0 ... ( N - 1 ) ) ) = ( x e. ( 0 ..^ N ) |-> if ( x <_ ( N - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - N ) ) ) ) )
229 11 228 eqtr4id 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> Q = ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) |` ( 0 ... ( N - 1 ) ) ) )
230 229 adantr 
 |-  ( ( ( -. J = ( N - 1 ) /\ ph ) /\ ( ( F cyclShift K ) ( EulerPaths ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) /\ ( F cyclShift K ) ( Circuits ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) ) ) -> Q = ( ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) |` ( 0 ... ( N - 1 ) ) ) )
231 211 212 230 3brtr4d 
 |-  ( ( ( -. J = ( N - 1 ) /\ ph ) /\ ( ( F cyclShift K ) ( EulerPaths ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) /\ ( F cyclShift K ) ( Circuits ` G ) ( x e. ( 0 ... ( # ` F ) ) |-> if ( x <_ ( ( # ` F ) - K ) , ( P ` ( x + K ) ) , ( P ` ( ( x + K ) - ( # ` F ) ) ) ) ) ) ) -> H ( EulerPaths ` S ) Q )
232 197 231 mpdan 
 |-  ( ( -. J = ( N - 1 ) /\ ph ) -> H ( EulerPaths ` S ) Q )
233 155 232 pm2.61ian 
 |-  ( ph -> H ( EulerPaths ` S ) Q )