Step | Hyp | Ref
| Expression |
1 | | clwlkclwwlkf.c |
. . . . 5
β’ πΆ = {π€ β (ClWalksβπΊ) β£ 1 β€
(β―β(1st βπ€))} |
2 | | clwlkclwwlkf.a |
. . . . 5
β’ π΄ = (1st βπ) |
3 | | clwlkclwwlkf.b |
. . . . 5
β’ π΅ = (2nd βπ) |
4 | 1, 2, 3 | clwlkclwwlkflem 28997 |
. . . 4
β’ (π β πΆ β (π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β)) |
5 | | clwlkclwwlkf.d |
. . . . 5
β’ π· = (1st βπ) |
6 | | clwlkclwwlkf.e |
. . . . 5
β’ πΈ = (2nd βπ) |
7 | 1, 5, 6 | clwlkclwwlkflem 28997 |
. . . 4
β’ (π β πΆ β (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) |
8 | 4, 7 | anim12i 614 |
. . 3
β’ ((π β πΆ β§ π β πΆ) β ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β))) |
9 | | eqid 2733 |
. . . . . . 7
β’
(VtxβπΊ) =
(VtxβπΊ) |
10 | 9 | wlkpwrd 28614 |
. . . . . 6
β’ (π΄(WalksβπΊ)π΅ β π΅ β Word (VtxβπΊ)) |
11 | 10 | 3ad2ant1 1134 |
. . . . 5
β’ ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β π΅ β Word (VtxβπΊ)) |
12 | 9 | wlkpwrd 28614 |
. . . . . 6
β’ (π·(WalksβπΊ)πΈ β πΈ β Word (VtxβπΊ)) |
13 | 12 | 3ad2ant1 1134 |
. . . . 5
β’ ((π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β) β πΈ β Word (VtxβπΊ)) |
14 | 11, 13 | anim12i 614 |
. . . 4
β’ (((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β (π΅ β Word (VtxβπΊ) β§ πΈ β Word (VtxβπΊ))) |
15 | | nnnn0 12428 |
. . . . . 6
β’
((β―βπ΄)
β β β (β―βπ΄) β
β0) |
16 | 15 | 3ad2ant3 1136 |
. . . . 5
β’ ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β
(β―βπ΄) β
β0) |
17 | | nnnn0 12428 |
. . . . . 6
β’
((β―βπ·)
β β β (β―βπ·) β
β0) |
18 | 17 | 3ad2ant3 1136 |
. . . . 5
β’ ((π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β) β
(β―βπ·) β
β0) |
19 | 16, 18 | anim12i 614 |
. . . 4
β’ (((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β
((β―βπ΄) β
β0 β§ (β―βπ·) β
β0)) |
20 | | wlklenvp1 28615 |
. . . . . . . 8
β’ (π΄(WalksβπΊ)π΅ β (β―βπ΅) = ((β―βπ΄) + 1)) |
21 | | nnre 12168 |
. . . . . . . . . 10
β’
((β―βπ΄)
β β β (β―βπ΄) β β) |
22 | 21 | lep1d 12094 |
. . . . . . . . 9
β’
((β―βπ΄)
β β β (β―βπ΄) β€ ((β―βπ΄) + 1)) |
23 | | breq2 5113 |
. . . . . . . . 9
β’
((β―βπ΅) =
((β―βπ΄) + 1)
β ((β―βπ΄)
β€ (β―βπ΅)
β (β―βπ΄)
β€ ((β―βπ΄) +
1))) |
24 | 22, 23 | syl5ibr 246 |
. . . . . . . 8
β’
((β―βπ΅) =
((β―βπ΄) + 1)
β ((β―βπ΄)
β β β (β―βπ΄) β€ (β―βπ΅))) |
25 | 20, 24 | syl 17 |
. . . . . . 7
β’ (π΄(WalksβπΊ)π΅ β ((β―βπ΄) β β β (β―βπ΄) β€ (β―βπ΅))) |
26 | 25 | a1d 25 |
. . . . . 6
β’ (π΄(WalksβπΊ)π΅ β ((π΅β0) = (π΅β(β―βπ΄)) β ((β―βπ΄) β β β (β―βπ΄) β€ (β―βπ΅)))) |
27 | 26 | 3imp 1112 |
. . . . 5
β’ ((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β
(β―βπ΄) β€
(β―βπ΅)) |
28 | | wlklenvp1 28615 |
. . . . . . . 8
β’ (π·(WalksβπΊ)πΈ β (β―βπΈ) = ((β―βπ·) + 1)) |
29 | | nnre 12168 |
. . . . . . . . . 10
β’
((β―βπ·)
β β β (β―βπ·) β β) |
30 | 29 | lep1d 12094 |
. . . . . . . . 9
β’
((β―βπ·)
β β β (β―βπ·) β€ ((β―βπ·) + 1)) |
31 | | breq2 5113 |
. . . . . . . . 9
β’
((β―βπΈ) =
((β―βπ·) + 1)
β ((β―βπ·)
β€ (β―βπΈ)
β (β―βπ·)
β€ ((β―βπ·) +
1))) |
32 | 30, 31 | syl5ibr 246 |
. . . . . . . 8
β’
((β―βπΈ) =
((β―βπ·) + 1)
β ((β―βπ·)
β β β (β―βπ·) β€ (β―βπΈ))) |
33 | 28, 32 | syl 17 |
. . . . . . 7
β’ (π·(WalksβπΊ)πΈ β ((β―βπ·) β β β (β―βπ·) β€ (β―βπΈ))) |
34 | 33 | a1d 25 |
. . . . . 6
β’ (π·(WalksβπΊ)πΈ β ((πΈβ0) = (πΈβ(β―βπ·)) β ((β―βπ·) β β β (β―βπ·) β€ (β―βπΈ)))) |
35 | 34 | 3imp 1112 |
. . . . 5
β’ ((π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β) β
(β―βπ·) β€
(β―βπΈ)) |
36 | 27, 35 | anim12i 614 |
. . . 4
β’ (((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β
((β―βπ΄) β€
(β―βπ΅) β§
(β―βπ·) β€
(β―βπΈ))) |
37 | 14, 19, 36 | 3jca 1129 |
. . 3
β’ (((π΄(WalksβπΊ)π΅ β§ (π΅β0) = (π΅β(β―βπ΄)) β§ (β―βπ΄) β β) β§ (π·(WalksβπΊ)πΈ β§ (πΈβ0) = (πΈβ(β―βπ·)) β§ (β―βπ·) β β)) β ((π΅ β Word (VtxβπΊ) β§ πΈ β Word (VtxβπΊ)) β§ ((β―βπ΄) β β0 β§
(β―βπ·) β
β0) β§ ((β―βπ΄) β€ (β―βπ΅) β§ (β―βπ·) β€ (β―βπΈ)))) |
38 | | pfxeq 14593 |
. . 3
β’ (((π΅ β Word (VtxβπΊ) β§ πΈ β Word (VtxβπΊ)) β§ ((β―βπ΄) β β0 β§
(β―βπ·) β
β0) β§ ((β―βπ΄) β€ (β―βπ΅) β§ (β―βπ·) β€ (β―βπΈ))) β ((π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·)) β ((β―βπ΄) = (β―βπ·) β§ βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ)))) |
39 | 8, 37, 38 | 3syl 18 |
. 2
β’ ((π β πΆ β§ π β πΆ) β ((π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·)) β ((β―βπ΄) = (β―βπ·) β§ βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ)))) |
40 | 39 | biimp3a 1470 |
1
β’ ((π β πΆ β§ π β πΆ β§ (π΅ prefix (β―βπ΄)) = (πΈ prefix (β―βπ·))) β ((β―βπ΄) = (β―βπ·) β§ βπ β (0..^(β―βπ΄))(π΅βπ) = (πΈβπ))) |