Metamath Proof Explorer

Theorem eucrctshift

Description: Cyclically shifting the indices of an Eulerian circuit <. F , P >. results in an Eulerian circuit <. H , Q >. . (Contributed by AV, 15-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 eucrctshift.v 
 |-  V = ( Vtx ` G )
2 eucrctshift.i 
 |-  I = ( iEdg ` G )
3 eucrctshift.c 
 |-  ( ph -> F ( Circuits ` G ) P )
4 eucrctshift.n 
 |-  N = ( # ` F )
5 eucrctshift.s 
 |-  ( ph -> S e. ( 0 ..^ N ) )
6 eucrctshift.h 
 |-  H = ( F cyclShift S )
7 eucrctshift.q 
 |-  Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
8 eucrctshift.e 
 |-  ( ph -> F ( EulerPaths ` G ) P )
9 1 2 3 4 5 6 7 crctcshtrl 
 |-  ( ph -> H ( Trails ` G ) Q )
10 simpr 
 |-  ( ( ph /\ H ( Trails ` G ) Q ) -> H ( Trails ` G ) Q )
11 2 eupthf1o 
 |-  ( F ( EulerPaths ` G ) P -> F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I )
12 8 11 syl 
 |-  ( ph -> F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I )
13 12 adantr 
 |-  ( ( ph /\ H ( Trails ` G ) Q ) -> F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I )
14 trliswlk 
 |-  ( H ( Trails ` G ) Q -> H ( Walks ` G ) Q )
15 2 wlkf 
 |-  ( H ( Walks ` G ) Q -> H e. Word dom I )
16 wrdf 
 |-  ( H e. Word dom I -> H : ( 0 ..^ ( # ` H ) ) --> dom I )
17 14 15 16 3syl 
 |-  ( H ( Trails ` G ) Q -> H : ( 0 ..^ ( # ` H ) ) --> dom I )
