Step | Hyp | Ref
| Expression |
1 | | crctcsh.h |
. . 3
β’ π» = (πΉ cyclShift π) |
2 | | oveq2 7366 |
. . . 4
β’ (π = 0 β (πΉ cyclShift π) = (πΉ cyclShift 0)) |
3 | | crctcsh.d |
. . . . . 6
β’ (π β πΉ(CircuitsβπΊ)π) |
4 | | crctiswlk 28786 |
. . . . . 6
β’ (πΉ(CircuitsβπΊ)π β πΉ(WalksβπΊ)π) |
5 | | crctcsh.i |
. . . . . . 7
β’ πΌ = (iEdgβπΊ) |
6 | 5 | wlkf 28604 |
. . . . . 6
β’ (πΉ(WalksβπΊ)π β πΉ β Word dom πΌ) |
7 | 3, 4, 6 | 3syl 18 |
. . . . 5
β’ (π β πΉ β Word dom πΌ) |
8 | | cshw0 14688 |
. . . . 5
β’ (πΉ β Word dom πΌ β (πΉ cyclShift 0) = πΉ) |
9 | 7, 8 | syl 17 |
. . . 4
β’ (π β (πΉ cyclShift 0) = πΉ) |
10 | 2, 9 | sylan9eqr 2795 |
. . 3
β’ ((π β§ π = 0) β (πΉ cyclShift π) = πΉ) |
11 | 1, 10 | eqtrid 2785 |
. 2
β’ ((π β§ π = 0) β π» = πΉ) |
12 | | crctcsh.q |
. . 3
β’ π = (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) |
13 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = 0 β (π β π) = (π β 0)) |
14 | | crctcsh.v |
. . . . . . . . . . . 12
β’ π = (VtxβπΊ) |
15 | | crctcsh.n |
. . . . . . . . . . . 12
β’ π = (β―βπΉ) |
16 | 14, 5, 3, 15 | crctcshlem1 28804 |
. . . . . . . . . . 11
β’ (π β π β
β0) |
17 | 16 | nn0cnd 12480 |
. . . . . . . . . 10
β’ (π β π β β) |
18 | 17 | subid1d 11506 |
. . . . . . . . 9
β’ (π β (π β 0) = π) |
19 | 13, 18 | sylan9eqr 2795 |
. . . . . . . 8
β’ ((π β§ π = 0) β (π β π) = π) |
20 | 19 | breq2d 5118 |
. . . . . . 7
β’ ((π β§ π = 0) β (π₯ β€ (π β π) β π₯ β€ π)) |
21 | 20 | adantr 482 |
. . . . . 6
β’ (((π β§ π = 0) β§ π₯ β (0...π)) β (π₯ β€ (π β π) β π₯ β€ π)) |
22 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = 0 β (π₯ + π) = (π₯ + 0)) |
23 | 22 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π = 0) β (π₯ + π) = (π₯ + 0)) |
24 | | elfzelz 13447 |
. . . . . . . . . 10
β’ (π₯ β (0...π) β π₯ β β€) |
25 | 24 | zcnd 12613 |
. . . . . . . . 9
β’ (π₯ β (0...π) β π₯ β β) |
26 | 25 | addid1d 11360 |
. . . . . . . 8
β’ (π₯ β (0...π) β (π₯ + 0) = π₯) |
27 | 23, 26 | sylan9eq 2793 |
. . . . . . 7
β’ (((π β§ π = 0) β§ π₯ β (0...π)) β (π₯ + π) = π₯) |
28 | 27 | fveq2d 6847 |
. . . . . 6
β’ (((π β§ π = 0) β§ π₯ β (0...π)) β (πβ(π₯ + π)) = (πβπ₯)) |
29 | 27 | fvoveq1d 7380 |
. . . . . 6
β’ (((π β§ π = 0) β§ π₯ β (0...π)) β (πβ((π₯ + π) β π)) = (πβ(π₯ β π))) |
30 | 21, 28, 29 | ifbieq12d 4515 |
. . . . 5
β’ (((π β§ π = 0) β§ π₯ β (0...π)) β if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π))) = if(π₯ β€ π, (πβπ₯), (πβ(π₯ β π)))) |
31 | 30 | mpteq2dva 5206 |
. . . 4
β’ ((π β§ π = 0) β (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) = (π₯ β (0...π) β¦ if(π₯ β€ π, (πβπ₯), (πβ(π₯ β π))))) |
32 | | elfzle2 13451 |
. . . . . . . . 9
β’ (π₯ β (0...π) β π₯ β€ π) |
33 | 32 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β (0...π)) β π₯ β€ π) |
34 | 33 | iftrued 4495 |
. . . . . . 7
β’ ((π β§ π₯ β (0...π)) β if(π₯ β€ π, (πβπ₯), (πβ(π₯ β π))) = (πβπ₯)) |
35 | 34 | mpteq2dva 5206 |
. . . . . 6
β’ (π β (π₯ β (0...π) β¦ if(π₯ β€ π, (πβπ₯), (πβ(π₯ β π)))) = (π₯ β (0...π) β¦ (πβπ₯))) |
36 | 14 | wlkp 28606 |
. . . . . . . 8
β’ (πΉ(WalksβπΊ)π β π:(0...(β―βπΉ))βΆπ) |
37 | 3, 4, 36 | 3syl 18 |
. . . . . . 7
β’ (π β π:(0...(β―βπΉ))βΆπ) |
38 | | ffn 6669 |
. . . . . . . . . . 11
β’ (π:(0...(β―βπΉ))βΆπ β π Fn (0...(β―βπΉ))) |
39 | 15 | eqcomi 2742 |
. . . . . . . . . . . . 13
β’
(β―βπΉ) =
π |
40 | 39 | oveq2i 7369 |
. . . . . . . . . . . 12
β’
(0...(β―βπΉ)) = (0...π) |
41 | 40 | fneq2i 6601 |
. . . . . . . . . . 11
β’ (π Fn (0...(β―βπΉ)) β π Fn (0...π)) |
42 | 38, 41 | sylib 217 |
. . . . . . . . . 10
β’ (π:(0...(β―βπΉ))βΆπ β π Fn (0...π)) |
43 | 42 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π:(0...(β―βπΉ))βΆπ) β π Fn (0...π)) |
44 | | dffn5 6902 |
. . . . . . . . 9
β’ (π Fn (0...π) β π = (π₯ β (0...π) β¦ (πβπ₯))) |
45 | 43, 44 | sylib 217 |
. . . . . . . 8
β’ ((π β§ π:(0...(β―βπΉ))βΆπ) β π = (π₯ β (0...π) β¦ (πβπ₯))) |
46 | 45 | eqcomd 2739 |
. . . . . . 7
β’ ((π β§ π:(0...(β―βπΉ))βΆπ) β (π₯ β (0...π) β¦ (πβπ₯)) = π) |
47 | 37, 46 | mpdan 686 |
. . . . . 6
β’ (π β (π₯ β (0...π) β¦ (πβπ₯)) = π) |
48 | 35, 47 | eqtrd 2773 |
. . . . 5
β’ (π β (π₯ β (0...π) β¦ if(π₯ β€ π, (πβπ₯), (πβ(π₯ β π)))) = π) |
49 | 48 | adantr 482 |
. . . 4
β’ ((π β§ π = 0) β (π₯ β (0...π) β¦ if(π₯ β€ π, (πβπ₯), (πβ(π₯ β π)))) = π) |
50 | 31, 49 | eqtrd 2773 |
. . 3
β’ ((π β§ π = 0) β (π₯ β (0...π) β¦ if(π₯ β€ (π β π), (πβ(π₯ + π)), (πβ((π₯ + π) β π)))) = π) |
51 | 12, 50 | eqtrid 2785 |
. 2
β’ ((π β§ π = 0) β π = π) |
52 | 11, 51 | jca 513 |
1
β’ ((π β§ π = 0) β (π» = πΉ β§ π = π)) |