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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
eucrct2eupth1.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
eucrct2eupth1.d ⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
eucrct2eupth1.c ⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
eucrct2eupth1.s ⊢ ( Vtx ‘ 𝑆 ) = 𝑉
eucrct2eupth.n ⊢ ( 𝜑 → 𝑁 = ( ♯ ‘ 𝐹 ) )
eucrct2eupth.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ 𝑁 ) )
eucrct2eupth.e ⊢ ( 𝜑 → ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ ( 𝐹 “ ( ( 0 ..^ 𝑁 ) ∖ { 𝐽 } ) ) ) )
eucrct2eupth.k ⊢ 𝐾 = ( 𝐽 + 1 )
eucrct2eupth.h ⊢ 𝐻 = ( ( 𝐹 cyclShift 𝐾 ) prefix ( 𝑁 − 1 ) )
eucrct2eupth.q ⊢ 𝑄 = ( 𝑥 ∈ ( 0 ..^ 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝐾 ) , ( 𝑃 ‘ ( 𝑥 + 𝐾 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝐾 ) − 𝑁 ) ) ) )
Assertion eucrct2eupth ( 𝜑 → 𝐻 ( EulerPaths ‘ 𝑆 ) 𝑄 )

Proof

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