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

Theorem eucrct2eupth 27397
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.)
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 𝐾) ↾ (0..^(𝑁 − 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 473 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
5 eucrct2eupth.k . . . . . . . 8 𝐾 = (𝐽 + 1)
65eqcomi 2769 . . . . . . 7 (𝐽 + 1) = 𝐾
76oveq2i 6824 . . . . . 6 (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝐾)
8 oveq1 6820 . . . . . . . . 9 (𝐽 = (𝑁 − 1) → (𝐽 + 1) = ((𝑁 − 1) + 1))
9 eucrct2eupth.j . . . . . . . . . 10 (𝜑𝐽 ∈ (0..^𝑁))
10 elfzo0 12703 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
11 nncn 11220 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
12113ad2ant2 1129 . . . . . . . . . . 11 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℂ)
1310, 12sylbi 207 . . . . . . . . . 10 (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℂ)
14 npcan1 10647 . . . . . . . . . 10 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
159, 13, 143syl 18 . . . . . . . . 9 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
168, 15sylan9eq 2814 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) = 𝑁)
1716oveq2d 6829 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝑁))
18 eucrct2eupth.n . . . . . . . . . 10 (𝜑𝑁 = (♯‘𝐹))
1918oveq2d 6829 . . . . . . . . 9 (𝜑 → (𝐹 cyclShift 𝑁) = (𝐹 cyclShift (♯‘𝐹)))
20 eucrct2eupth1.c . . . . . . . . . . 11 (𝜑𝐹(Circuits‘𝐺)𝑃)
21 crctiswlk 26902 . . . . . . . . . . . 12 (𝐹(Circuits‘𝐺)𝑃𝐹(Walks‘𝐺)𝑃)
222wlkf 26720 . . . . . . . . . . . 12 (𝐹(Walks‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
2321, 22syl 17 . . . . . . . . . . 11 (𝐹(Circuits‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
2420, 23syl 17 . . . . . . . . . 10 (𝜑𝐹 ∈ Word dom 𝐼)
25 cshwn 13743 . . . . . . . . . 10 (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
2624, 25syl 17 . . . . . . . . 9 (𝜑 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
2719, 26eqtrd 2794 . . . . . . . 8 (𝜑 → (𝐹 cyclShift 𝑁) = 𝐹)
2827adantl 473 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝑁) = 𝐹)
2917, 28eqtrd 2794 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = 𝐹)
307, 29syl5eqr 2808 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾) = 𝐹)
31 eqid 2760 . . . . . . . . . . . . . 14 (♯‘𝐹) = (♯‘𝐹)
321, 2, 20, 31crctcshlem1 26920 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐹) ∈ ℕ0)
33 fz0sn0fz1 12650 . . . . . . . . . . . . 13 ((♯‘𝐹) ∈ ℕ0 → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
3432, 33syl 17 . . . . . . . . . . . 12 (𝜑 → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
3534eleq2d 2825 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ 𝑥 ∈ ({0} ∪ (1...(♯‘𝐹)))))
36 elun 3896 . . . . . . . . . . 11 (𝑥 ∈ ({0} ∪ (1...(♯‘𝐹))) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))))
3735, 36syl6bb 276 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹)))))
38 elsni 4338 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {0} → 𝑥 = 0)
39 0le0 11302 . . . . . . . . . . . . . . . 16 0 ≤ 0
4038, 39syl6eqbr 4843 . . . . . . . . . . . . . . 15 (𝑥 ∈ {0} → 𝑥 ≤ 0)
4140adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ {0}) → 𝑥 ≤ 0)
4241iftrued 4238 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘(𝑥 + 𝑁)))
4318fveq2d 6356 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑃𝑁) = (𝑃‘(♯‘𝐹)))
44 crctprop 26898 . . . . . . . . . . . . . . . . . 18 (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
45 simpr 479 . . . . . . . . . . . . . . . . . . 19 ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘0) = (𝑃‘(♯‘𝐹)))
4645eqcomd 2766 . . . . . . . . . . . . . . . . . 18 ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
4720, 44, 463syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
4843, 47eqtrd 2794 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃𝑁) = (𝑃‘0))
4948adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 0) → (𝑃𝑁) = (𝑃‘0))
50 oveq1 6820 . . . . . . . . . . . . . . . . 17 (𝑥 = 0 → (𝑥 + 𝑁) = (0 + 𝑁))
519, 13syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℂ)
5251addid2d 10429 . . . . . . . . . . . . . . . . 17 (𝜑 → (0 + 𝑁) = 𝑁)
5350, 52sylan9eqr 2816 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 = 0) → (𝑥 + 𝑁) = 𝑁)
5453fveq2d 6356 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃𝑁))
55 fveq2 6352 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → (𝑃𝑥) = (𝑃‘0))
5655adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 0) → (𝑃𝑥) = (𝑃‘0))
5749, 54, 563eqtr4d 2804 . . . . . . . . . . . . . 14 ((𝜑𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃𝑥))
5838, 57sylan2 492 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ {0}) → (𝑃‘(𝑥 + 𝑁)) = (𝑃𝑥))
5942, 58eqtrd 2794 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥))
6059ex 449 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ {0} → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
61 elfznn 12563 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℕ)
62 nnnle0 11243 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → ¬ 𝑥 ≤ 0)
6361, 62syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1...(♯‘𝐹)) → ¬ 𝑥 ≤ 0)
6463adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → ¬ 𝑥 ≤ 0)
6564iffalsed 4241 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
6661nncnd 11228 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℂ)
6766adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → 𝑥 ∈ ℂ)
6851adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → 𝑁 ∈ ℂ)
6967, 68pncand 10585 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → ((𝑥 + 𝑁) − 𝑁) = 𝑥)
7069fveq2d 6356 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → (𝑃‘((𝑥 + 𝑁) − 𝑁)) = (𝑃𝑥))
7165, 70eqtrd 2794 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥))
7271ex 449 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (1...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
7360, 72jaod 394 . . . . . . . . . 10 (𝜑 → ((𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
7437, 73sylbid 230 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
7574imp 444 . . . . . . . 8 ((𝜑𝑥 ∈ (0...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥))
7675mpteq2dva 4896 . . . . . . 7 (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃𝑥)))
7776adantl 473 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃𝑥)))
785oveq2i 6824 . . . . . . . . . 10 (𝑁𝐾) = (𝑁 − (𝐽 + 1))
798oveq2d 6829 . . . . . . . . . . 11 (𝐽 = (𝑁 − 1) → (𝑁 − (𝐽 + 1)) = (𝑁 − ((𝑁 − 1) + 1)))
8015oveq2d 6829 . . . . . . . . . . . 12 (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = (𝑁𝑁))
8151subidd 10572 . . . . . . . . . . . 12 (𝜑 → (𝑁𝑁) = 0)
8280, 81eqtrd 2794 . . . . . . . . . . 11 (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = 0)
8379, 82sylan9eq 2814 . . . . . . . . . 10 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − (𝐽 + 1)) = 0)
8478, 83syl5eq 2806 . . . . . . . . 9 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁𝐾) = 0)
8584breq2d 4816 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ (𝑁𝐾) ↔ 𝑥 ≤ 0))
865oveq2i 6824 . . . . . . . . . 10 (𝑥 + 𝐾) = (𝑥 + (𝐽 + 1))
8786fveq2i 6355 . . . . . . . . 9 (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + (𝐽 + 1)))
888oveq2d 6829 . . . . . . . . . . 11 (𝐽 = (𝑁 − 1) → (𝑥 + (𝐽 + 1)) = (𝑥 + ((𝑁 − 1) + 1)))
8915oveq2d 6829 . . . . . . . . . . 11 (𝜑 → (𝑥 + ((𝑁 − 1) + 1)) = (𝑥 + 𝑁))
9088, 89sylan9eq 2814 . . . . . . . . . 10 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 + (𝐽 + 1)) = (𝑥 + 𝑁))
9190fveq2d 6356 . . . . . . . . 9 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + (𝐽 + 1))) = (𝑃‘(𝑥 + 𝑁)))
9287, 91syl5eq 2806 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + 𝑁)))
9386oveq1i 6823 . . . . . . . . . 10 ((𝑥 + 𝐾) − 𝑁) = ((𝑥 + (𝐽 + 1)) − 𝑁)
9493fveq2i 6355 . . . . . . . . 9 (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁))
9588oveq1d 6828 . . . . . . . . . . 11 (𝐽 = (𝑁 − 1) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁))
9689oveq1d 6828 . . . . . . . . . . 11 (𝜑 → ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
9795, 96sylan9eq 2814 . . . . . . . . . 10 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
9897fveq2d 6356 . . . . . . . . 9 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
9994, 98syl5eq 2806 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
10085, 92, 99ifbieq12d 4257 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))) = if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))))
101100mpteq2dv 4897 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))))
10220, 21syl 17 . . . . . . . . 9 (𝜑𝐹(Walks‘𝐺)𝑃)
1031wlkp 26722 . . . . . . . . 9 (𝐹(Walks‘𝐺)𝑃𝑃:(0...(♯‘𝐹))⟶𝑉)
104 ffn 6206 . . . . . . . . 9 (𝑃:(0...(♯‘𝐹))⟶𝑉𝑃 Fn (0...(♯‘𝐹)))
105102, 103, 1043syl 18 . . . . . . . 8 (𝜑𝑃 Fn (0...(♯‘𝐹)))
106105adantl 473 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 Fn (0...(♯‘𝐹)))
107 dffn5 6403 . . . . . . 7 (𝑃 Fn (0...(♯‘𝐹)) ↔ 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃𝑥)))
108106, 107sylib 208 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃𝑥)))
10977, 101, 1083eqtr4d 2804 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = 𝑃)
1104, 30, 1093brtr4d 4836 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
11120adantl 473 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
112111, 30, 1093brtr4d 4836 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
113 eucrct2eupth1.s . . . 4 (Vtx‘𝑆) = 𝑉
114 elfzolt3 12674 . . . . . . 7 (𝐽 ∈ (0..^𝑁) → 0 < 𝑁)
1159, 114syl 17 . . . . . 6 (𝜑 → 0 < 𝑁)
116 elfzoelz 12664 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
1179, 116syl 17 . . . . . . . . . 10 (𝜑𝐽 ∈ ℤ)
118117peano2zd 11677 . . . . . . . . 9 (𝜑 → (𝐽 + 1) ∈ ℤ)
1195, 118syl5eqel 2843 . . . . . . . 8 (𝜑𝐾 ∈ ℤ)
120 cshwlen 13745 . . . . . . . . 9 ((𝐹 ∈ Word dom 𝐼𝐾 ∈ ℤ) → (♯‘(𝐹 cyclShift 𝐾)) = (♯‘𝐹))
121120eqcomd 2766 . . . . . . . 8 ((𝐹 ∈ Word dom 𝐼𝐾 ∈ ℤ) → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
12224, 119, 121syl2anc 696 . . . . . . 7 (𝜑 → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
12318, 122eqtrd 2794 . . . . . 6 (𝜑𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
124115, 123breqtrd 4830 . . . . 5 (𝜑 → 0 < (♯‘(𝐹 cyclShift 𝐾)))
125124adantl 473 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
126123adantl 473 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
127126oveq1d 6828 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
128 eucrct2eupth.e . . . . . 6 (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
129128adantl 473 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
13024, 18, 93jca 1123 . . . . . . . . 9 (𝜑 → (𝐹 ∈ Word dom 𝐼𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
131130adantl 473 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
132 cshimadifsn0 13776 . . . . . . . 8 ((𝐹 ∈ Word dom 𝐼𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
133131, 132syl 17 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
1347imaeq1i 5621 . . . . . . 7 ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))
135133, 134syl6eq 2810 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
136135reseq2d 5551 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
137129, 136eqtrd 2794 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
138 eqid 2760 . . . 4 ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1)))
139 eqid 2760 . . . 4 ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))
1401, 2, 110, 112, 113, 125, 127, 137, 138, 139eucrct2eupth1 27396 . . 3 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1)))(EulerPaths‘𝑆)((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
141 eucrct2eupth.h . . . 4 𝐻 = ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1)))
142141a1i 11 . . 3 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻 = ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1))))
143 eucrct2eupth.q . . . . 5 𝑄 = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
144 fzossfz 12682 . . . . . . . 8 (0..^𝑁) ⊆ (0...𝑁)
14518oveq2d 6829 . . . . . . . 8 (𝜑 → (0...𝑁) = (0...(♯‘𝐹)))
146144, 145syl5sseq 3794 . . . . . . 7 (𝜑 → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
147146resmptd 5610 . . . . . 6 (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
148 elfzoel2 12663 . . . . . . . 8 (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
149 fzoval 12665 . . . . . . . 8 (𝑁 ∈ ℤ → (0..^𝑁) = (0...(𝑁 − 1)))
1509, 148, 1493syl 18 . . . . . . 7 (𝜑 → (0..^𝑁) = (0...(𝑁 − 1)))
151150reseq2d 5551 . . . . . 6 (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
152147, 151eqtr3d 2796 . . . . 5 (𝜑 → (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
153143, 152syl5eq 2806 . . . 4 (𝜑𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
154153adantl 473 . . 3 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
155140, 142, 1543brtr4d 4836 . 2 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
15620adantl 473 . . . 4 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
157 peano2nn0 11525 . . . . . . . . . . . . 13 (𝐽 ∈ ℕ0 → (𝐽 + 1) ∈ ℕ0)
1581573ad2ant1 1128 . . . . . . . . . . . 12 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℕ0)
159158adantr 472 . . . . . . . . . . 11 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) ∈ ℕ0)
160 simpl2 1230 . . . . . . . . . . 11 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → 𝑁 ∈ ℕ)
161 1cnd 10248 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 1 ∈ ℂ)
162 nn0cn 11494 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ ℕ0𝐽 ∈ ℂ)
1631623ad2ant1 1128 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝐽 ∈ ℂ)
16412, 161, 163subadd2d 10603 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝑁 − 1) = 𝐽 ↔ (𝐽 + 1) = 𝑁))
165 eqcom 2767 . . . . . . . . . . . . . . 15 (𝐽 = (𝑁 − 1) ↔ (𝑁 − 1) = 𝐽)
166 eqcom 2767 . . . . . . . . . . . . . . 15 (𝑁 = (𝐽 + 1) ↔ (𝐽 + 1) = 𝑁)
167164, 165, 1663bitr4g 303 . . . . . . . . . . . . . 14 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 = (𝑁 − 1) ↔ 𝑁 = (𝐽 + 1)))
168167necon3bbid 2969 . . . . . . . . . . . . 13 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) ↔ 𝑁 ≠ (𝐽 + 1)))
169157nn0red 11544 . . . . . . . . . . . . . . . 16 (𝐽 ∈ ℕ0 → (𝐽 + 1) ∈ ℝ)
1701693ad2ant1 1128 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℝ)
171 nnre 11219 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
1721713ad2ant2 1129 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℝ)
173 nn0z 11592 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ ℕ0𝐽 ∈ ℤ)
174 nnz 11591 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
175 zltp1le 11619 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
176173, 174, 175syl2an 495 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
177176biimp3a 1581 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ≤ 𝑁)
178170, 172, 177leltned 10382 . . . . . . . . . . . . . 14 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝐽 + 1) < 𝑁𝑁 ≠ (𝐽 + 1)))
179178biimprd 238 . . . . . . . . . . . . 13 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝑁 ≠ (𝐽 + 1) → (𝐽 + 1) < 𝑁))
180168, 179sylbid 230 . . . . . . . . . . . 12 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) < 𝑁))
181180imp 444 . . . . . . . . . . 11 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) < 𝑁)
182159, 160, 1813jca 1123 . . . . . . . . . 10 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
183182ex 449 . . . . . . . . 9 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
18410, 183sylbi 207 . . . . . . . 8 (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
185 elfzo0 12703 . . . . . . . 8 ((𝐽 + 1) ∈ (0..^𝑁) ↔ ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
186184, 185syl6ibr 242 . . . . . . 7 (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
1879, 186syl 17 . . . . . 6 (𝜑 → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
188187impcom 445 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) ∈ (0..^𝑁))
1895a1i 11 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 = (𝐽 + 1))
19018eqcomd 2766 . . . . . . 7 (𝜑 → (♯‘𝐹) = 𝑁)
191190oveq2d 6829 . . . . . 6 (𝜑 → (0..^(♯‘𝐹)) = (0..^𝑁))
192191adantl 473 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^(♯‘𝐹)) = (0..^𝑁))
193188, 189, 1923eltr4d 2854 . . . 4 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 ∈ (0..^(♯‘𝐹)))
194 eqid 2760 . . . 4 (𝐹 cyclShift 𝐾) = (𝐹 cyclShift 𝐾)
195 eqid 2760 . . . 4 (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))
1963adantl 473 . . . 4 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
1971, 2, 156, 31, 193, 194, 195, 196eucrctshift 27395 . . 3 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))))
198 simprl 811 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
199 simprr 813 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
200124ad2antlr 765 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
201123oveq1d 6828 . . . . . 6 (𝜑 → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
202201ad2antlr 765 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
203128adantl 473 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
204130adantl 473 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
205204, 132syl 17 . . . . . . . . 9 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
206205, 134syl6eq 2810 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
207206reseq2d 5551 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
208203, 207eqtrd 2794 . . . . . 6 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
209208adantr 472 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
210 eqid 2760 . . . . 5 ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1)))
2111, 2, 198, 199, 113, 200, 202, 209, 138, 210eucrct2eupth1 27396 . . . 4 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1)))(EulerPaths‘𝑆)((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
212141a1i 11 . . . 4 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝐻 = ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1))))
213190oveq1d 6828 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝐹) − 𝐾) = (𝑁𝐾))
214213breq2d 4816 . . . . . . . . . . 11 (𝜑 → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁𝐾)))
215214adantl 473 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁𝐾)))
216190oveq2d 6829 . . . . . . . . . . . 12 (𝜑 → ((𝑥 + 𝐾) − (♯‘𝐹)) = ((𝑥 + 𝐾) − 𝑁))
217216fveq2d 6356 . . . . . . . . . . 11 (𝜑 → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
218217adantl 473 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
219215, 218ifbieq2d 4255 . . . . . . . . 9 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))) = if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
220219mpteq2dv 4897 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
221150eqcomd 2766 . . . . . . . . 9 (𝜑 → (0...(𝑁 − 1)) = (0..^𝑁))
222221adantl 473 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...(𝑁 − 1)) = (0..^𝑁))
223220, 222reseq12d 5552 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)))
22418adantl 473 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘𝐹))
225224oveq2d 6829 . . . . . . . . 9 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...𝑁) = (0...(♯‘𝐹)))
226144, 225syl5sseq 3794 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
227226resmptd 5610 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
228223, 227eqtrd 2794 . . . . . 6 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
229228, 143syl6reqr 2813 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
230229adantr 472 . . . 4 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
231211, 212, 2303brtr4d 4836 . . 3 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝐻(EulerPaths‘𝑆)𝑄)
232197, 231mpdan 705 . 2 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
233155, 232pm2.61ian 866 1 (𝜑𝐻(EulerPaths‘𝑆)𝑄)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1632  wcel 2139  wne 2932  cdif 3712  cun 3713  ifcif 4230  {csn 4321   class class class wbr 4804  cmpt 4881  dom cdm 5266  cres 5268  cima 5269   Fn wfn 6044  wf 6045  cfv 6049  (class class class)co 6813  cc 10126  cr 10127  0cc0 10128  1c1 10129   + caddc 10131   < clt 10266  cle 10267  cmin 10458  cn 11212  0cn0 11484  cz 11569  ...cfz 12519  ..^cfzo 12659  chash 13311  Word cword 13477   cyclShift ccsh 13734  Vtxcvtx 26073  iEdgciedg 26074  Walkscwlks 26702  Trailsctrls 26797  Circuitsccrcts 26890  EulerPathsceupth 27349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ifp 1051  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-inf 8514  df-card 8955  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-n0 11485  df-z 11570  df-uz 11880  df-rp 12026  df-ico 12374  df-fz 12520  df-fzo 12660  df-fl 12787  df-mod 12863  df-hash 13312  df-word 13485  df-concat 13487  df-substr 13489  df-csh 13735  df-wlks 26705  df-trls 26799  df-crcts 26892  df-eupth 27350
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator