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 𝑉 = ( Vtx ‘ 𝐺 )
eucrctshift.i 𝐼 = ( iEdg ‘ 𝐺 )
eucrctshift.c ( 𝜑𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
eucrctshift.n 𝑁 = ( ♯ ‘ 𝐹 )
eucrctshift.s ( 𝜑𝑆 ∈ ( 0 ..^ 𝑁 ) )
eucrctshift.h 𝐻 = ( 𝐹 cyclShift 𝑆 )
eucrctshift.q 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
eucrctshift.e ( 𝜑𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
Assertion eucrctshift ( 𝜑 → ( 𝐻 ( EulerPaths ‘ 𝐺 ) 𝑄𝐻 ( Circuits ‘ 𝐺 ) 𝑄 ) )

Proof

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