This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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