Proof of Theorem crctcshlem4
| Step | Hyp | Ref
| Expression |
| 1 | | crctcsh.h |
. . 3
⊢ 𝐻 = (𝐹 cyclShift 𝑆) |
| 2 | | oveq2 7439 |
. . . 4
⊢ (𝑆 = 0 → (𝐹 cyclShift 𝑆) = (𝐹 cyclShift 0)) |
| 3 | | crctcsh.d |
. . . . 5
⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃) |
| 4 | | crctiswlk 29816 |
. . . . 5
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) |
| 5 | | crctcsh.i |
. . . . . 6
⊢ 𝐼 = (iEdg‘𝐺) |
| 6 | 5 | wlkf 29632 |
. . . . 5
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
| 7 | | cshw0 14832 |
. . . . 5
⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift 0) = 𝐹) |
| 8 | 3, 4, 6, 7 | 4syl 19 |
. . . 4
⊢ (𝜑 → (𝐹 cyclShift 0) = 𝐹) |
| 9 | 2, 8 | sylan9eqr 2799 |
. . 3
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝐹 cyclShift 𝑆) = 𝐹) |
| 10 | 1, 9 | eqtrid 2789 |
. 2
⊢ ((𝜑 ∧ 𝑆 = 0) → 𝐻 = 𝐹) |
| 11 | | crctcsh.q |
. . 3
⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) |
| 12 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑆 = 0 → (𝑁 − 𝑆) = (𝑁 − 0)) |
| 13 | | crctcsh.v |
. . . . . . . . . . . 12
⊢ 𝑉 = (Vtx‘𝐺) |
| 14 | | crctcsh.n |
. . . . . . . . . . . 12
⊢ 𝑁 = (♯‘𝐹) |
| 15 | 13, 5, 3, 14 | crctcshlem1 29837 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 16 | 15 | nn0cnd 12589 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 17 | 16 | subid1d 11609 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − 0) = 𝑁) |
| 18 | 12, 17 | sylan9eqr 2799 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝑁 − 𝑆) = 𝑁) |
| 19 | 18 | breq2d 5155 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝑥 ≤ (𝑁 − 𝑆) ↔ 𝑥 ≤ 𝑁)) |
| 20 | 19 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 = 0) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 ≤ (𝑁 − 𝑆) ↔ 𝑥 ≤ 𝑁)) |
| 21 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑆 = 0 → (𝑥 + 𝑆) = (𝑥 + 0)) |
| 22 | 21 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝑥 + 𝑆) = (𝑥 + 0)) |
| 23 | | elfzelz 13564 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℤ) |
| 24 | 23 | zcnd 12723 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℂ) |
| 25 | 24 | addridd 11461 |
. . . . . . . 8
⊢ (𝑥 ∈ (0...𝑁) → (𝑥 + 0) = 𝑥) |
| 26 | 22, 25 | sylan9eq 2797 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 = 0) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) = 𝑥) |
| 27 | 26 | fveq2d 6910 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 = 0) ∧ 𝑥 ∈ (0...𝑁)) → (𝑃‘(𝑥 + 𝑆)) = (𝑃‘𝑥)) |
| 28 | 26 | fvoveq1d 7453 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 = 0) ∧ 𝑥 ∈ (0...𝑁)) → (𝑃‘((𝑥 + 𝑆) − 𝑁)) = (𝑃‘(𝑥 − 𝑁))) |
| 29 | 20, 27, 28 | ifbieq12d 4554 |
. . . . 5
⊢ (((𝜑 ∧ 𝑆 = 0) ∧ 𝑥 ∈ (0...𝑁)) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) = if(𝑥 ≤ 𝑁, (𝑃‘𝑥), (𝑃‘(𝑥 − 𝑁)))) |
| 30 | 29 | mpteq2dva 5242 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ 𝑁, (𝑃‘𝑥), (𝑃‘(𝑥 − 𝑁))))) |
| 31 | | elfzle2 13568 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ≤ 𝑁) |
| 32 | 31 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ≤ 𝑁) |
| 33 | 32 | iftrued 4533 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0...𝑁)) → if(𝑥 ≤ 𝑁, (𝑃‘𝑥), (𝑃‘(𝑥 − 𝑁))) = (𝑃‘𝑥)) |
| 34 | 33 | mpteq2dva 5242 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ 𝑁, (𝑃‘𝑥), (𝑃‘(𝑥 − 𝑁)))) = (𝑥 ∈ (0...𝑁) ↦ (𝑃‘𝑥))) |
| 35 | 13 | wlkp 29634 |
. . . . . . . 8
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
| 36 | 3, 4, 35 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
| 37 | | ffn 6736 |
. . . . . . . . . . 11
⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → 𝑃 Fn (0...(♯‘𝐹))) |
| 38 | 14 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢
(♯‘𝐹) =
𝑁 |
| 39 | 38 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢
(0...(♯‘𝐹)) = (0...𝑁) |
| 40 | 39 | fneq2i 6666 |
. . . . . . . . . . 11
⊢ (𝑃 Fn (0...(♯‘𝐹)) ↔ 𝑃 Fn (0...𝑁)) |
| 41 | 37, 40 | sylib 218 |
. . . . . . . . . 10
⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → 𝑃 Fn (0...𝑁)) |
| 42 | 41 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → 𝑃 Fn (0...𝑁)) |
| 43 | | dffn5 6967 |
. . . . . . . . 9
⊢ (𝑃 Fn (0...𝑁) ↔ 𝑃 = (𝑥 ∈ (0...𝑁) ↦ (𝑃‘𝑥))) |
| 44 | 42, 43 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → 𝑃 = (𝑥 ∈ (0...𝑁) ↦ (𝑃‘𝑥))) |
| 45 | 44 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → (𝑥 ∈ (0...𝑁) ↦ (𝑃‘𝑥)) = 𝑃) |
| 46 | 36, 45 | mpdan 687 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0...𝑁) ↦ (𝑃‘𝑥)) = 𝑃) |
| 47 | 34, 46 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ 𝑁, (𝑃‘𝑥), (𝑃‘(𝑥 − 𝑁)))) = 𝑃) |
| 48 | 47 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ 𝑁, (𝑃‘𝑥), (𝑃‘(𝑥 − 𝑁)))) = 𝑃) |
| 49 | 30, 48 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) = 𝑃) |
| 50 | 11, 49 | eqtrid 2789 |
. 2
⊢ ((𝜑 ∧ 𝑆 = 0) → 𝑄 = 𝑃) |
| 51 | 10, 50 | jca 511 |
1
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝐻 = 𝐹 ∧ 𝑄 = 𝑃)) |