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

Theorem eucrct2eupthOLD 27623
 Description: Obsolete version of eucrct2eupth 27624 as of 30-Nov-2022. (Contributed by AV, 17-Mar-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
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)
eucrct2eupthOLD.h 𝐻 = ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1)))
eucrct2eupthOLD.q 𝑄 = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
Assertion
Ref Expression
eucrct2eupthOLD (𝜑𝐻(EulerPaths‘𝑆)𝑄)
Distinct variable groups:   𝑥,𝐹   𝑥,𝐼   𝑥,𝐽   𝑥,𝐾   𝑥,𝑁   𝑥,𝑃   𝑥,𝑉   𝜑,𝑥
Allowed substitution hints:   𝑄(𝑥)   𝑆(𝑥)   𝐺(𝑥)   𝐻(𝑥)

Proof of Theorem eucrct2eupthOLD
StepHypRef Expression
1 eucrct2eupth1.v . . . 4 𝑉 = (Vtx‘𝐺)
2 eucrct2eupth1.i . . . 4 𝐼 = (iEdg‘𝐺)
3 eucrct2eupth1.d . . . . . 6 (𝜑𝐹(EulerPaths‘𝐺)𝑃)
43adantl 475 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
5 eucrct2eupth.k . . . . . . . 8 𝐾 = (𝐽 + 1)
65eqcomi 2834 . . . . . . 7 (𝐽 + 1) = 𝐾
76oveq2i 6916 . . . . . 6 (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝐾)
8 oveq1 6912 . . . . . . . . 9 (𝐽 = (𝑁 − 1) → (𝐽 + 1) = ((𝑁 − 1) + 1))
9 eucrct2eupth.j . . . . . . . . . 10 (𝜑𝐽 ∈ (0..^𝑁))
10 elfzo0 12804 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
11 nncn 11359 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
12113ad2ant2 1170 . . . . . . . . . . 11 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℂ)
1310, 12sylbi 209 . . . . . . . . . 10 (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℂ)
14 npcan1 10779 . . . . . . . . . 10 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
159, 13, 143syl 18 . . . . . . . . 9 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
168, 15sylan9eq 2881 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) = 𝑁)
1716oveq2d 6921 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝑁))
18 eucrct2eupth.n . . . . . . . . . 10 (𝜑𝑁 = (♯‘𝐹))
1918oveq2d 6921 . . . . . . . . 9 (𝜑 → (𝐹 cyclShift 𝑁) = (𝐹 cyclShift (♯‘𝐹)))
20 eucrct2eupth1.c . . . . . . . . . . 11 (𝜑𝐹(Circuits‘𝐺)𝑃)
21 crctiswlk 27098 . . . . . . . . . . . 12 (𝐹(Circuits‘𝐺)𝑃𝐹(Walks‘𝐺)𝑃)
222wlkf 26912 . . . . . . . . . . . 12 (𝐹(Walks‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
2321, 22syl 17 . . . . . . . . . . 11 (𝐹(Circuits‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
2420, 23syl 17 . . . . . . . . . 10 (𝜑𝐹 ∈ Word dom 𝐼)
25 cshwn 13918 . . . . . . . . . 10 (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
2624, 25syl 17 . . . . . . . . 9 (𝜑 → (𝐹 cyclShift (♯‘𝐹)) = 𝐹)
2719, 26eqtrd 2861 . . . . . . . 8 (𝜑 → (𝐹 cyclShift 𝑁) = 𝐹)
2827adantl 475 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝑁) = 𝐹)
2917, 28eqtrd 2861 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = 𝐹)
307, 29syl5eqr 2875 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾) = 𝐹)
31 eqid 2825 . . . . . . . . . . . . . 14 (♯‘𝐹) = (♯‘𝐹)
321, 2, 20, 31crctcshlem1 27116 . . . . . . . . . . . . 13 (𝜑 → (♯‘𝐹) ∈ ℕ0)
33 fz0sn0fz1 12751 . . . . . . . . . . . . 13 ((♯‘𝐹) ∈ ℕ0 → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
3432, 33syl 17 . . . . . . . . . . . 12 (𝜑 → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
3534eleq2d 2892 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ 𝑥 ∈ ({0} ∪ (1...(♯‘𝐹)))))
36 elun 3980 . . . . . . . . . . 11 (𝑥 ∈ ({0} ∪ (1...(♯‘𝐹))) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))))
3735, 36syl6bb 279 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹)))))
38 elsni 4414 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {0} → 𝑥 = 0)
39 0le0 11459 . . . . . . . . . . . . . . . 16 0 ≤ 0
4038, 39syl6eqbr 4912 . . . . . . . . . . . . . . 15 (𝑥 ∈ {0} → 𝑥 ≤ 0)
4140adantl 475 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ {0}) → 𝑥 ≤ 0)
4241iftrued 4314 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘(𝑥 + 𝑁)))
4318fveq2d 6437 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑃𝑁) = (𝑃‘(♯‘𝐹)))
44 crctprop 27094 . . . . . . . . . . . . . . . . . 18 (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
45 simpr 479 . . . . . . . . . . . . . . . . . . 19 ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘0) = (𝑃‘(♯‘𝐹)))
4645eqcomd 2831 . . . . . . . . . . . . . . . . . 18 ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
4720, 44, 463syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑃‘(♯‘𝐹)) = (𝑃‘0))
4843, 47eqtrd 2861 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃𝑁) = (𝑃‘0))
4948adantr 474 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 0) → (𝑃𝑁) = (𝑃‘0))
50 oveq1 6912 . . . . . . . . . . . . . . . . 17 (𝑥 = 0 → (𝑥 + 𝑁) = (0 + 𝑁))
519, 13syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℂ)
5251addid2d 10556 . . . . . . . . . . . . . . . . 17 (𝜑 → (0 + 𝑁) = 𝑁)
5350, 52sylan9eqr 2883 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 = 0) → (𝑥 + 𝑁) = 𝑁)
5453fveq2d 6437 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃𝑁))
55 fveq2 6433 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → (𝑃𝑥) = (𝑃‘0))
5655adantl 475 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 0) → (𝑃𝑥) = (𝑃‘0))
5749, 54, 563eqtr4d 2871 . . . . . . . . . . . . . 14 ((𝜑𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃𝑥))
5838, 57sylan2 588 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ {0}) → (𝑃‘(𝑥 + 𝑁)) = (𝑃𝑥))
5942, 58eqtrd 2861 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥))
6059ex 403 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ {0} → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
61 elfznn 12663 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℕ)
62 nnnle0 11385 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → ¬ 𝑥 ≤ 0)
6361, 62syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1...(♯‘𝐹)) → ¬ 𝑥 ≤ 0)
6463adantl 475 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → ¬ 𝑥 ≤ 0)
6564iffalsed 4317 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
6661nncnd 11368 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...(♯‘𝐹)) → 𝑥 ∈ ℂ)
6766adantl 475 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → 𝑥 ∈ ℂ)
6851adantr 474 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → 𝑁 ∈ ℂ)
6967, 68pncand 10714 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → ((𝑥 + 𝑁) − 𝑁) = 𝑥)
7069fveq2d 6437 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → (𝑃‘((𝑥 + 𝑁) − 𝑁)) = (𝑃𝑥))
7165, 70eqtrd 2861 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥))
7271ex 403 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (1...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
7360, 72jaod 892 . . . . . . . . . 10 (𝜑 → ((𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
7437, 73sylbid 232 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
7574imp 397 . . . . . . . 8 ((𝜑𝑥 ∈ (0...(♯‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥))
7675mpteq2dva 4967 . . . . . . 7 (𝜑 → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃𝑥)))
7776adantl 475 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃𝑥)))
785oveq2i 6916 . . . . . . . . . 10 (𝑁𝐾) = (𝑁 − (𝐽 + 1))
798oveq2d 6921 . . . . . . . . . . 11 (𝐽 = (𝑁 − 1) → (𝑁 − (𝐽 + 1)) = (𝑁 − ((𝑁 − 1) + 1)))
8015oveq2d 6921 . . . . . . . . . . . 12 (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = (𝑁𝑁))
8151subidd 10701 . . . . . . . . . . . 12 (𝜑 → (𝑁𝑁) = 0)
8280, 81eqtrd 2861 . . . . . . . . . . 11 (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = 0)
8379, 82sylan9eq 2881 . . . . . . . . . 10 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − (𝐽 + 1)) = 0)
8478, 83syl5eq 2873 . . . . . . . . 9 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁𝐾) = 0)
8584breq2d 4885 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ (𝑁𝐾) ↔ 𝑥 ≤ 0))
865oveq2i 6916 . . . . . . . . . 10 (𝑥 + 𝐾) = (𝑥 + (𝐽 + 1))
8786fveq2i 6436 . . . . . . . . 9 (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + (𝐽 + 1)))
888oveq2d 6921 . . . . . . . . . . 11 (𝐽 = (𝑁 − 1) → (𝑥 + (𝐽 + 1)) = (𝑥 + ((𝑁 − 1) + 1)))
8915oveq2d 6921 . . . . . . . . . . 11 (𝜑 → (𝑥 + ((𝑁 − 1) + 1)) = (𝑥 + 𝑁))
9088, 89sylan9eq 2881 . . . . . . . . . 10 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 + (𝐽 + 1)) = (𝑥 + 𝑁))
9190fveq2d 6437 . . . . . . . . 9 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + (𝐽 + 1))) = (𝑃‘(𝑥 + 𝑁)))
9287, 91syl5eq 2873 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + 𝑁)))
9386oveq1i 6915 . . . . . . . . . 10 ((𝑥 + 𝐾) − 𝑁) = ((𝑥 + (𝐽 + 1)) − 𝑁)
9493fveq2i 6436 . . . . . . . . 9 (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁))
9588oveq1d 6920 . . . . . . . . . . 11 (𝐽 = (𝑁 − 1) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁))
9689oveq1d 6920 . . . . . . . . . . 11 (𝜑 → ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
9795, 96sylan9eq 2881 . . . . . . . . . 10 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
9897fveq2d 6437 . . . . . . . . 9 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
9994, 98syl5eq 2873 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
10085, 92, 99ifbieq12d 4333 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))) = if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))))
101100mpteq2dv 4968 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))))
10220, 21syl 17 . . . . . . . . 9 (𝜑𝐹(Walks‘𝐺)𝑃)
1031wlkp 26914 . . . . . . . . 9 (𝐹(Walks‘𝐺)𝑃𝑃:(0...(♯‘𝐹))⟶𝑉)
104 ffn 6278 . . . . . . . . 9 (𝑃:(0...(♯‘𝐹))⟶𝑉𝑃 Fn (0...(♯‘𝐹)))
105102, 103, 1043syl 18 . . . . . . . 8 (𝜑𝑃 Fn (0...(♯‘𝐹)))
106105adantl 475 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 Fn (0...(♯‘𝐹)))
107 dffn5 6488 . . . . . . 7 (𝑃 Fn (0...(♯‘𝐹)) ↔ 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃𝑥)))
108106, 107sylib 210 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 = (𝑥 ∈ (0...(♯‘𝐹)) ↦ (𝑃𝑥)))
10977, 101, 1083eqtr4d 2871 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = 𝑃)
1104, 30, 1093brtr4d 4905 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
11120adantl 475 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
112111, 30, 1093brtr4d 4905 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
113 eucrct2eupth1.s . . . 4 (Vtx‘𝑆) = 𝑉
114 elfzolt3 12775 . . . . . . 7 (𝐽 ∈ (0..^𝑁) → 0 < 𝑁)
1159, 114syl 17 . . . . . 6 (𝜑 → 0 < 𝑁)
116 elfzoelz 12765 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
1179, 116syl 17 . . . . . . . . . 10 (𝜑𝐽 ∈ ℤ)
118117peano2zd 11813 . . . . . . . . 9 (𝜑 → (𝐽 + 1) ∈ ℤ)
1195, 118syl5eqel 2910 . . . . . . . 8 (𝜑𝐾 ∈ ℤ)
120 cshwlen 13920 . . . . . . . . 9 ((𝐹 ∈ Word dom 𝐼𝐾 ∈ ℤ) → (♯‘(𝐹 cyclShift 𝐾)) = (♯‘𝐹))
121120eqcomd 2831 . . . . . . . 8 ((𝐹 ∈ Word dom 𝐼𝐾 ∈ ℤ) → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
12224, 119, 121syl2anc 581 . . . . . . 7 (𝜑 → (♯‘𝐹) = (♯‘(𝐹 cyclShift 𝐾)))
12318, 122eqtrd 2861 . . . . . 6 (𝜑𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
124115, 123breqtrd 4899 . . . . 5 (𝜑 → 0 < (♯‘(𝐹 cyclShift 𝐾)))
125124adantl 475 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
126123adantl 475 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘(𝐹 cyclShift 𝐾)))
127126oveq1d 6920 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
128 eucrct2eupth.e . . . . . 6 (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
129128adantl 475 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
13024, 18, 93jca 1164 . . . . . . . . 9 (𝜑 → (𝐹 ∈ Word dom 𝐼𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
131130adantl 475 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
132 cshimadifsn0 13951 . . . . . . . 8 ((𝐹 ∈ Word dom 𝐼𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
133131, 132syl 17 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
1347imaeq1i 5704 . . . . . . 7 ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))
135133, 134syl6eq 2877 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
136135reseq2d 5629 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
137129, 136eqtrd 2861 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
138 eqid 2825 . . . 4 ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1)))
139 eqid 2825 . . . 4 ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))
1401, 2, 110, 112, 113, 125, 127, 137, 138, 139eucrct2eupth1OLD 27622 . . 3 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1)))(EulerPaths‘𝑆)((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
141 eucrct2eupthOLD.h . . . 4 𝐻 = ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1)))
142141a1i 11 . . 3 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻 = ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1))))
143 eucrct2eupthOLD.q . . . . 5 𝑄 = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
144 fzossfz 12783 . . . . . . . 8 (0..^𝑁) ⊆ (0...𝑁)
14518oveq2d 6921 . . . . . . . 8 (𝜑 → (0...𝑁) = (0...(♯‘𝐹)))
146144, 145syl5sseq 3878 . . . . . . 7 (𝜑 → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
147146resmptd 5689 . . . . . 6 (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
148 elfzoel2 12764 . . . . . . . 8 (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
149 fzoval 12766 . . . . . . . 8 (𝑁 ∈ ℤ → (0..^𝑁) = (0...(𝑁 − 1)))
1509, 148, 1493syl 18 . . . . . . 7 (𝜑 → (0..^𝑁) = (0...(𝑁 − 1)))
151150reseq2d 5629 . . . . . 6 (𝜑 → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
152147, 151eqtr3d 2863 . . . . 5 (𝜑 → (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
153143, 152syl5eq 2873 . . . 4 (𝜑𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
154153adantl 475 . . 3 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
155140, 142, 1543brtr4d 4905 . 2 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
15620adantl 475 . . . 4 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(Circuits‘𝐺)𝑃)
157 peano2nn0 11660 . . . . . . . . . . . . 13 (𝐽 ∈ ℕ0 → (𝐽 + 1) ∈ ℕ0)
1581573ad2ant1 1169 . . . . . . . . . . . 12 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℕ0)
159158adantr 474 . . . . . . . . . . 11 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) ∈ ℕ0)
160 simpl2 1250 . . . . . . . . . . 11 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → 𝑁 ∈ ℕ)
161 1cnd 10351 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 1 ∈ ℂ)
162 nn0cn 11629 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ ℕ0𝐽 ∈ ℂ)
1631623ad2ant1 1169 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝐽 ∈ ℂ)
16412, 161, 163subadd2d 10732 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝑁 − 1) = 𝐽 ↔ (𝐽 + 1) = 𝑁))
165 eqcom 2832 . . . . . . . . . . . . . . 15 (𝐽 = (𝑁 − 1) ↔ (𝑁 − 1) = 𝐽)
166 eqcom 2832 . . . . . . . . . . . . . . 15 (𝑁 = (𝐽 + 1) ↔ (𝐽 + 1) = 𝑁)
167164, 165, 1663bitr4g 306 . . . . . . . . . . . . . 14 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 = (𝑁 − 1) ↔ 𝑁 = (𝐽 + 1)))
168167necon3bbid 3036 . . . . . . . . . . . . 13 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) ↔ 𝑁 ≠ (𝐽 + 1)))
169157nn0red 11679 . . . . . . . . . . . . . . . 16 (𝐽 ∈ ℕ0 → (𝐽 + 1) ∈ ℝ)
1701693ad2ant1 1169 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℝ)
171 nnre 11358 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
1721713ad2ant2 1170 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℝ)
173 nn0z 11728 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ ℕ0𝐽 ∈ ℤ)
174 nnz 11727 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
175 zltp1le 11755 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
176173, 174, 175syl2an 591 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
177176biimp3a 1599 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ≤ 𝑁)
178170, 172, 177leltned 10509 . . . . . . . . . . . . . 14 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝐽 + 1) < 𝑁𝑁 ≠ (𝐽 + 1)))
179178biimprd 240 . . . . . . . . . . . . 13 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝑁 ≠ (𝐽 + 1) → (𝐽 + 1) < 𝑁))
180168, 179sylbid 232 . . . . . . . . . . . 12 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) < 𝑁))
181180imp 397 . . . . . . . . . . 11 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) < 𝑁)
182159, 160, 1813jca 1164 . . . . . . . . . 10 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
183182ex 403 . . . . . . . . 9 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
18410, 183sylbi 209 . . . . . . . 8 (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
185 elfzo0 12804 . . . . . . . 8 ((𝐽 + 1) ∈ (0..^𝑁) ↔ ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
186184, 185syl6ibr 244 . . . . . . 7 (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
1879, 186syl 17 . . . . . 6 (𝜑 → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
188187impcom 398 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) ∈ (0..^𝑁))
1895a1i 11 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 = (𝐽 + 1))
19018eqcomd 2831 . . . . . . 7 (𝜑 → (♯‘𝐹) = 𝑁)
191190oveq2d 6921 . . . . . 6 (𝜑 → (0..^(♯‘𝐹)) = (0..^𝑁))
192191adantl 475 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^(♯‘𝐹)) = (0..^𝑁))
193188, 189, 1923eltr4d 2921 . . . 4 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 ∈ (0..^(♯‘𝐹)))
194 eqid 2825 . . . 4 (𝐹 cyclShift 𝐾) = (𝐹 cyclShift 𝐾)
195 eqid 2825 . . . 4 (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))
1963adantl 475 . . . 4 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
1971, 2, 156, 31, 193, 194, 195, 196eucrctshift 27620 . . 3 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))))))
198 simprl 789 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
199 simprr 791 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))
200124ad2antlr 720 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 0 < (♯‘(𝐹 cyclShift 𝐾)))
201123oveq1d 6920 . . . . . 6 (𝜑 → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
202201ad2antlr 720 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (𝑁 − 1) = ((♯‘(𝐹 cyclShift 𝐾)) − 1))
203128adantl 475 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
204130adantl 475 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
205204, 132syl 17 . . . . . . . . 9 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
206205, 134syl6eq 2877 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
207206reseq2d 5629 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
208203, 207eqtrd 2861 . . . . . 6 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
209208adantr 474 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
210 eqid 2825 . . . . 5 ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1)))
2111, 2, 198, 199, 113, 200, 202, 209, 138, 210eucrct2eupth1OLD 27622 . . . 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 6920 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝐹) − 𝐾) = (𝑁𝐾))
214213breq2d 4885 . . . . . . . . . . 11 (𝜑 → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁𝐾)))
215214adantl 475 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ ((♯‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁𝐾)))
216190oveq2d 6921 . . . . . . . . . . . 12 (𝜑 → ((𝑥 + 𝐾) − (♯‘𝐹)) = ((𝑥 + 𝐾) − 𝑁))
217216fveq2d 6437 . . . . . . . . . . 11 (𝜑 → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
218217adantl 475 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
219215, 218ifbieq2d 4331 . . . . . . . . 9 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹)))) = if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
220219mpteq2dv 4968 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) = (𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
221150eqcomd 2831 . . . . . . . . 9 (𝜑 → (0...(𝑁 − 1)) = (0..^𝑁))
222221adantl 475 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...(𝑁 − 1)) = (0..^𝑁))
223220, 222reseq12d 5630 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)))
22418adantl 475 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (♯‘𝐹))
225224oveq2d 6921 . . . . . . . . 9 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...𝑁) = (0...(♯‘𝐹)))
226144, 225syl5sseq 3878 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^𝑁) ⊆ (0...(♯‘𝐹)))
227226resmptd 5689 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
228223, 227eqtrd 2861 . . . . . 6 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
229228, 143syl6reqr 2880 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
230229adantr 474 . . . 4 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝑄 = ((𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ↾ (0...(𝑁 − 1))))
231211, 212, 2303brtr4d 4905 . . 3 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(Circuits‘𝐺)(𝑥 ∈ (0...(♯‘𝐹)) ↦ if(𝑥 ≤ ((♯‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (♯‘𝐹))))))) → 𝐻(EulerPaths‘𝑆)𝑄)
232197, 231mpdan 680 . 2 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
233155, 232pm2.61ian 848 1 (𝜑𝐻(EulerPaths‘𝑆)𝑄)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 880   ∧ w3a 1113   = wceq 1658   ∈ wcel 2166   ≠ wne 2999   ∖ cdif 3795   ∪ cun 3796  ifcif 4306  {csn 4397   class class class wbr 4873   ↦ cmpt 4952  dom cdm 5342   ↾ cres 5344   “ cima 5345   Fn wfn 6118  ⟶wf 6119  ‘cfv 6123  (class class class)co 6905  ℂcc 10250  ℝcr 10251  0cc0 10252  1c1 10253   + caddc 10255   < clt 10391   ≤ cle 10392   − cmin 10585  ℕcn 11350  ℕ0cn0 11618  ℤcz 11704  ...cfz 12619  ..^cfzo 12760  ♯chash 13410  Word cword 13574   cyclShift ccsh 13904  Vtxcvtx 26294  iEdgciedg 26295  Walkscwlks 26894  Trailsctrls 26991  Circuitsccrcts 27086  EulerPathsceupth 27573 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-pre-sup 10330 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-ifp 1092  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-oadd 7830  df-er 8009  df-map 8124  df-pm 8125  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-sup 8617  df-inf 8618  df-card 9078  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010  df-nn 11351  df-2 11414  df-n0 11619  df-z 11705  df-uz 11969  df-rp 12113  df-ico 12469  df-fz 12620  df-fzo 12761  df-fl 12888  df-mod 12964  df-hash 13411  df-word 13575  df-concat 13631  df-substr 13701  df-pfx 13750  df-csh 13906  df-wlks 26897  df-trls 26993  df-crcts 27088  df-eupth 27574 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator