Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  eucrct2eupth Structured version   Visualization version   GIF version

Theorem eucrct2eupth 41413
 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 481 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
5 eucrct2eupth.k . . . . . . . 8 𝐾 = (𝐽 + 1)
65eqcomi 2619 . . . . . . 7 (𝐽 + 1) = 𝐾
76oveq2i 6560 . . . . . 6 (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝐾)
8 oveq1 6556 . . . . . . . . 9 (𝐽 = (𝑁 − 1) → (𝐽 + 1) = ((𝑁 − 1) + 1))
9 eucrct2eupth.j . . . . . . . . . 10 (𝜑𝐽 ∈ (0..^𝑁))
10 elfzo0 12376 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) ↔ (𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁))
11 nncn 10905 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
12113ad2ant2 1076 . . . . . . . . . . 11 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℂ)
1310, 12sylbi 206 . . . . . . . . . 10 (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℂ)
14 npcan1 10334 . . . . . . . . . 10 (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
159, 13, 143syl 18 . . . . . . . . 9 (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
168, 15sylan9eq 2664 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) = 𝑁)
1716oveq2d 6565 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = (𝐹 cyclShift 𝑁))
18 eucrct2eupth.n . . . . . . . . . 10 (𝜑𝑁 = (#‘𝐹))
1918oveq2d 6565 . . . . . . . . 9 (𝜑 → (𝐹 cyclShift 𝑁) = (𝐹 cyclShift (#‘𝐹)))
20 eucrct2eupth1.c . . . . . . . . . . 11 (𝜑𝐹(CircuitS‘𝐺)𝑃)
21 crctis1wlk 41002 . . . . . . . . . . . 12 (𝐹(CircuitS‘𝐺)𝑃𝐹(1Walks‘𝐺)𝑃)
2221wlkf 40819 . . . . . . . . . . . 12 (𝐹(1Walks‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
2321, 22syl 17 . . . . . . . . . . 11 (𝐹(CircuitS‘𝐺)𝑃𝐹 ∈ Word dom 𝐼)
2420, 23syl 17 . . . . . . . . . 10 (𝜑𝐹 ∈ Word dom 𝐼)
25 cshwn 13394 . . . . . . . . . 10 (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift (#‘𝐹)) = 𝐹)
2624, 25syl 17 . . . . . . . . 9 (𝜑 → (𝐹 cyclShift (#‘𝐹)) = 𝐹)
2719, 26eqtrd 2644 . . . . . . . 8 (𝜑 → (𝐹 cyclShift 𝑁) = 𝐹)
2827adantl 481 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝑁) = 𝐹)
2917, 28eqtrd 2644 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift (𝐽 + 1)) = 𝐹)
307, 29syl5eqr 2658 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾) = 𝐹)
31 eqid 2610 . . . . . . . . . . . . . 14 (#‘𝐹) = (#‘𝐹)
321, 2, 20, 31crctcshlem1 41020 . . . . . . . . . . . . 13 (𝜑 → (#‘𝐹) ∈ ℕ0)
33 fz0sn0fz1 12325 . . . . . . . . . . . . 13 ((#‘𝐹) ∈ ℕ0 → (0...(#‘𝐹)) = ({0} ∪ (1...(#‘𝐹))))
3432, 33syl 17 . . . . . . . . . . . 12 (𝜑 → (0...(#‘𝐹)) = ({0} ∪ (1...(#‘𝐹))))
3534eleq2d 2673 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (0...(#‘𝐹)) ↔ 𝑥 ∈ ({0} ∪ (1...(#‘𝐹)))))
36 elun 3715 . . . . . . . . . . 11 (𝑥 ∈ ({0} ∪ (1...(#‘𝐹))) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(#‘𝐹))))
3735, 36syl6bb 275 . . . . . . . . . 10 (𝜑 → (𝑥 ∈ (0...(#‘𝐹)) ↔ (𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(#‘𝐹)))))
38 elsni 4142 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {0} → 𝑥 = 0)
39 0le0 10987 . . . . . . . . . . . . . . . 16 0 ≤ 0
4038, 39syl6eqbr 4622 . . . . . . . . . . . . . . 15 (𝑥 ∈ {0} → 𝑥 ≤ 0)
4140adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ {0}) → 𝑥 ≤ 0)
4241iftrued 4044 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘(𝑥 + 𝑁)))
4318fveq2d 6107 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑃𝑁) = (𝑃‘(#‘𝐹)))
44 crctprop 40998 . . . . . . . . . . . . . . . . . 18 (𝐹(CircuitS‘𝐺)𝑃 → (𝐹(TrailS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))
45 simpr 476 . . . . . . . . . . . . . . . . . . 19 ((𝐹(TrailS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝑃‘0) = (𝑃‘(#‘𝐹)))
4645eqcomd 2616 . . . . . . . . . . . . . . . . . 18 ((𝐹(TrailS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝑃‘(#‘𝐹)) = (𝑃‘0))
4720, 44, 463syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑃‘(#‘𝐹)) = (𝑃‘0))
4843, 47eqtrd 2644 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑃𝑁) = (𝑃‘0))
4948adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 0) → (𝑃𝑁) = (𝑃‘0))
50 oveq1 6556 . . . . . . . . . . . . . . . . 17 (𝑥 = 0 → (𝑥 + 𝑁) = (0 + 𝑁))
519, 13syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℂ)
5251addid2d 10116 . . . . . . . . . . . . . . . . 17 (𝜑 → (0 + 𝑁) = 𝑁)
5350, 52sylan9eqr 2666 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 = 0) → (𝑥 + 𝑁) = 𝑁)
5453fveq2d 6107 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃𝑁))
55 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑥 = 0 → (𝑃𝑥) = (𝑃‘0))
5655adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 = 0) → (𝑃𝑥) = (𝑃‘0))
5749, 54, 563eqtr4d 2654 . . . . . . . . . . . . . 14 ((𝜑𝑥 = 0) → (𝑃‘(𝑥 + 𝑁)) = (𝑃𝑥))
5838, 57sylan2 490 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ {0}) → (𝑃‘(𝑥 + 𝑁)) = (𝑃𝑥))
5942, 58eqtrd 2644 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ {0}) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥))
6059ex 449 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ {0} → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
61 elfznn 12241 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...(#‘𝐹)) → 𝑥 ∈ ℕ)
62 nnnle0 10928 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → ¬ 𝑥 ≤ 0)
6361, 62syl 17 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1...(#‘𝐹)) → ¬ 𝑥 ≤ 0)
6463adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...(#‘𝐹))) → ¬ 𝑥 ≤ 0)
6564iffalsed 4047 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...(#‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
6661nncnd 10913 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...(#‘𝐹)) → 𝑥 ∈ ℂ)
6766adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...(#‘𝐹))) → 𝑥 ∈ ℂ)
6851adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (1...(#‘𝐹))) → 𝑁 ∈ ℂ)
6967, 68pncand 10272 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ (1...(#‘𝐹))) → ((𝑥 + 𝑁) − 𝑁) = 𝑥)
7069fveq2d 6107 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ (1...(#‘𝐹))) → (𝑃‘((𝑥 + 𝑁) − 𝑁)) = (𝑃𝑥))
7165, 70eqtrd 2644 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...(#‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥))
7271ex 449 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (1...(#‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
7360, 72jaod 394 . . . . . . . . . 10 (𝜑 → ((𝑥 ∈ {0} ∨ 𝑥 ∈ (1...(#‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
7437, 73sylbid 229 . . . . . . . . 9 (𝜑 → (𝑥 ∈ (0...(#‘𝐹)) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥)))
7574imp 444 . . . . . . . 8 ((𝜑𝑥 ∈ (0...(#‘𝐹))) → if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))) = (𝑃𝑥))
7675mpteq2dva 4672 . . . . . . 7 (𝜑 → (𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(#‘𝐹)) ↦ (𝑃𝑥)))
7776adantl 481 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))) = (𝑥 ∈ (0...(#‘𝐹)) ↦ (𝑃𝑥)))
785oveq2i 6560 . . . . . . . . . 10 (𝑁𝐾) = (𝑁 − (𝐽 + 1))
798oveq2d 6565 . . . . . . . . . . 11 (𝐽 = (𝑁 − 1) → (𝑁 − (𝐽 + 1)) = (𝑁 − ((𝑁 − 1) + 1)))
8015oveq2d 6565 . . . . . . . . . . . 12 (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = (𝑁𝑁))
8151subidd 10259 . . . . . . . . . . . 12 (𝜑 → (𝑁𝑁) = 0)
8280, 81eqtrd 2644 . . . . . . . . . . 11 (𝜑 → (𝑁 − ((𝑁 − 1) + 1)) = 0)
8379, 82sylan9eq 2664 . . . . . . . . . 10 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − (𝐽 + 1)) = 0)
8478, 83syl5eq 2656 . . . . . . . . 9 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁𝐾) = 0)
8584breq2d 4595 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ (𝑁𝐾) ↔ 𝑥 ≤ 0))
865oveq2i 6560 . . . . . . . . . 10 (𝑥 + 𝐾) = (𝑥 + (𝐽 + 1))
8786fveq2i 6106 . . . . . . . . 9 (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + (𝐽 + 1)))
888oveq2d 6565 . . . . . . . . . . 11 (𝐽 = (𝑁 − 1) → (𝑥 + (𝐽 + 1)) = (𝑥 + ((𝑁 − 1) + 1)))
8915oveq2d 6565 . . . . . . . . . . 11 (𝜑 → (𝑥 + ((𝑁 − 1) + 1)) = (𝑥 + 𝑁))
9088, 89sylan9eq 2664 . . . . . . . . . 10 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 + (𝐽 + 1)) = (𝑥 + 𝑁))
9190fveq2d 6107 . . . . . . . . 9 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + (𝐽 + 1))) = (𝑃‘(𝑥 + 𝑁)))
9287, 91syl5eq 2656 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘(𝑥 + 𝐾)) = (𝑃‘(𝑥 + 𝑁)))
9386oveq1i 6559 . . . . . . . . . 10 ((𝑥 + 𝐾) − 𝑁) = ((𝑥 + (𝐽 + 1)) − 𝑁)
9493fveq2i 6106 . . . . . . . . 9 (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁))
9588oveq1d 6564 . . . . . . . . . . 11 (𝐽 = (𝑁 − 1) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁))
9689oveq1d 6564 . . . . . . . . . . 11 (𝜑 → ((𝑥 + ((𝑁 − 1) + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
9795, 96sylan9eq 2664 . . . . . . . . . 10 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 + (𝐽 + 1)) − 𝑁) = ((𝑥 + 𝑁) − 𝑁))
9897fveq2d 6107 . . . . . . . . 9 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + (𝐽 + 1)) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
9994, 98syl5eq 2656 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − 𝑁)) = (𝑃‘((𝑥 + 𝑁) − 𝑁)))
10085, 92, 99ifbieq12d 4063 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))) = if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁))))
101100mpteq2dv 4673 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = (𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ 0, (𝑃‘(𝑥 + 𝑁)), (𝑃‘((𝑥 + 𝑁) − 𝑁)))))
10220, 21syl 17 . . . . . . . . 9 (𝜑𝐹(1Walks‘𝐺)𝑃)
10311wlkp 40821 . . . . . . . . 9 (𝐹(1Walks‘𝐺)𝑃𝑃:(0...(#‘𝐹))⟶𝑉)
104 ffn 5958 . . . . . . . . 9 (𝑃:(0...(#‘𝐹))⟶𝑉𝑃 Fn (0...(#‘𝐹)))
105102, 103, 1043syl 18 . . . . . . . 8 (𝜑𝑃 Fn (0...(#‘𝐹)))
106105adantl 481 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 Fn (0...(#‘𝐹)))
107 dffn5 6151 . . . . . . 7 (𝑃 Fn (0...(#‘𝐹)) ↔ 𝑃 = (𝑥 ∈ (0...(#‘𝐹)) ↦ (𝑃𝑥)))
108106, 107sylib 207 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑃 = (𝑥 ∈ (0...(#‘𝐹)) ↦ (𝑃𝑥)))
10977, 101, 1083eqtr4d 2654 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = 𝑃)
1104, 30, 1093brtr4d 4615 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
11120adantl 481 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(CircuitS‘𝐺)𝑃)
112111, 30, 1093brtr4d 4615 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 cyclShift 𝐾)(CircuitS‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
113 eucrct2eupth1.s . . . 4 (Vtx‘𝑆) = 𝑉
114 elfzolt3 12349 . . . . . . 7 (𝐽 ∈ (0..^𝑁) → 0 < 𝑁)
1159, 114syl 17 . . . . . 6 (𝜑 → 0 < 𝑁)
116 elfzoelz 12339 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
1179, 116syl 17 . . . . . . . . . 10 (𝜑𝐽 ∈ ℤ)
118117peano2zd 11361 . . . . . . . . 9 (𝜑 → (𝐽 + 1) ∈ ℤ)
1195, 118syl5eqel 2692 . . . . . . . 8 (𝜑𝐾 ∈ ℤ)
120 cshwlen 13396 . . . . . . . . 9 ((𝐹 ∈ Word dom 𝐼𝐾 ∈ ℤ) → (#‘(𝐹 cyclShift 𝐾)) = (#‘𝐹))
121120eqcomd 2616 . . . . . . . 8 ((𝐹 ∈ Word dom 𝐼𝐾 ∈ ℤ) → (#‘𝐹) = (#‘(𝐹 cyclShift 𝐾)))
12224, 119, 121syl2anc 691 . . . . . . 7 (𝜑 → (#‘𝐹) = (#‘(𝐹 cyclShift 𝐾)))
12318, 122eqtrd 2644 . . . . . 6 (𝜑𝑁 = (#‘(𝐹 cyclShift 𝐾)))
124115, 123breqtrd 4609 . . . . 5 (𝜑 → 0 < (#‘(𝐹 cyclShift 𝐾)))
125124adantl 481 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 0 < (#‘(𝐹 cyclShift 𝐾)))
126123adantl 481 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (#‘(𝐹 cyclShift 𝐾)))
127126oveq1d 6564 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑁 − 1) = ((#‘(𝐹 cyclShift 𝐾)) − 1))
128 eucrct2eupth.e . . . . . 6 (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
129128adantl 481 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
13024, 18, 93jca 1235 . . . . . . . . 9 (𝜑 → (𝐹 ∈ Word dom 𝐼𝑁 = (#‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
131130adantl 481 . . . . . . . 8 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼𝑁 = (#‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
132 cshimadifsn0 13427 . . . . . . . 8 ((𝐹 ∈ Word dom 𝐼𝑁 = (#‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
133131, 132syl 17 . . . . . . 7 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
1347imaeq1i 5382 . . . . . . 7 ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))
135133, 134syl6eq 2660 . . . . . 6 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
136135reseq2d 5317 . . . . 5 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
137129, 136eqtrd 2644 . . . 4 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
138 eqid 2610 . . . 4 ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1))) = ((𝐹 cyclShift 𝐾) ↾ (0..^(𝑁 − 1)))
139 eqid 2610 . . . 4 ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1)))
1401, 2, 110, 112, 113, 125, 127, 137, 138, 139eucrct2eupth1 41412 . . 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 12357 . . . . . . . 8 (0..^𝑁) ⊆ (0...𝑁)
14518oveq2d 6565 . . . . . . . 8 (𝜑 → (0...𝑁) = (0...(#‘𝐹)))
146144, 145syl5sseq 3616 . . . . . . 7 (𝜑 → (0..^𝑁) ⊆ (0...(#‘𝐹)))
147146resmptd 5371 . . . . . 6 (𝜑 → ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
148 elfzoel2 12338 . . . . . . . 8 (𝐽 ∈ (0..^𝑁) → 𝑁 ∈ ℤ)
149 fzoval 12340 . . . . . . . 8 (𝑁 ∈ ℤ → (0..^𝑁) = (0...(𝑁 − 1)))
1509, 148, 1493syl 18 . . . . . . 7 (𝜑 → (0..^𝑁) = (0...(𝑁 − 1)))
151150reseq2d 5317 . . . . . 6 (𝜑 → ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
152147, 151eqtr3d 2646 . . . . 5 (𝜑 → (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) = ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
153143, 152syl5eq 2656 . . . 4 (𝜑𝑄 = ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
154153adantl 481 . . 3 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0...(𝑁 − 1))))
155140, 142, 1543brtr4d 4615 . 2 ((𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
15620adantl 481 . . . 4 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(CircuitS‘𝐺)𝑃)
157 peano2nn0 11210 . . . . . . . . . . . . 13 (𝐽 ∈ ℕ0 → (𝐽 + 1) ∈ ℕ0)
1581573ad2ant1 1075 . . . . . . . . . . . 12 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℕ0)
159158adantr 480 . . . . . . . . . . 11 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) ∈ ℕ0)
160 simpl2 1058 . . . . . . . . . . 11 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → 𝑁 ∈ ℕ)
161 1cnd 9935 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 1 ∈ ℂ)
162 nn0cn 11179 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ ℕ0𝐽 ∈ ℂ)
1631623ad2ant1 1075 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝐽 ∈ ℂ)
16412, 161, 163subadd2d 10290 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝑁 − 1) = 𝐽 ↔ (𝐽 + 1) = 𝑁))
165 eqcom 2617 . . . . . . . . . . . . . . 15 (𝐽 = (𝑁 − 1) ↔ (𝑁 − 1) = 𝐽)
166 eqcom 2617 . . . . . . . . . . . . . . 15 (𝑁 = (𝐽 + 1) ↔ (𝐽 + 1) = 𝑁)
167164, 165, 1663bitr4g 302 . . . . . . . . . . . . . 14 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 = (𝑁 − 1) ↔ 𝑁 = (𝐽 + 1)))
168167necon3bbid 2819 . . . . . . . . . . . . 13 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) ↔ 𝑁 ≠ (𝐽 + 1)))
169157nn0red 11229 . . . . . . . . . . . . . . . 16 (𝐽 ∈ ℕ0 → (𝐽 + 1) ∈ ℝ)
1701693ad2ant1 1075 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ∈ ℝ)
171 nnre 10904 . . . . . . . . . . . . . . . 16 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
1721713ad2ant2 1076 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → 𝑁 ∈ ℝ)
173 nn0z 11277 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ ℕ0𝐽 ∈ ℤ)
174 nnz 11276 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
175 zltp1le 11304 . . . . . . . . . . . . . . . . 17 ((𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
176173, 174, 175syl2an 493 . . . . . . . . . . . . . . . 16 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ) → (𝐽 < 𝑁 ↔ (𝐽 + 1) ≤ 𝑁))
177176biimp3a 1424 . . . . . . . . . . . . . . 15 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝐽 + 1) ≤ 𝑁)
178170, 172, 177leltned 10069 . . . . . . . . . . . . . 14 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → ((𝐽 + 1) < 𝑁𝑁 ≠ (𝐽 + 1)))
179178biimprd 237 . . . . . . . . . . . . 13 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (𝑁 ≠ (𝐽 + 1) → (𝐽 + 1) < 𝑁))
180168, 179sylbid 229 . . . . . . . . . . . 12 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) < 𝑁))
181180imp 444 . . . . . . . . . . 11 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → (𝐽 + 1) < 𝑁)
182159, 160, 1813jca 1235 . . . . . . . . . 10 (((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) ∧ ¬ 𝐽 = (𝑁 − 1)) → ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
183182ex 449 . . . . . . . . 9 ((𝐽 ∈ ℕ0𝑁 ∈ ℕ ∧ 𝐽 < 𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
18410, 183sylbi 206 . . . . . . . 8 (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁)))
185 elfzo0 12376 . . . . . . . 8 ((𝐽 + 1) ∈ (0..^𝑁) ↔ ((𝐽 + 1) ∈ ℕ0𝑁 ∈ ℕ ∧ (𝐽 + 1) < 𝑁))
186184, 185syl6ibr 241 . . . . . . 7 (𝐽 ∈ (0..^𝑁) → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
1879, 186syl 17 . . . . . 6 (𝜑 → (¬ 𝐽 = (𝑁 − 1) → (𝐽 + 1) ∈ (0..^𝑁)))
188187impcom 445 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐽 + 1) ∈ (0..^𝑁))
1895a1i 11 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 = (𝐽 + 1))
19018eqcomd 2616 . . . . . . 7 (𝜑 → (#‘𝐹) = 𝑁)
191190oveq2d 6565 . . . . . 6 (𝜑 → (0..^(#‘𝐹)) = (0..^𝑁))
192191adantl 481 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^(#‘𝐹)) = (0..^𝑁))
193188, 189, 1923eltr4d 2703 . . . 4 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐾 ∈ (0..^(#‘𝐹)))
194 eqid 2610 . . . 4 (𝐹 cyclShift 𝐾) = (𝐹 cyclShift 𝐾)
195 eqid 2610 . . . 4 (𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) = (𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹)))))
1963adantl 481 . . . 4 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐹(EulerPaths‘𝐺)𝑃)
1971, 2, 156, 31, 193, 194, 195, 196eucrctshift 41411 . . 3 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(CircuitS‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹)))))))
198 simprl 790 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(CircuitS‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))))) → (𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))))
199 simprr 792 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(CircuitS‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))))) → (𝐹 cyclShift 𝐾)(CircuitS‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))))
200124ad2antlr 759 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(CircuitS‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))))) → 0 < (#‘(𝐹 cyclShift 𝐾)))
201123oveq1d 6564 . . . . . 6 (𝜑 → (𝑁 − 1) = ((#‘(𝐹 cyclShift 𝐾)) − 1))
202201ad2antlr 759 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(CircuitS‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))))) → (𝑁 − 1) = ((#‘(𝐹 cyclShift 𝐾)) − 1))
203128adantl 481 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))
204130adantl 481 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 ∈ Word dom 𝐼𝑁 = (#‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)))
205204, 132syl 17 . . . . . . . . 9 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
206205, 134syl6eq 2660 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1))))
207206reseq2d 5317 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
208203, 207eqtrd 2644 . . . . . 6 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
209208adantr 480 . . . . 5 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(CircuitS‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))))) → (iEdg‘𝑆) = (𝐼 ↾ ((𝐹 cyclShift 𝐾) “ (0..^(𝑁 − 1)))))
210 eqid 2610 . . . . 5 ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ↾ (0...(𝑁 − 1)))
2111, 2, 198, 199, 113, 200, 202, 209, 138, 210eucrct2eupth1 41412 . . . 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 6564 . . . . . . . . . . . 12 (𝜑 → ((#‘𝐹) − 𝐾) = (𝑁𝐾))
214213breq2d 4595 . . . . . . . . . . 11 (𝜑 → (𝑥 ≤ ((#‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁𝐾)))
215214adantl 481 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ≤ ((#‘𝐹) − 𝐾) ↔ 𝑥 ≤ (𝑁𝐾)))
216190oveq2d 6565 . . . . . . . . . . . 12 (𝜑 → ((𝑥 + 𝐾) − (#‘𝐹)) = ((𝑥 + 𝐾) − 𝑁))
217216fveq2d 6107 . . . . . . . . . . 11 (𝜑 → (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
218217adantl 481 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))) = (𝑃‘((𝑥 + 𝐾) − 𝑁)))
219215, 218ifbieq2d 4061 . . . . . . . . 9 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹)))) = if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))
220219mpteq2dv 4673 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) = (𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
221150eqcomd 2616 . . . . . . . . 9 (𝜑 → (0...(𝑁 − 1)) = (0..^𝑁))
222221adantl 481 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...(𝑁 − 1)) = (0..^𝑁))
223220, 222reseq12d 5318 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ↾ (0...(𝑁 − 1))) = ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)))
22418adantl 481 . . . . . . . . . 10 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑁 = (#‘𝐹))
225224oveq2d 6565 . . . . . . . . 9 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0...𝑁) = (0...(#‘𝐹)))
226144, 225syl5sseq 3616 . . . . . . . 8 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → (0..^𝑁) ⊆ (0...(#‘𝐹)))
227226resmptd 5371 . . . . . . 7 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))) ↾ (0..^𝑁)) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
228223, 227eqtrd 2644 . . . . . 6 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ↾ (0...(𝑁 − 1))) = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁)))))
229228, 143syl6reqr 2663 . . . . 5 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝑄 = ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ↾ (0...(𝑁 − 1))))
230229adantr 480 . . . 4 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(CircuitS‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))))) → 𝑄 = ((𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ↾ (0...(𝑁 − 1))))
231211, 212, 2303brtr4d 4615 . . 3 (((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) ∧ ((𝐹 cyclShift 𝐾)(EulerPaths‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))) ∧ (𝐹 cyclShift 𝐾)(CircuitS‘𝐺)(𝑥 ∈ (0...(#‘𝐹)) ↦ if(𝑥 ≤ ((#‘𝐹) − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − (#‘𝐹))))))) → 𝐻(EulerPaths‘𝑆)𝑄)
232197, 231mpdan 699 . 2 ((¬ 𝐽 = (𝑁 − 1) ∧ 𝜑) → 𝐻(EulerPaths‘𝑆)𝑄)
233155, 232pm2.61ian 827 1 (𝜑𝐻(EulerPaths‘𝑆)𝑄)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780   ∖ cdif 3537   ∪ cun 3538  ifcif 4036  {csn 4125   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038   ↾ cres 5040   “ cima 5041   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℕ0cn0 11169  ℤcz 11254  ...cfz 12197  ..^cfzo 12334  #chash 12979  Word cword 13146   cyclShift ccsh 13385  Vtxcvtx 25673  iEdgciedg 25674  1Walksc1wlks 40796  TrailSctrls 40899  CircuitSccrcts 40990  EulerPathsceupth 41364 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ifp 1007  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-ico 12052  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-hash 12980  df-word 13154  df-concat 13156  df-substr 13158  df-csh 13386  df-1wlks 40800  df-trls 40901  df-crcts 40992  df-eupth 41365 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator