Step | Hyp | Ref
| Expression |
1 | | clwlkclwwlkf.c |
. . . . 5
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€
(β―β(1st βπ€))} |
2 | | clwlkclwwlkf.a |
. . . . 5
β’ π΄ = (1st βπ) |
3 | | clwlkclwwlkf.b |
. . . . 5
β’ π΅ = (2nd βπ) |
4 | | clwlkclwwlkf.d |
. . . . 5
β’ π· = (1st βπ) |
5 | | clwlkclwwlkf.e |
. . . . 5
β’ πΈ = (2nd βπ) |
6 | 1, 2, 3, 4, 5 | clwlkclwwlkf1lem2 28998 |
. . . 4
β’ ((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β ((β―βπ΄) = (β―βπ·) β§ βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ))) |
7 | | simprr 772 |
. . . . 5
β’ (((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β§ ((β―βπ΄) = (β―βπ·) β§ βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ))) β βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ)) |
8 | 1, 2, 3 | clwlkclwwlkflem 28997 |
. . . . . . . . 9
β’ (π β πΆ β (π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β)) |
9 | 1, 4, 5 | clwlkclwwlkflem 28997 |
. . . . . . . . 9
β’ (π β πΆ β (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) |
10 | | lbfzo0 13621 |
. . . . . . . . . . . . . . . 16
β’ (0 β
(0..^(β―βπ΄))
β (β―βπ΄)
β β) |
11 | 10 | biimpri 227 |
. . . . . . . . . . . . . . 15
β’
((β―βπ΄)
β β β 0 β (0..^(β―βπ΄))) |
12 | 11 | 3ad2ant3 1136 |
. . . . . . . . . . . . . 14
β’ ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β 0 β
(0..^(β―βπ΄))) |
13 | 12 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β 0 β
(0..^(β―βπ΄))) |
14 | 13 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β§
(β―βπ΄) =
(β―βπ·)) β 0
β (0..^(β―βπ΄))) |
15 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (π΅βπ) = (π΅β0)) |
16 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (πΈβπ) = (πΈβ0)) |
17 | 15, 16 | eqeq12d 2749 |
. . . . . . . . . . . . 13
β’ (π = 0 β ((π΅βπ) = (πΈβπ) β (π΅β0) = (πΈβ0))) |
18 | 17 | rspcv 3579 |
. . . . . . . . . . . 12
β’ (0 β
(0..^(β―βπ΄))
β (βπ β
(0..^(β―βπ΄))(π΅βπ) = (πΈβπ) β (π΅β0) = (πΈβ0))) |
19 | 14, 18 | syl 17 |
. . . . . . . . . . 11
β’ ((((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β§
(β―βπ΄) =
(β―βπ·)) β
(βπ β
(0..^(β―βπ΄))(π΅βπ) = (πΈβπ) β (π΅β0) = (πΈβ0))) |
20 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π΅β(β―βπ΄)) = (π΅β0) β§ ((π΅β0) = (πΈβ0) β§ (πΈβ0) = (πΈβ(β―βπ·)))) β (π΅β(β―βπ΄)) = (π΅β0)) |
21 | | eqtr 2756 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π΅β0) = (πΈβ0) β§ (πΈβ0) = (πΈβ(β―βπ·))) β (π΅β0) = (πΈβ(β―βπ·))) |
22 | 21 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π΅β(β―βπ΄)) = (π΅β0) β§ ((π΅β0) = (πΈβ0) β§ (πΈβ0) = (πΈβ(β―βπ·)))) β (π΅β0) = (πΈβ(β―βπ·))) |
23 | 20, 22 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π΅β(β―βπ΄)) = (π΅β0) β§ ((π΅β0) = (πΈβ0) β§ (πΈβ0) = (πΈβ(β―βπ·)))) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ·))) |
24 | 23 | exp32 422 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π΅β(β―βπ΄)) = (π΅β0) β ((π΅β0) = (πΈβ0) β ((πΈβ0) = (πΈβ(β―βπ·)) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ·))))) |
25 | 24 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΅β(β―βπ΄)) = (π΅β0) β ((πΈβ0) = (πΈβ(β―βπ·)) β ((π΅β0) = (πΈβ0) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ·))))) |
26 | 25 | eqcoms 2741 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΅β0) = (π΅β(β―βπ΄)) β ((πΈβ0) = (πΈβ(β―βπ·)) β ((π΅β0) = (πΈβ0) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ·))))) |
27 | 26 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β ((πΈβ0) = (πΈβ(β―βπ·)) β ((π΅β0) = (πΈβ0) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ·))))) |
28 | 27 | com12 32 |
. . . . . . . . . . . . . . . . 17
β’ ((πΈβ0) = (πΈβ(β―βπ·)) β ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β ((π΅β0) = (πΈβ0) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ·))))) |
29 | 28 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . 16
β’ ((π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β) β ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β ((π΅β0) = (πΈβ0) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ·))))) |
30 | 29 | impcom 409 |
. . . . . . . . . . . . . . 15
β’ (((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β ((π΅β0) = (πΈβ0) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ·)))) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β§
(β―βπ΄) =
(β―βπ·)) β
((π΅β0) = (πΈβ0) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ·)))) |
32 | 31 | imp 408 |
. . . . . . . . . . . . 13
β’
(((((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β§
(β―βπ΄) =
(β―βπ·)) β§
(π΅β0) = (πΈβ0)) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ·))) |
33 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ·) =
(β―βπ΄) β
(πΈβ(β―βπ·)) = (πΈβ(β―βπ΄))) |
34 | 33 | eqcoms 2741 |
. . . . . . . . . . . . . . 15
β’
((β―βπ΄) =
(β―βπ·) β
(πΈβ(β―βπ·)) = (πΈβ(β―βπ΄))) |
35 | 34 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β§
(β―βπ΄) =
(β―βπ·)) β
(πΈβ(β―βπ·)) = (πΈβ(β―βπ΄))) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β§
(β―βπ΄) =
(β―βπ·)) β§
(π΅β0) = (πΈβ0)) β (πΈβ(β―βπ·)) = (πΈβ(β―βπ΄))) |
37 | 32, 36 | eqtrd 2773 |
. . . . . . . . . . . 12
β’
(((((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β§
(β―βπ΄) =
(β―βπ·)) β§
(π΅β0) = (πΈβ0)) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ΄))) |
38 | 37 | ex 414 |
. . . . . . . . . . 11
β’ ((((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β§
(β―βπ΄) =
(β―βπ·)) β
((π΅β0) = (πΈβ0) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ΄)))) |
39 | 19, 38 | syld 47 |
. . . . . . . . . 10
β’ ((((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β§
(β―βπ΄) =
(β―βπ·)) β
(βπ β
(0..^(β―βπ΄))(π΅βπ) = (πΈβπ) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ΄)))) |
40 | 39 | ex 414 |
. . . . . . . . 9
β’ (((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β
((β―βπ΄) =
(β―βπ·) β
(βπ β
(0..^(β―βπ΄))(π΅βπ) = (πΈβπ) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ΄))))) |
41 | 8, 9, 40 | syl2an 597 |
. . . . . . . 8
β’ ((π β πΆ β§ π β πΆ) β ((β―βπ΄) = (β―βπ·) β (βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ΄))))) |
42 | 41 | impd 412 |
. . . . . . 7
β’ ((π β πΆ β§ π β πΆ) β (((β―βπ΄) = (β―βπ·) β§ βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ)) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ΄)))) |
43 | 42 | 3adant3 1133 |
. . . . . 6
β’ ((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β (((β―βπ΄) = (β―βπ·) β§ βπ β
(0..^(β―βπ΄))(π΅βπ) = (πΈβπ)) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ΄)))) |
44 | 43 | imp 408 |
. . . . 5
β’ (((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β§ ((β―βπ΄) = (β―βπ·) β§ βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ))) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ΄))) |
45 | 7, 44 | jca 513 |
. . . 4
β’ (((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β§ ((β―βπ΄) = (β―βπ·) β§ βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ))) β (βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ) β§ (π΅β(β―βπ΄)) = (πΈβ(β―βπ΄)))) |
46 | 6, 45 | mpdan 686 |
. . 3
β’ ((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β (βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ) β§ (π΅β(β―βπ΄)) = (πΈβ(β―βπ΄)))) |
47 | | fvex 6859 |
. . . 4
β’
(β―βπ΄)
β V |
48 | | fveq2 6846 |
. . . . . 6
β’ (π = (β―βπ΄) β (π΅βπ) = (π΅β(β―βπ΄))) |
49 | | fveq2 6846 |
. . . . . 6
β’ (π = (β―βπ΄) β (πΈβπ) = (πΈβ(β―βπ΄))) |
50 | 48, 49 | eqeq12d 2749 |
. . . . 5
β’ (π = (β―βπ΄) β ((π΅βπ) = (πΈβπ) β (π΅β(β―βπ΄)) = (πΈβ(β―βπ΄)))) |
51 | 50 | ralunsn 4855 |
. . . 4
β’
((β―βπ΄)
β V β (βπ
β ((0..^(β―βπ΄)) βͺ {(β―βπ΄)})(π΅βπ) = (πΈβπ) β (βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ) β§ (π΅β(β―βπ΄)) = (πΈβ(β―βπ΄))))) |
52 | 47, 51 | ax-mp 5 |
. . 3
β’
(βπ β
((0..^(β―βπ΄))
βͺ {(β―βπ΄)})(π΅βπ) = (πΈβπ) β (βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ) β§ (π΅β(β―βπ΄)) = (πΈβ(β―βπ΄)))) |
53 | 46, 52 | sylibr 233 |
. 2
β’ ((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β βπ β ((0..^(β―βπ΄)) βͺ {(β―βπ΄)})(π΅βπ) = (πΈβπ)) |
54 | | nnnn0 12428 |
. . . . . . . 8
β’
((β―βπ΄)
β β β (β―βπ΄) β
β0) |
55 | | elnn0uz 12816 |
. . . . . . . 8
β’
((β―βπ΄)
β β0 β (β―βπ΄) β
(β€β₯β0)) |
56 | 54, 55 | sylib 217 |
. . . . . . 7
β’
((β―βπ΄)
β β β (β―βπ΄) β
(β€β₯β0)) |
57 | 56 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β
(β―βπ΄) β
(β€β₯β0)) |
58 | 8, 57 | syl 17 |
. . . . 5
β’ (π β πΆ β (β―βπ΄) β
(β€β₯β0)) |
59 | 58 | 3ad2ant1 1134 |
. . . 4
β’ ((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β (β―βπ΄) β
(β€β₯β0)) |
60 | | fzisfzounsn 13693 |
. . . 4
β’
((β―βπ΄)
β (β€β₯β0) β (0...(β―βπ΄)) = ((0..^(β―βπ΄)) βͺ {(β―βπ΄)})) |
61 | 59, 60 | syl 17 |
. . 3
β’ ((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β (0...(β―βπ΄)) = ((0..^(β―βπ΄)) βͺ {(β―βπ΄)})) |
62 | 61 | raleqdv 3312 |
. 2
β’ ((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β (βπ β (0...(β―βπ΄))(π΅βπ) = (πΈβπ) β βπ β ((0..^(β―βπ΄)) βͺ {(β―βπ΄)})(π΅βπ) = (πΈβπ))) |
63 | 53, 62 | mpbird 257 |
1
β’ ((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β βπ β (0...(β―βπ΄))(π΅βπ) = (πΈβπ)) |