MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eucrct2eupth Structured version   Visualization version   GIF version

Theorem eucrct2eupth 28018
Description: Removing one edge (𝐼‘(𝐹𝐽)) from a graph 𝐺 with an Eulerian circuit 𝐹, 𝑃 results in a graph 𝑆 with an Eulerian path 𝐻, 𝑄. (Contributed by AV, 17-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
Hypotheses
Ref Expression
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
Ref Expression
eucrct2eupth (𝜑𝐻(EulerPaths‘𝑆)𝑄)
Distinct variable groups:   𝑥,𝐹   𝑥,𝐼   𝑥,𝐽   𝑥,𝐾   𝑥,𝑁   𝑥,𝑃   𝑥,𝑉   𝜑,𝑥
Allowed substitution hints:   𝑄(𝑥)   𝑆(𝑥)   𝐺(𝑥)   𝐻(𝑥)

Proof of Theorem eucrct2eupth
StepHypRef Expression
1 eucrct2eupth1.v . . . 4 𝑉 = (Vtx‘𝐺)
2 eucrct2eupth1.i . . . 4 𝐼 = (iEdg‘𝐺)
3 eucrct2eupth1.d . . . . . 6 (𝜑𝐹(EulerPaths‘𝐺)𝑃)
43adantl 484 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
5 eucrct2eupth.k . . . . . . . 8 𝐾 = (𝐽 + 1)
65eqcomi 2830 . . . . . . 7 (𝐽 + 1) = 𝐾
76oveq2i 7161 . . . . . 6 (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝐾)
8 oveq1 7157 . . . . . . . . 9 (𝐽 = (𝑁 − 1) → (𝐽 + 1) = ((𝑁 − 1) + 1))
9 eucrct2eupth.j . . . . . . . . . 10 (𝜑𝐽 ∈ (0..^𝑁))
10 elfzo0 13072 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
11 nncn 11640 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
12113ad2ant2 1130 . . . . . . . . . . 11 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℂ)
1310, 12sylbi 219 . . . . . . . . . 10 (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℂ)
14 npcan1 11059 . . . . . . . . . 10 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
159, 13, 143syl 18 . . . . . . . . 9 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
168, 15sylan9eq 2876 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) = 𝑁)
1716oveq2d 7166 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝑁))
18 eucrct2eupth.n . . . . . . . . . 10 (𝜑𝑁 = (♯‘𝐹))
1918oveq2d 7166 . . . . . . . . 9 (𝜑 → (𝐹 cyclShift 𝑁) = (𝐹 cyclShift (♯‘𝐹)))
20 eucrct2eupth1.c . . . . . . . . . . 11 (𝜑𝐹(Circuits‘𝐺)𝑃)
21 crctiswlk 27571 . . . . . . . . . . . 12 (𝐹(Circuits‘𝐺)𝑃𝐹(Walks‘𝐺)𝑃)
222wlkf 27390 . . . . . . . . . . . 12 (𝐹(Walks‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
2321, 22syl 17 . . . . . . . . . . 11 (𝐹(Circuits‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
2420, 23syl 17 . . . . . . . . . 10 (𝜑𝐹 ∈ Word dom 𝐼)
25 cshwn 14153 . . . . . . . . . 10 (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
2624, 25syl 17 . . . . . . . . 9 (𝜑 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
2719, 26eqtrd 2856 . . . . . . . 8 (𝜑 → (𝐹 cyclShift 𝑁) = 𝐹)
2827adantl 484 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝑁) = 𝐹)
2917, 28eqtrd 2856 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = 𝐹)
307, 29syl5eqr 2870 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾) = 𝐹)
31 eqid 2821 . . . . . . . . . . . . . 14 (♯‘𝐹) = (♯‘𝐹)
321, 2, 20, 31crctcshlem1 27589 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐹) ∈ ℕ0)
33 fz0sn0fz1 13018 . . . . . . . . . . . . 13 ((♯‘𝐹) ∈ ℕ0 → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
3432, 33syl 17 . . . . . . . . . . . 12 (𝜑 → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
3534eleq2d 2898 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ 𝑥 ∈ ({0} ∪ (1...(♯‘𝐹)))))
36 elun 4125 . . . . . . . . . . 11 (𝑥 ∈ ({0} ∪ (1...(♯‘𝐹))) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))))
3735, 36syl6bb 289 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹)))))
38 elsni 4578 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {0} → 𝑥 = 0)
39 0le0 11732 . . . . . . . . . . . . . . . 16 0 ≤ 0
4038, 39eqbrtrdi 5098 . . . . . . . . . . . . . . 15 (𝑥 ∈ {0} → 𝑥 ≤ 0)
4140adantl 484 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ {0}) → 𝑥 ≤ 0)
4241iftrued 4475 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘(𝑥 + 𝑁)))
4318fveq2d 6669 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑃𝑁) = (𝑃‘(♯‘𝐹)))
44 crctprop 27567 . . . . . . . . . . . . . . . . . 18 (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
45 simpr 487 . . . . . . . . . . . . . . . . . . 19 ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘0) = (𝑃‘(♯‘𝐹)))
4645eqcomd 2827 . . . . . . . . . . . . . . . . . 18 ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
4720, 44, 463syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
4843, 47eqtrd 2856 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃𝑁) = (𝑃‘0))
4948adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 0) → (𝑃𝑁) = (𝑃‘0))
50 oveq1 7157 . . . . . . . . . . . . . . . . 17 (𝑥 = 0 → (𝑥 + 𝑁) = (0 + 𝑁))
519, 13syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℂ)
5251addid2d 10835 . . . . . . . . . . . . . . . . 17 (𝜑 → (0 + 𝑁) = 𝑁)
5350, 52sylan9eqr 2878 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 = 0) → (𝑥 + 𝑁) = 𝑁)
5453fveq2d 6669 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃𝑁))
55 fveq2 6665 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → (𝑃𝑥) = (𝑃‘0))
5655adantl 484 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 0) → (𝑃𝑥) = (𝑃‘0))
5749, 54, 563eqtr4d 2866 . . . . . . . . . . . . . 14 ((𝜑𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃𝑥))
5838, 57sylan2 594 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ {0}) → (𝑃‘(𝑥 + 𝑁)) = (𝑃𝑥))
5942, 58eqtrd 2856 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥))
6059ex 415 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ {0} → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
61 elfznn 12930 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℕ)
62 nnnle0 11664 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → ¬ 𝑥 ≤ 0)
6361, 62syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1...(♯‘𝐹)) → ¬ 𝑥 ≤ 0)
6463adantl 484 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → ¬ 𝑥 ≤ 0)
6564iffalsed 4478 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
6661nncnd 11648 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℂ)
6766adantl 484 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → 𝑥 ∈ ℂ)
6851adantr 483 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → 𝑁 ∈ ℂ)
6967, 68pncand 10992 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → ((𝑥 + 𝑁) − 𝑁) = 𝑥)
7069fveq2d 6669 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → (𝑃‘((𝑥 + 𝑁) − 𝑁)) = (𝑃𝑥))
7165, 70eqtrd 2856 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥))
7271ex 415 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (1...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
7360, 72jaod 855 . . . . . . . . . 10 (𝜑 → ((𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
7437, 73sylbid 242 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
7574imp 409 . . . . . . . 8 ((𝜑𝑥 ∈ (0...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥))
7675mpteq2dva 5154 . . . . . . 7 (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃𝑥)))
7776adantl 484 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃𝑥)))
785oveq2i 7161 . . . . . . . . . 10 (𝑁𝐾) = (𝑁 − (𝐽 + 1))
798oveq2d 7166 . . . . . . . . . . 11 (𝐽 = (𝑁 − 1) → (𝑁 − (𝐽 + 1)) = (𝑁 − ((𝑁 − 1) + 1)))
8015oveq2d 7166 . . . . . . . . . . . 12 (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = (𝑁𝑁))
8151subidd 10979 . . . . . . . . . . . 12 (𝜑 → (𝑁𝑁) = 0)
8280, 81eqtrd 2856 . . . . . . . . . . 11 (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = 0)
8379, 82sylan9eq 2876 . . . . . . . . . 10 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − (𝐽 + 1)) = 0)
8478, 83syl5eq 2868 . . . . . . . . 9 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁𝐾) = 0)
8584breq2d 5071 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ (𝑁𝐾) ↔ 𝑥 ≤ 0))
865oveq2i 7161 . . . . . . . . . 10 (𝑥 + 𝐾) = (𝑥 + (𝐽 + 1))
8786fveq2i 6668 . . . . . . . . 9 (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + (𝐽 + 1)))
888oveq2d 7166 . . . . . . . . . . 11 (𝐽 = (𝑁 − 1) → (𝑥 + (𝐽 + 1)) = (𝑥 + ((𝑁 − 1) + 1)))
8915oveq2d 7166 . . . . . . . . . . 11 (𝜑 → (𝑥 + ((𝑁 − 1) + 1)) = (𝑥 + 𝑁))
9088, 89sylan9eq 2876 . . . . . . . . . 10 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 + (𝐽 + 1)) = (𝑥 + 𝑁))
9190fveq2d 6669 . . . . . . . . 9 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + (𝐽 + 1))) = (𝑃‘(𝑥 + 𝑁)))
9287, 91syl5eq 2868 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + 𝑁)))
9386oveq1i 7160 . . . . . . . . . 10 ((𝑥 + 𝐾) − 𝑁) = ((𝑥 + (𝐽 + 1)) − 𝑁)
9493fveq2i 6668 . . . . . . . . 9 (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁))
9588oveq1d 7165 . . . . . . . . . . 11 (𝐽 = (𝑁 − 1) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁))
9689oveq1d 7165 . . . . . . . . . . 11 (𝜑 → ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
9795, 96sylan9eq 2876 . . . . . . . . . 10 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
9897fveq2d 6669 . . . . . . . . 9 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
9994, 98syl5eq 2868 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
10085, 92, 99ifbieq12d 4494 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))) = if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))))
101100mpteq2dv 5155 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))))
10220, 21syl 17 . . . . . . . . 9 (𝜑𝐹(Walks‘𝐺)𝑃)
1031wlkp 27392 . . . . . . . . 9 (𝐹(Walks‘𝐺)𝑃𝑃:(0...(♯‘𝐹))⟶𝑉)
104 ffn 6509 . . . . . . . . 9 (𝑃:(0...(♯‘𝐹))⟶𝑉𝑃 Fn (0...(♯‘𝐹)))
105102, 103, 1043syl 18 . . . . . . . 8 (𝜑𝑃 Fn (0...(♯‘𝐹)))
106105adantl 484 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 Fn (0...(♯‘𝐹)))
107 dffn5 6719 . . . . . . 7 (𝑃 Fn (0...(♯‘𝐹)) ↔ 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃𝑥)))
108106, 107sylib 220 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃𝑥)))
10977, 101, 1083eqtr4d 2866 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = 𝑃)
1104, 30, 1093brtr4d 5091 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
11120adantl 484 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
112111, 30, 1093brtr4d 5091 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
113 eucrct2eupth1.s . . . 4 (Vtx‘𝑆) = 𝑉
114 elfzolt3 13042 . . . . . . 7 (𝐽 ∈ (0..^𝑁) → 0 < 𝑁)
1159, 114syl 17 . . . . . 6 (𝜑 → 0 < 𝑁)
116 elfzoelz 13032 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
1179, 116syl 17 . . . . . . . . . 10 (𝜑𝐽 ∈ ℤ)
118117peano2zd 12084 . . . . . . . . 9 (𝜑 → (𝐽 + 1) ∈ ℤ)
1195, 118eqeltrid 2917 . . . . . . . 8 (𝜑𝐾 ∈ ℤ)
120 cshwlen 14155 . . . . . . . . 9 ((𝐹 ∈ Word dom 𝐼𝐾 ∈ ℤ) → (♯‘(𝐹 cyclShift 𝐾)) = (♯‘𝐹))
121120eqcomd 2827 . . . . . . . 8 ((𝐹 ∈ Word dom 𝐼𝐾 ∈ ℤ) → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
12224, 119, 121syl2anc 586 . . . . . . 7 (𝜑 → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
12318, 122eqtrd 2856 . . . . . 6 (𝜑𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
124115, 123breqtrd 5085 . . . . 5 (𝜑 → 0 < (♯‘(𝐹 cyclShift 𝐾)))
125124adantl 484 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
126123adantl 484 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
127126oveq1d 7165 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
128 eucrct2eupth.e . . . . . 6 (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
129128adantl 484 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
13024, 18, 93jca 1124 . . . . . . . . 9 (𝜑 → (𝐹 ∈ Word dom 𝐼𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
131130adantl 484 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
132 cshimadifsn0 14186 . . . . . . . 8 ((𝐹 ∈ Word dom 𝐼𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
133131, 132syl 17 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
1347imaeq1i 5921 . . . . . . 7 ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))
135133, 134syl6eq 2872 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
136135reseq2d 5848 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
137129, 136eqtrd 2856 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
138 eqid 2821 . . . 4 ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1)) = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))
139 eqid 2821 . . . 4 ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))
1401, 2, 110, 112, 113, 125, 127, 137, 138, 139eucrct2eupth1 28017 . . 3 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))(EulerPaths‘𝑆)((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
141 eucrct2eupth.h . . . 4 𝐻 = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))
142141a1i 11 . . 3 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻 = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1)))
143 eucrct2eupth.q . . . . 5 𝑄 = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
144 fzossfz 13050 . . . . . . . 8 (0..^𝑁) ⊆ (0...𝑁)
14518oveq2d 7166 . . . . . . . 8 (𝜑 → (0...𝑁) = (0...(♯‘𝐹)))
146144, 145sseqtrid 4019 . . . . . . 7 (𝜑 → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
147146resmptd 5903 . . . . . 6 (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
148 elfzoel2 13031 . . . . . . . 8 (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
149 fzoval 13033 . . . . . . . 8 (𝑁 ∈ ℤ → (0..^𝑁) = (0...(𝑁 − 1)))
1509, 148, 1493syl 18 . . . . . . 7 (𝜑 → (0..^𝑁) = (0...(𝑁 − 1)))
151150reseq2d 5848 . . . . . 6 (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
152147, 151eqtr3d 2858 . . . . 5 (𝜑 → (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
153143, 152syl5eq 2868 . . . 4 (𝜑𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
154153adantl 484 . . 3 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
155140, 142, 1543brtr4d 5091 . 2 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
15620adantl 484 . . . 4 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
157 peano2nn0 11931 . . . . . . . . . . . . 13 (𝐽 ∈ ℕ0 → (𝐽 + 1) ∈ ℕ0)
1581573ad2ant1 1129 . . . . . . . . . . . 12 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℕ0)
159158adantr 483 . . . . . . . . . . 11 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) ∈ ℕ0)
160 simpl2 1188 . . . . . . . . . . 11 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → 𝑁 ∈ ℕ)
161 1cnd 10630 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 1 ∈ ℂ)
162 nn0cn 11901 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ ℕ0𝐽 ∈ ℂ)
1631623ad2ant1 1129 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝐽 ∈ ℂ)
16412, 161, 163subadd2d 11010 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝑁 − 1) = 𝐽 ↔ (𝐽 + 1) = 𝑁))
165 eqcom 2828 . . . . . . . . . . . . . . 15 (𝐽 = (𝑁 − 1) ↔ (𝑁 − 1) = 𝐽)
166 eqcom 2828 . . . . . . . . . . . . . . 15 (𝑁 = (𝐽 + 1) ↔ (𝐽 + 1) = 𝑁)
167164, 165, 1663bitr4g 316 . . . . . . . . . . . . . 14 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 = (𝑁 − 1) ↔ 𝑁 = (𝐽 + 1)))
168167necon3bbid 3053 . . . . . . . . . . . . 13 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) ↔ 𝑁 ≠ (𝐽 + 1)))
169157nn0red 11950 . . . . . . . . . . . . . . . 16 (𝐽 ∈ ℕ0 → (𝐽 + 1) ∈ ℝ)
1701693ad2ant1 1129 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℝ)
171 nnre 11639 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
1721713ad2ant2 1130 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℝ)
173 nn0z 11999 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ ℕ0𝐽 ∈ ℤ)
174 nnz 11998 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
175 zltp1le 12026 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
176173, 174, 175syl2an 597 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
177176biimp3a 1465 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ≤ 𝑁)
178170, 172, 177leltned 10787 . . . . . . . . . . . . . 14 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝐽 + 1) < 𝑁𝑁 ≠ (𝐽 + 1)))
179178biimprd 250 . . . . . . . . . . . . 13 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝑁 ≠ (𝐽 + 1) → (𝐽 + 1) < 𝑁))
180168, 179sylbid 242 . . . . . . . . . . . 12 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) < 𝑁))
181180imp 409 . . . . . . . . . . 11 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) < 𝑁)
182159, 160, 1813jca 1124 . . . . . . . . . 10 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
183182ex 415 . . . . . . . . 9 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
18410, 183sylbi 219 . . . . . . . 8 (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
185 elfzo0 13072 . . . . . . . 8 ((𝐽 + 1) ∈ (0..^𝑁) ↔ ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
186184, 185syl6ibr 254 . . . . . . 7 (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
1879, 186syl 17 . . . . . 6 (𝜑 → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
188187impcom 410 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) ∈ (0..^𝑁))
1895a1i 11 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 = (𝐽 + 1))
19018eqcomd 2827 . . . . . . 7 (𝜑 → (♯‘𝐹) = 𝑁)
191190oveq2d 7166 . . . . . 6 (𝜑 → (0..^(♯‘𝐹)) = (0..^𝑁))
192191adantl 484 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^(♯‘𝐹)) = (0..^𝑁))
193188, 189, 1923eltr4d 2928 . . . 4 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 ∈ (0..^(♯‘𝐹)))
194 eqid 2821 . . . 4 (𝐹 cyclShift 𝐾) = (𝐹 cyclShift 𝐾)
195 eqid 2821 . . . 4 (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))
1963adantl 484 . . . 4 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
1971, 2, 156, 31, 193, 194, 195, 196eucrctshift 28016 . . 3 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))))
198 simprl 769 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
199 simprr 771 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
200124ad2antlr 725 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
201123oveq1d 7165 . . . . . 6 (𝜑 → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
202201ad2antlr 725 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
203128adantl 484 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
204130adantl 484 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
205204, 132syl 17 . . . . . . . . 9 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
206205, 134syl6eq 2872 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
207206reseq2d 5848 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
208203, 207eqtrd 2856 . . . . . 6 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
209208adantr 483 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
210 eqid 2821 . . . . 5 ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1)))
2111, 2, 198, 199, 113, 200, 202, 209, 138, 210eucrct2eupth1 28017 . . . 4 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))(EulerPaths‘𝑆)((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
212141a1i 11 . . . 4 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝐻 = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1)))
213190oveq1d 7165 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝐹) − 𝐾) = (𝑁𝐾))
214213breq2d 5071 . . . . . . . . . . 11 (𝜑 → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁𝐾)))
215214adantl 484 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁𝐾)))
216190oveq2d 7166 . . . . . . . . . . . 12 (𝜑 → ((𝑥 + 𝐾) − (♯‘𝐹)) = ((𝑥 + 𝐾) − 𝑁))
217216fveq2d 6669 . . . . . . . . . . 11 (𝜑 → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
218217adantl 484 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
219215, 218ifbieq2d 4492 . . . . . . . . 9 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))) = if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
220219mpteq2dv 5155 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
221150eqcomd 2827 . . . . . . . . 9 (𝜑 → (0...(𝑁 − 1)) = (0..^𝑁))
222221adantl 484 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...(𝑁 − 1)) = (0..^𝑁))
223220, 222reseq12d 5849 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)))
22418adantl 484 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘𝐹))
225224oveq2d 7166 . . . . . . . . 9 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...𝑁) = (0...(♯‘𝐹)))
226144, 225sseqtrid 4019 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
227226resmptd 5903 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
228223, 227eqtrd 2856 . . . . . 6 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
229228, 143syl6reqr 2875 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
230229adantr 483 . . . 4 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
231211, 212, 2303brtr4d 5091 . . 3 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝐻(EulerPaths‘𝑆)𝑄)
232197, 231mpdan 685 . 2 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
233155, 232pm2.61ian 810 1 (𝜑𝐻(EulerPaths‘𝑆)𝑄)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843  w3a 1083   = wceq 1533  wcel 2110  wne 3016  cdif 3933  cun 3934  ifcif 4467  {csn 4561   class class class wbr 5059  cmpt 5139  dom cdm 5550  cres 5552  cima 5553   Fn wfn 6345  wf 6346  cfv 6350  (class class class)co 7150  cc 10529  cr 10530  0cc0 10531  1c1 10532   + caddc 10534   < clt 10669  cle 10670  cmin 10864  cn 11632  0cn0 11891  cz 11975  ...cfz 12886  ..^cfzo 13027  chash 13684  Word cword 13855   prefix cpfx 14026   cyclShift ccsh 14144  Vtxcvtx 26775  iEdgciedg 26776  Walkscwlks 27372  Trailsctrls 27466  Circuitsccrcts 27559  EulerPathsceupth 27970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608  ax-pre-sup 10609
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ifp 1058  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8283  df-map 8402  df-pm 8403  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-sup 8900  df-inf 8901  df-card 9362  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-2 11694  df-n0 11892  df-z 11976  df-uz 12238  df-rp 12384  df-ico 12738  df-fz 12887  df-fzo 13028  df-fl 13156  df-mod 13232  df-hash 13685  df-word 13856  df-concat 13917  df-substr 13997  df-pfx 14027  df-csh 14145  df-wlks 27375  df-trls 27468  df-crcts 27561  df-eupth 27971
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator