Proof of Theorem crctcshlem4
Step | Hyp | Ref
| Expression |
1 | | crctcsh.h |
. . 3
⊢ 𝐻 = (𝐹 cyclShift 𝑆) |
2 | | oveq2 6557 |
. . . 4
⊢ (𝑆 = 0 → (𝐹 cyclShift 𝑆) = (𝐹 cyclShift 0)) |
3 | | crctcsh.d |
. . . . . 6
⊢ (𝜑 → 𝐹(CircuitS‘𝐺)𝑃) |
4 | | crctis1wlk 41002 |
. . . . . 6
⊢ (𝐹(CircuitS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) |
5 | | crctcsh.i |
. . . . . . 7
⊢ 𝐼 = (iEdg‘𝐺) |
6 | 5 | 1wlkf 40819 |
. . . . . 6
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
7 | 3, 4, 6 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) |
8 | | cshw0 13391 |
. . . . 5
⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift 0) = 𝐹) |
9 | 7, 8 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐹 cyclShift 0) = 𝐹) |
10 | 2, 9 | sylan9eqr 2666 |
. . 3
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝐹 cyclShift 𝑆) = 𝐹) |
11 | 1, 10 | syl5eq 2656 |
. 2
⊢ ((𝜑 ∧ 𝑆 = 0) → 𝐻 = 𝐹) |
12 | | crctcsh.q |
. . 3
⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) |
13 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑆 = 0 → (𝑁 − 𝑆) = (𝑁 − 0)) |
14 | | crctcsh.v |
. . . . . . . . . . . 12
⊢ 𝑉 = (Vtx‘𝐺) |
15 | | crctcsh.n |
. . . . . . . . . . . 12
⊢ 𝑁 = (#‘𝐹) |
16 | 14, 5, 3, 15 | crctcshlem1 41020 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
17 | 16 | nn0cnd 11230 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℂ) |
18 | 17 | subid1d 10260 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − 0) = 𝑁) |
19 | 13, 18 | sylan9eqr 2666 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝑁 − 𝑆) = 𝑁) |
20 | 19 | breq2d 4595 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝑥 ≤ (𝑁 − 𝑆) ↔ 𝑥 ≤ 𝑁)) |
21 | 20 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 = 0) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 ≤ (𝑁 − 𝑆) ↔ 𝑥 ≤ 𝑁)) |
22 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑆 = 0 → (𝑥 + 𝑆) = (𝑥 + 0)) |
23 | 22 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝑥 + 𝑆) = (𝑥 + 0)) |
24 | | elfzelz 12213 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℤ) |
25 | 24 | zcnd 11359 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℂ) |
26 | 25 | addid1d 10115 |
. . . . . . . 8
⊢ (𝑥 ∈ (0...𝑁) → (𝑥 + 0) = 𝑥) |
27 | 23, 26 | sylan9eq 2664 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 = 0) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) = 𝑥) |
28 | 27 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 = 0) ∧ 𝑥 ∈ (0...𝑁)) → (𝑃‘(𝑥 + 𝑆)) = (𝑃‘𝑥)) |
29 | 27 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 = 0) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) − 𝑁) = (𝑥 − 𝑁)) |
30 | 29 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 = 0) ∧ 𝑥 ∈ (0...𝑁)) → (𝑃‘((𝑥 + 𝑆) − 𝑁)) = (𝑃‘(𝑥 − 𝑁))) |
31 | 21, 28, 30 | ifbieq12d 4063 |
. . . . 5
⊢ (((𝜑 ∧ 𝑆 = 0) ∧ 𝑥 ∈ (0...𝑁)) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) = if(𝑥 ≤ 𝑁, (𝑃‘𝑥), (𝑃‘(𝑥 − 𝑁)))) |
32 | 31 | mpteq2dva 4672 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ 𝑁, (𝑃‘𝑥), (𝑃‘(𝑥 − 𝑁))))) |
33 | | elfzle2 12216 |
. . . . . . . . 9
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ≤ 𝑁) |
34 | 33 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ≤ 𝑁) |
35 | 34 | iftrued 4044 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (0...𝑁)) → if(𝑥 ≤ 𝑁, (𝑃‘𝑥), (𝑃‘(𝑥 − 𝑁))) = (𝑃‘𝑥)) |
36 | 35 | mpteq2dva 4672 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ 𝑁, (𝑃‘𝑥), (𝑃‘(𝑥 − 𝑁)))) = (𝑥 ∈ (0...𝑁) ↦ (𝑃‘𝑥))) |
37 | 14 | 1wlkp 40821 |
. . . . . . . 8
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶𝑉) |
38 | 3, 4, 37 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝑃:(0...(#‘𝐹))⟶𝑉) |
39 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → 𝑃 Fn (0...(#‘𝐹))) |
40 | 15 | eqcomi 2619 |
. . . . . . . . . . . . 13
⊢
(#‘𝐹) = 𝑁 |
41 | 40 | oveq2i 6560 |
. . . . . . . . . . . 12
⊢
(0...(#‘𝐹)) =
(0...𝑁) |
42 | 41 | fneq2i 5900 |
. . . . . . . . . . 11
⊢ (𝑃 Fn (0...(#‘𝐹)) ↔ 𝑃 Fn (0...𝑁)) |
43 | 39, 42 | sylib 207 |
. . . . . . . . . 10
⊢ (𝑃:(0...(#‘𝐹))⟶𝑉 → 𝑃 Fn (0...𝑁)) |
44 | 43 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → 𝑃 Fn (0...𝑁)) |
45 | | dffn5 6151 |
. . . . . . . . 9
⊢ (𝑃 Fn (0...𝑁) ↔ 𝑃 = (𝑥 ∈ (0...𝑁) ↦ (𝑃‘𝑥))) |
46 | 44, 45 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → 𝑃 = (𝑥 ∈ (0...𝑁) ↦ (𝑃‘𝑥))) |
47 | 46 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (𝑥 ∈ (0...𝑁) ↦ (𝑃‘𝑥)) = 𝑃) |
48 | 38, 47 | mpdan 699 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (0...𝑁) ↦ (𝑃‘𝑥)) = 𝑃) |
49 | 36, 48 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ 𝑁, (𝑃‘𝑥), (𝑃‘(𝑥 − 𝑁)))) = 𝑃) |
50 | 49 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ 𝑁, (𝑃‘𝑥), (𝑃‘(𝑥 − 𝑁)))) = 𝑃) |
51 | 32, 50 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) = 𝑃) |
52 | 12, 51 | syl5eq 2656 |
. 2
⊢ ((𝜑 ∧ 𝑆 = 0) → 𝑄 = 𝑃) |
53 | 11, 52 | jca 553 |
1
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝐻 = 𝐹 ∧ 𝑄 = 𝑃)) |