18 df-f1o 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I <-> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I /\ F : ( 0 ..^ ( # ` F ) ) -onto-> dom I ) )
19 dffo3 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -onto-> dom I <-> ( F : ( 0 ..^ ( # ` F ) ) --> dom I /\ A. i e. dom I E. y e. ( 0 ..^ ( # ` F ) ) i = ( F ` y ) ) )
20 crctiswlk 
 |-  ( F ( Circuits ` G ) P -> F ( Walks ` G ) P )
21 2 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
22 lencl 
 |-  ( F e. Word dom I -> ( # ` F ) e. NN0 )
23 4 oveq2i 
 |-  ( 0 ..^ N ) = ( 0 ..^ ( # ` F ) )
24 23 eleq2i 
 |-  ( S e. ( 0 ..^ N ) <-> S e. ( 0 ..^ ( # ` F ) ) )
25 elfzonn0 
 |-  ( S e. ( 0 ..^ ( # ` F ) ) -> S e. NN0 )
26 25 adantl 
 |-  ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) -> S e. NN0 )
27 elfzonn0 
 |-  ( y e. ( 0 ..^ ( # ` F ) ) -> y e. NN0 )
28 nn0sub 
 |-  ( ( S e. NN0 /\ y e. NN0 ) -> ( S <_ y <-> ( y - S ) e. NN0 ) )
29 26 27 28 syl2an 
 |-  ( ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) -> ( S <_ y <-> ( y - S ) e. NN0 ) )
30 29 biimpac 
 |-  ( ( S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( y - S ) e. NN0 )
31 elfzo0 
 |-  ( y e. ( 0 ..^ ( # ` F ) ) <-> ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) )
32 simp2 
 |-  ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) -> ( # ` F ) e. NN )
33 31 32 sylbi 
 |-  ( y e. ( 0 ..^ ( # ` F ) ) -> ( # ` F ) e. NN )
34 33 ad2antll 
 |-  ( ( S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( # ` F ) e. NN )
35 nn0re 
 |-  ( y e. NN0 -> y e. RR )
36 35 ad2antrr 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN ) /\ S e. ( 0 ..^ ( # ` F ) ) ) -> y e. RR )
37 nnre 
 |-  ( ( # ` F ) e. NN -> ( # ` F ) e. RR )
38 37 adantl 
 |-  ( ( y e. NN0 /\ ( # ` F ) e. NN ) -> ( # ` F ) e. RR )
39 38 adantr 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN ) /\ S e. ( 0 ..^ ( # ` F ) ) ) -> ( # ` F ) e. RR )
40 elfzoelz 
 |-  ( S e. ( 0 ..^ ( # ` F ) ) -> S e. ZZ )
41 40 zred 
 |-  ( S e. ( 0 ..^ ( # ` F ) ) -> S e. RR )
42 readdcl 
 |-  ( ( ( # ` F ) e. RR /\ S e. RR ) -> ( ( # ` F ) + S ) e. RR )
43 38 41 42 syl2an 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN ) /\ S e. ( 0 ..^ ( # ` F ) ) ) -> ( ( # ` F ) + S ) e. RR )
44 36 39 43 3jca 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN ) /\ S e. ( 0 ..^ ( # ` F ) ) ) -> ( y e. RR /\ ( # ` F ) e. RR /\ ( ( # ` F ) + S ) e. RR ) )
45 elfzole1 
 |-  ( S e. ( 0 ..^ ( # ` F ) ) -> 0 <_ S )
46 45 adantl 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN ) /\ S e. ( 0 ..^ ( # ` F ) ) ) -> 0 <_ S )
47 addge01 
 |-  ( ( ( # ` F ) e. RR /\ S e. RR ) -> ( 0 <_ S <-> ( # ` F ) <_ ( ( # ` F ) + S ) ) )
48 38 41 47 syl2an 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN ) /\ S e. ( 0 ..^ ( # ` F ) ) ) -> ( 0 <_ S <-> ( # ` F ) <_ ( ( # ` F ) + S ) ) )
49 46 48 mpbid 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN ) /\ S e. ( 0 ..^ ( # ` F ) ) ) -> ( # ` F ) <_ ( ( # ` F ) + S ) )
50 44 49 lelttrdi 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN ) /\ S e. ( 0 ..^ ( # ` F ) ) ) -> ( y < ( # ` F ) -> y < ( ( # ` F ) + S ) ) )
51 50 ex 
 |-  ( ( y e. NN0 /\ ( # ` F ) e. NN ) -> ( S e. ( 0 ..^ ( # ` F ) ) -> ( y < ( # ` F ) -> y < ( ( # ` F ) + S ) ) ) )
52 51 com23 
 |-  ( ( y e. NN0 /\ ( # ` F ) e. NN ) -> ( y < ( # ` F ) -> ( S e. ( 0 ..^ ( # ` F ) ) -> y < ( ( # ` F ) + S ) ) ) )
53 52 3impia 
 |-  ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) -> ( S e. ( 0 ..^ ( # ` F ) ) -> y < ( ( # ` F ) + S ) ) )
54 53 adantld 
 |-  ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) -> ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) -> y < ( ( # ` F ) + S ) ) )
55 54 imp 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) /\ ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) ) -> y < ( ( # ` F ) + S ) )
56 35 3ad2ant1 
 |-  ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) -> y e. RR )
57 56 adantr 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) /\ ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) ) -> y e. RR )
58 41 ad2antll 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) /\ ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) ) -> S e. RR )
59 elfzoel2 
 |-  ( S e. ( 0 ..^ ( # ` F ) ) -> ( # ` F ) e. ZZ )
60 59 zred 
 |-  ( S e. ( 0 ..^ ( # ` F ) ) -> ( # ` F ) e. RR )
61 60 ad2antll 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) /\ ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) ) -> ( # ` F ) e. RR )
62 57 58 61 ltsubaddd 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) /\ ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( y - S ) < ( # ` F ) <-> y < ( ( # ` F ) + S ) ) )
63 55 62 mpbird 
 |-  ( ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) /\ ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) ) -> ( y - S ) < ( # ` F ) )
64 63 ex 
 |-  ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) -> ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) -> ( y - S ) < ( # ` F ) ) )
65 31 64 sylbi 
 |-  ( y e. ( 0 ..^ ( # ` F ) ) -> ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) -> ( y - S ) < ( # ` F ) ) )
66 65 impcom 
 |-  ( ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) -> ( y - S ) < ( # ` F ) )
67 66 adantl 
 |-  ( ( S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( y - S ) < ( # ` F ) )
68 elfzo0 
 |-  ( ( y - S ) e. ( 0 ..^ ( # ` F ) ) <-> ( ( y - S ) e. NN0 /\ ( # ` F ) e. NN /\ ( y - S ) < ( # ` F ) ) )
69 30 34 67 68 syl3anbrc 
 |-  ( ( S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( y - S ) e. ( 0 ..^ ( # ` F ) ) )
70 oveq1 
 |-  ( z = ( y - S ) -> ( z + S ) = ( ( y - S ) + S ) )
71 70 oveq1d 
 |-  ( z = ( y - S ) -> ( ( z + S ) mod ( # ` F ) ) = ( ( ( y - S ) + S ) mod ( # ` F ) ) )
72 40 zcnd 
 |-  ( S e. ( 0 ..^ ( # ` F ) ) -> S e. CC )
73 72 adantl 
 |-  ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) -> S e. CC )
74 elfzoelz 
 |-  ( y e. ( 0 ..^ ( # ` F ) ) -> y e. ZZ )
75 74 zcnd 
 |-  ( y e. ( 0 ..^ ( # ` F ) ) -> y e. CC )
76 73 75 anim12ci 
 |-  ( ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) -> ( y e. CC /\ S e. CC ) )
77 76 adantl 
 |-  ( ( S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( y e. CC /\ S e. CC ) )
78 npcan 
 |-  ( ( y e. CC /\ S e. CC ) -> ( ( y - S ) + S ) = y )
79 77 78 syl 
 |-  ( ( S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( y - S ) + S ) = y )
80 79 oveq1d 
 |-  ( ( S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( ( y - S ) + S ) mod ( # ` F ) ) = ( y mod ( # ` F ) ) )
81 zmodidfzoimp 
 |-  ( y e. ( 0 ..^ ( # ` F ) ) -> ( y mod ( # ` F ) ) = y )
82 81 ad2antll 
 |-  ( ( S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( y mod ( # ` F ) ) = y )
83 80 82 eqtrd 
 |-  ( ( S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( ( y - S ) + S ) mod ( # ` F ) ) = y )
84 71 83 sylan9eqr 
 |-  ( ( ( S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) /\ z = ( y - S ) ) -> ( ( z + S ) mod ( # ` F ) ) = y )
85 84 eqcomd 
 |-  ( ( ( S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) /\ z = ( y - S ) ) -> y = ( ( z + S ) mod ( # ` F ) ) )
86 69 85 rspcedeq2vd 
 |-  ( ( S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> E. z e. ( 0 ..^ ( # ` F ) ) y = ( ( z + S ) mod ( # ` F ) ) )
87 elfzo0 
 |-  ( S e. ( 0 ..^ ( # ` F ) ) <-> ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) )
88 nn0cn 
 |-  ( y e. NN0 -> y e. CC )
89 88 ad2antrr 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> y e. CC )
90 nn0cn 
 |-  ( S e. NN0 -> S e. CC )
91 90 3ad2ant1 
 |-  ( ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) -> S e. CC )
92 91 adantl 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> S e. CC )
93 nncn 
 |-  ( ( # ` F ) e. NN -> ( # ` F ) e. CC )
94 93 3ad2ant2 
 |-  ( ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) -> ( # ` F ) e. CC )
95 94 adantl 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> ( # ` F ) e. CC )
96 89 92 95 subadd23d 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> ( ( y - S ) + ( # ` F ) ) = ( y + ( ( # ` F ) - S ) ) )
97 simpll 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> y e. NN0 )
98 nn0z 
 |-  ( S e. NN0 -> S e. ZZ )
99 nnz 
 |-  ( ( # ` F ) e. NN -> ( # ` F ) e. ZZ )
100 znnsub 
 |-  ( ( S e. ZZ /\ ( # ` F ) e. ZZ ) -> ( S < ( # ` F ) <-> ( ( # ` F ) - S ) e. NN ) )
101 98 99 100 syl2an 
 |-  ( ( S e. NN0 /\ ( # ` F ) e. NN ) -> ( S < ( # ` F ) <-> ( ( # ` F ) - S ) e. NN ) )
102 101 biimp3a 
 |-  ( ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) -> ( ( # ` F ) - S ) e. NN )
103 102 adantl 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> ( ( # ` F ) - S ) e. NN )
104 103 nnnn0d 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> ( ( # ` F ) - S ) e. NN0 )
105 97 104 nn0addcld 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> ( y + ( ( # ` F ) - S ) ) e. NN0 )
106 96 105 eqeltrd 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> ( ( y - S ) + ( # ` F ) ) e. NN0 )
107 106 adantr 
 |-  ( ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) /\ -. S <_ y ) -> ( ( y - S ) + ( # ` F ) ) e. NN0 )
108 simplr2 
 |-  ( ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) /\ -. S <_ y ) -> ( # ` F ) e. NN )
109 88 adantr 
 |-  ( ( y e. NN0 /\ y < ( # ` F ) ) -> y e. CC )
110 subcl 
 |-  ( ( y e. CC /\ S e. CC ) -> ( y - S ) e. CC )
111 109 91 110 syl2an 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> ( y - S ) e. CC )
112 95 111 jca 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> ( ( # ` F ) e. CC /\ ( y - S ) e. CC ) )
113 112 adantr 
 |-  ( ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) /\ -. S <_ y ) -> ( ( # ` F ) e. CC /\ ( y - S ) e. CC ) )
114 addcom 
 |-  ( ( ( # ` F ) e. CC /\ ( y - S ) e. CC ) -> ( ( # ` F ) + ( y - S ) ) = ( ( y - S ) + ( # ` F ) ) )
115 113 114 syl 
 |-  ( ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) /\ -. S <_ y ) -> ( ( # ` F ) + ( y - S ) ) = ( ( y - S ) + ( # ` F ) ) )
116 35 adantr 
 |-  ( ( y e. NN0 /\ y < ( # ` F ) ) -> y e. RR )
117 nn0re 
 |-  ( S e. NN0 -> S e. RR )
118 117 3ad2ant1 
 |-  ( ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) -> S e. RR )
119 ltnle 
 |-  ( ( y e. RR /\ S e. RR ) -> ( y < S <-> -. S <_ y ) )
120 simpl 
 |-  ( ( y e. RR /\ S e. RR ) -> y e. RR )
121 simpr 
 |-  ( ( y e. RR /\ S e. RR ) -> S e. RR )
122 120 121 sublt0d 
 |-  ( ( y e. RR /\ S e. RR ) -> ( ( y - S ) < 0 <-> y < S ) )
123 122 biimprd 
 |-  ( ( y e. RR /\ S e. RR ) -> ( y < S -> ( y - S ) < 0 ) )
124 119 123 sylbird 
 |-  ( ( y e. RR /\ S e. RR ) -> ( -. S <_ y -> ( y - S ) < 0 ) )
125 116 118 124 syl2an 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> ( -. S <_ y -> ( y - S ) < 0 ) )
126 125 imp 
 |-  ( ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) /\ -. S <_ y ) -> ( y - S ) < 0 )
127 resubcl 
 |-  ( ( y e. RR /\ S e. RR ) -> ( y - S ) e. RR )
128 116 118 127 syl2an 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> ( y - S ) e. RR )
129 37 3ad2ant2 
 |-  ( ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) -> ( # ` F ) e. RR )
130 129 adantl 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> ( # ` F ) e. RR )
131 128 130 jca 
 |-  ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) -> ( ( y - S ) e. RR /\ ( # ` F ) e. RR ) )
132 131 adantr 
 |-  ( ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) /\ -. S <_ y ) -> ( ( y - S ) e. RR /\ ( # ` F ) e. RR ) )
133 ltaddneg 
 |-  ( ( ( y - S ) e. RR /\ ( # ` F ) e. RR ) -> ( ( y - S ) < 0 <-> ( ( # ` F ) + ( y - S ) ) < ( # ` F ) ) )
134 132 133 syl 
 |-  ( ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) /\ -. S <_ y ) -> ( ( y - S ) < 0 <-> ( ( # ` F ) + ( y - S ) ) < ( # ` F ) ) )
135 126 134 mpbid 
 |-  ( ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) /\ -. S <_ y ) -> ( ( # ` F ) + ( y - S ) ) < ( # ` F ) )
136 115 135 eqbrtrrd 
 |-  ( ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) /\ -. S <_ y ) -> ( ( y - S ) + ( # ` F ) ) < ( # ` F ) )
137 107 108 136 3jca 
 |-  ( ( ( ( y e. NN0 /\ y < ( # ` F ) ) /\ ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) ) /\ -. S <_ y ) -> ( ( ( y - S ) + ( # ` F ) ) e. NN0 /\ ( # ` F ) e. NN /\ ( ( y - S ) + ( # ` F ) ) < ( # ` F ) ) )
138 137 exp31 
 |-  ( ( y e. NN0 /\ y < ( # ` F ) ) -> ( ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) -> ( -. S <_ y -> ( ( ( y - S ) + ( # ` F ) ) e. NN0 /\ ( # ` F ) e. NN /\ ( ( y - S ) + ( # ` F ) ) < ( # ` F ) ) ) ) )
139 138 3adant2 
 |-  ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) -> ( ( S e. NN0 /\ ( # ` F ) e. NN /\ S < ( # ` F ) ) -> ( -. S <_ y -> ( ( ( y - S ) + ( # ` F ) ) e. NN0 /\ ( # ` F ) e. NN /\ ( ( y - S ) + ( # ` F ) ) < ( # ` F ) ) ) ) )
140 87 139 syl5bi 
 |-  ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) -> ( S e. ( 0 ..^ ( # ` F ) ) -> ( -. S <_ y -> ( ( ( y - S ) + ( # ` F ) ) e. NN0 /\ ( # ` F ) e. NN /\ ( ( y - S ) + ( # ` F ) ) < ( # ` F ) ) ) ) )
141 140 adantld 
 |-  ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) -> ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) -> ( -. S <_ y -> ( ( ( y - S ) + ( # ` F ) ) e. NN0 /\ ( # ` F ) e. NN /\ ( ( y - S ) + ( # ` F ) ) < ( # ` F ) ) ) ) )
142 31 141 sylbi 
 |-  ( y e. ( 0 ..^ ( # ` F ) ) -> ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) -> ( -. S <_ y -> ( ( ( y - S ) + ( # ` F ) ) e. NN0 /\ ( # ` F ) e. NN /\ ( ( y - S ) + ( # ` F ) ) < ( # ` F ) ) ) ) )
143 142 impcom 
 |-  ( ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) -> ( -. S <_ y -> ( ( ( y - S ) + ( # ` F ) ) e. NN0 /\ ( # ` F ) e. NN /\ ( ( y - S ) + ( # ` F ) ) < ( # ` F ) ) ) )
144 143 impcom 
 |-  ( ( -. S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( ( y - S ) + ( # ` F ) ) e. NN0 /\ ( # ` F ) e. NN /\ ( ( y - S ) + ( # ` F ) ) < ( # ` F ) ) )
145 elfzo0 
 |-  ( ( ( y - S ) + ( # ` F ) ) e. ( 0 ..^ ( # ` F ) ) <-> ( ( ( y - S ) + ( # ` F ) ) e. NN0 /\ ( # ` F ) e. NN /\ ( ( y - S ) + ( # ` F ) ) < ( # ` F ) ) )
146 144 145 sylibr 
 |-  ( ( -. S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( y - S ) + ( # ` F ) ) e. ( 0 ..^ ( # ` F ) ) )
147 oveq1 
 |-  ( z = ( ( y - S ) + ( # ` F ) ) -> ( z + S ) = ( ( ( y - S ) + ( # ` F ) ) + S ) )
148 147 oveq1d 
 |-  ( z = ( ( y - S ) + ( # ` F ) ) -> ( ( z + S ) mod ( # ` F ) ) = ( ( ( ( y - S ) + ( # ` F ) ) + S ) mod ( # ` F ) ) )
149 73 adantr 
 |-  ( ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) -> S e. CC )
150 75 adantl 
 |-  ( ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) -> y e. CC )
151 nn0cn 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. CC )
152 151 ad2antrr 
 |-  ( ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) -> ( # ` F ) e. CC )
153 149 150 152 3jca 
 |-  ( ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) -> ( S e. CC /\ y e. CC /\ ( # ` F ) e. CC ) )
154 153 adantl 
 |-  ( ( -. S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( S e. CC /\ y e. CC /\ ( # ` F ) e. CC ) )
155 simp2 
 |-  ( ( S e. CC /\ y e. CC /\ ( # ` F ) e. CC ) -> y e. CC )
156 simp3 
 |-  ( ( S e. CC /\ y e. CC /\ ( # ` F ) e. CC ) -> ( # ` F ) e. CC )
157 simp1 
 |-  ( ( S e. CC /\ y e. CC /\ ( # ` F ) e. CC ) -> S e. CC )
158 155 157 156 nppcand 
 |-  ( ( S e. CC /\ y e. CC /\ ( # ` F ) e. CC ) -> ( ( ( y - S ) + ( # ` F ) ) + S ) = ( y + ( # ` F ) ) )
159 155 156 158 comraddd 
 |-  ( ( S e. CC /\ y e. CC /\ ( # ` F ) e. CC ) -> ( ( ( y - S ) + ( # ` F ) ) + S ) = ( ( # ` F ) + y ) )
160 154 159 syl 
 |-  ( ( -. S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( ( y - S ) + ( # ` F ) ) + S ) = ( ( # ` F ) + y ) )
161 160 oveq1d 
 |-  ( ( -. S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( ( ( y - S ) + ( # ` F ) ) + S ) mod ( # ` F ) ) = ( ( ( # ` F ) + y ) mod ( # ` F ) ) )
162 31 biimpi 
 |-  ( y e. ( 0 ..^ ( # ` F ) ) -> ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) )
163 162 ad2antll 
 |-  ( ( -. S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) )
164 addmodid 
 |-  ( ( y e. NN0 /\ ( # ` F ) e. NN /\ y < ( # ` F ) ) -> ( ( ( # ` F ) + y ) mod ( # ` F ) ) = y )
165 163 164 syl 
 |-  ( ( -. S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( ( # ` F ) + y ) mod ( # ` F ) ) = y )
166 161 165 eqtrd 
 |-  ( ( -. S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( ( ( y - S ) + ( # ` F ) ) + S ) mod ( # ` F ) ) = y )
167 148 166 sylan9eqr 
 |-  ( ( ( -. S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) /\ z = ( ( y - S ) + ( # ` F ) ) ) -> ( ( z + S ) mod ( # ` F ) ) = y )
168 167 eqcomd 
 |-  ( ( ( -. S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) /\ z = ( ( y - S ) + ( # ` F ) ) ) -> y = ( ( z + S ) mod ( # ` F ) ) )
169 146 168 rspcedeq2vd 
 |-  ( ( -. S <_ y /\ ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) ) -> E. z e. ( 0 ..^ ( # ` F ) ) y = ( ( z + S ) mod ( # ` F ) ) )
170 86 169 pm2.61ian 
 |-  ( ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) -> E. z e. ( 0 ..^ ( # ` F ) ) y = ( ( z + S ) mod ( # ` F ) ) )
171 23 rexeqi 
 |-  ( E. z e. ( 0 ..^ N ) y = ( ( z + S ) mod ( # ` F ) ) <-> E. z e. ( 0 ..^ ( # ` F ) ) y = ( ( z + S ) mod ( # ` F ) ) )
172 170 171 sylibr 
 |-  ( ( ( ( # ` F ) e. NN0 /\ S e. ( 0 ..^ ( # ` F ) ) ) /\ y e. ( 0 ..^ ( # ` F ) ) ) -> E. z e. ( 0 ..^ N ) y = ( ( z + S ) mod ( # ` F ) ) )
173 172 exp31 
 |-  ( ( # ` F ) e. NN0 -> ( S e. ( 0 ..^ ( # ` F ) ) -> ( y e. ( 0 ..^ ( # ` F ) ) -> E. z e. ( 0 ..^ N ) y = ( ( z + S ) mod ( # ` F ) ) ) ) )
174 24 173 syl5bi 
 |-  ( ( # ` F ) e. NN0 -> ( S e. ( 0 ..^ N ) -> ( y e. ( 0 ..^ ( # ` F ) ) -> E. z e. ( 0 ..^ N ) y = ( ( z + S ) mod ( # ` F ) ) ) ) )
175 22 174 syl 
 |-  ( F e. Word dom I -> ( S e. ( 0 ..^ N ) -> ( y e. ( 0 ..^ ( # ` F ) ) -> E. z e. ( 0 ..^ N ) y = ( ( z + S ) mod ( # ` F ) ) ) ) )
176 20 21 175 3syl 
 |-  ( F ( Circuits ` G ) P -> ( S e. ( 0 ..^ N ) -> ( y e. ( 0 ..^ ( # ` F ) ) -> E. z e. ( 0 ..^ N ) y = ( ( z + S ) mod ( # ` F ) ) ) ) )
177 3 5 176 sylc 
 |-  ( ph -> ( y e. ( 0 ..^ ( # ` F ) ) -> E. z e. ( 0 ..^ N ) y = ( ( z + S ) mod ( # ` F ) ) ) )
178 177 adantr 
 |-  ( ( ph /\ i e. dom I ) -> ( y e. ( 0 ..^ ( # ` F ) ) -> E. z e. ( 0 ..^ N ) y = ( ( z + S ) mod ( # ` F ) ) ) )
179 178 imp 
 |-  ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) -> E. z e. ( 0 ..^ N ) y = ( ( z + S ) mod ( # ` F ) ) )
180 179 adantr 
 |-  ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) -> E. z e. ( 0 ..^ N ) y = ( ( z + S ) mod ( # ` F ) ) )
181 fveq2 
 |-  ( y = ( ( z + S ) mod ( # ` F ) ) -> ( F ` y ) = ( F ` ( ( z + S ) mod ( # ` F ) ) ) )
182 181 reximi 
 |-  ( E. z e. ( 0 ..^ N ) y = ( ( z + S ) mod ( # ` F ) ) -> E. z e. ( 0 ..^ N ) ( F ` y ) = ( F ` ( ( z + S ) mod ( # ` F ) ) ) )
183 180 182 syl 
 |-  ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) -> E. z e. ( 0 ..^ N ) ( F ` y ) = ( F ` ( ( z + S ) mod ( # ` F ) ) ) )
184 3 20 21 3syl 
 |-  ( ph -> F e. Word dom I )
185 184 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) -> F e. Word dom I )
186 elfzoelz 
 |-  ( S e. ( 0 ..^ N ) -> S e. ZZ )
187 5 186 syl 
 |-  ( ph -> S e. ZZ )
188 187 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) -> S e. ZZ )
189 23 eleq2i 
 |-  ( z e. ( 0 ..^ N ) <-> z e. ( 0 ..^ ( # ` F ) ) )
190 189 biimpi 
 |-  ( z e. ( 0 ..^ N ) -> z e. ( 0 ..^ ( # ` F ) ) )
191 cshwidxmod 
 |-  ( ( F e. Word dom I /\ S e. ZZ /\ z e. ( 0 ..^ ( # ` F ) ) ) -> ( ( F cyclShift S ) ` z ) = ( F ` ( ( z + S ) mod ( # ` F ) ) ) )
192 185 188 190 191 syl2an3an 
 |-  ( ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) /\ z e. ( 0 ..^ N ) ) -> ( ( F cyclShift S ) ` z ) = ( F ` ( ( z + S ) mod ( # ` F ) ) ) )
193 192 eqeq2d 
 |-  ( ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) /\ z e. ( 0 ..^ N ) ) -> ( ( F ` y ) = ( ( F cyclShift S ) ` z ) <-> ( F ` y ) = ( F ` ( ( z + S ) mod ( # ` F ) ) ) ) )
194 193 rexbidva 
 |-  ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) -> ( E. z e. ( 0 ..^ N ) ( F ` y ) = ( ( F cyclShift S ) ` z ) <-> E. z e. ( 0 ..^ N ) ( F ` y ) = ( F ` ( ( z + S ) mod ( # ` F ) ) ) ) )
195 183 194 mpbird 
 |-  ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) -> E. z e. ( 0 ..^ N ) ( F ` y ) = ( ( F cyclShift S ) ` z ) )
196 1 2 3 4 5 6 crctcshlem2 
 |-  ( ph -> ( # ` H ) = N )
197 196 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` H ) ) = ( 0 ..^ N ) )
198 197 ad3antrrr 
 |-  ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) -> ( 0 ..^ ( # ` H ) ) = ( 0 ..^ N ) )
199 simpr 
 |-  ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) -> i = ( F ` y ) )
200 6 fveq1i 
 |-  ( H ` z ) = ( ( F cyclShift S ) ` z )
201 200 a1i 
 |-  ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) -> ( H ` z ) = ( ( F cyclShift S ) ` z ) )
202 199 201 eqeq12d 
 |-  ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) -> ( i = ( H ` z ) <-> ( F ` y ) = ( ( F cyclShift S ) ` z ) ) )
203 198 202 rexeqbidv 
 |-  ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) -> ( E. z e. ( 0 ..^ ( # ` H ) ) i = ( H ` z ) <-> E. z e. ( 0 ..^ N ) ( F ` y ) = ( ( F cyclShift S ) ` z ) ) )
204 195 203 mpbird 
 |-  ( ( ( ( ph /\ i e. dom I ) /\ y e. ( 0 ..^ ( # ` F ) ) ) /\ i = ( F ` y ) ) -> E. z e. ( 0 ..^ ( # ` H ) ) i = ( H ` z ) )
205 204 rexlimdva2 
 |-  ( ( ph /\ i e. dom I ) -> ( E. y e. ( 0 ..^ ( # ` F ) ) i = ( F ` y ) -> E. z e. ( 0 ..^ ( # ` H ) ) i = ( H ` z ) ) )
206 205 ralimdva 
 |-  ( ph -> ( A. i e. dom I E. y e. ( 0 ..^ ( # ` F ) ) i = ( F ` y ) -> A. i e. dom I E. z e. ( 0 ..^ ( # ` H ) ) i = ( H ` z ) ) )
207 206 impcom 
 |-  ( ( A. i e. dom I E. y e. ( 0 ..^ ( # ` F ) ) i = ( F ` y ) /\ ph ) -> A. i e. dom I E. z e. ( 0 ..^ ( # ` H ) ) i = ( H ` z ) )
208 207 anim1ci 
 |-  ( ( ( A. i e. dom I E. y e. ( 0 ..^ ( # ` F ) ) i = ( F ` y ) /\ ph ) /\ H : ( 0 ..^ ( # ` H ) ) --> dom I ) -> ( H : ( 0 ..^ ( # ` H ) ) --> dom I /\ A. i e. dom I E. z e. ( 0 ..^ ( # ` H ) ) i = ( H ` z ) ) )
209 dffo3 
 |-  ( H : ( 0 ..^ ( # ` H ) ) -onto-> dom I <-> ( H : ( 0 ..^ ( # ` H ) ) --> dom I /\ A. i e. dom I E. z e. ( 0 ..^ ( # ` H ) ) i = ( H ` z ) ) )
210 208 209 sylibr 
 |-  ( ( ( A. i e. dom I E. y e. ( 0 ..^ ( # ` F ) ) i = ( F ` y ) /\ ph ) /\ H : ( 0 ..^ ( # ` H ) ) --> dom I ) -> H : ( 0 ..^ ( # ` H ) ) -onto-> dom I )
211 210 exp31 
 |-  ( A. i e. dom I E. y e. ( 0 ..^ ( # ` F ) ) i = ( F ` y ) -> ( ph -> ( H : ( 0 ..^ ( # ` H ) ) --> dom I -> H : ( 0 ..^ ( # ` H ) ) -onto-> dom I ) ) )
212 19 211 simplbiim 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -onto-> dom I -> ( ph -> ( H : ( 0 ..^ ( # ` H ) ) --> dom I -> H : ( 0 ..^ ( # ` H ) ) -onto-> dom I ) ) )
213 18 212 simplbiim 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I -> ( ph -> ( H : ( 0 ..^ ( # ` H ) ) --> dom I -> H : ( 0 ..^ ( # ` H ) ) -onto-> dom I ) ) )
214 213 com13 
 |-  ( H : ( 0 ..^ ( # ` H ) ) --> dom I -> ( ph -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I -> H : ( 0 ..^ ( # ` H ) ) -onto-> dom I ) ) )
215 17 214 syl 
 |-  ( H ( Trails ` G ) Q -> ( ph -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I -> H : ( 0 ..^ ( # ` H ) ) -onto-> dom I ) ) )
216 215 impcom 
 |-  ( ( ph /\ H ( Trails ` G ) Q ) -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I -> H : ( 0 ..^ ( # ` H ) ) -onto-> dom I ) )
217 13 216 mpd 
 |-  ( ( ph /\ H ( Trails ` G ) Q ) -> H : ( 0 ..^ ( # ` H ) ) -onto-> dom I )
218 10 217 jca 
 |-  ( ( ph /\ H ( Trails ` G ) Q ) -> ( H ( Trails ` G ) Q /\ H : ( 0 ..^ ( # ` H ) ) -onto-> dom I ) )
219 9 218 mpdan 
 |-  ( ph -> ( H ( Trails ` G ) Q /\ H : ( 0 ..^ ( # ` H ) ) -onto-> dom I ) )
220 2 iseupth 
 |-  ( H ( EulerPaths ` G ) Q <-> ( H ( Trails ` G ) Q /\ H : ( 0 ..^ ( # ` H ) ) -onto-> dom I ) )
221 219 220 sylibr 
 |-  ( ph -> H ( EulerPaths ` G ) Q )
222 1 2 3 4 5 6 7 crctcsh 
 |-  ( ph -> H ( Circuits ` G ) Q )
223 221 222 jca 
 |-  ( ph -> ( H ( EulerPaths ` G ) Q /\ H ( Circuits ` G ) Q ) )