Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
โข
(iEdgโ๐บ) =
(iEdgโ๐บ) |
2 | 1 | wlkf 28871 |
. . 3
โข (๐น(Walksโ๐บ)๐ โ ๐น โ Word dom (iEdgโ๐บ)) |
3 | | revcl 14711 |
. . 3
โข (๐น โ Word dom
(iEdgโ๐บ) โ
(reverseโ๐น) โ
Word dom (iEdgโ๐บ)) |
4 | 2, 3 | syl 17 |
. 2
โข (๐น(Walksโ๐บ)๐ โ (reverseโ๐น) โ Word dom (iEdgโ๐บ)) |
5 | | eqid 2733 |
. . . . 5
โข
(Vtxโ๐บ) =
(Vtxโ๐บ) |
6 | 5 | wlkpwrd 28874 |
. . . 4
โข (๐น(Walksโ๐บ)๐ โ ๐ โ Word (Vtxโ๐บ)) |
7 | | revcl 14711 |
. . . 4
โข (๐ โ Word (Vtxโ๐บ) โ (reverseโ๐) โ Word (Vtxโ๐บ)) |
8 | | wrdf 14469 |
. . . 4
โข
((reverseโ๐)
โ Word (Vtxโ๐บ)
โ (reverseโ๐):(0..^(โฏโ(reverseโ๐)))โถ(Vtxโ๐บ)) |
9 | 6, 7, 8 | 3syl 18 |
. . 3
โข (๐น(Walksโ๐บ)๐ โ (reverseโ๐):(0..^(โฏโ(reverseโ๐)))โถ(Vtxโ๐บ)) |
10 | | revlen 14712 |
. . . . . . 7
โข (๐น โ Word dom
(iEdgโ๐บ) โ
(โฏโ(reverseโ๐น)) = (โฏโ๐น)) |
11 | 2, 10 | syl 17 |
. . . . . 6
โข (๐น(Walksโ๐บ)๐ โ (โฏโ(reverseโ๐น)) = (โฏโ๐น)) |
12 | 11 | oveq2d 7425 |
. . . . 5
โข (๐น(Walksโ๐บ)๐ โ
(0...(โฏโ(reverseโ๐น))) = (0...(โฏโ๐น))) |
13 | | wlklenvp1 28875 |
. . . . . . 7
โข (๐น(Walksโ๐บ)๐ โ (โฏโ๐) = ((โฏโ๐น) + 1)) |
14 | 13 | oveq2d 7425 |
. . . . . 6
โข (๐น(Walksโ๐บ)๐ โ (0..^(โฏโ๐)) = (0..^((โฏโ๐น) + 1))) |
15 | | revlen 14712 |
. . . . . . . 8
โข (๐ โ Word (Vtxโ๐บ) โ
(โฏโ(reverseโ๐)) = (โฏโ๐)) |
16 | 6, 15 | syl 17 |
. . . . . . 7
โข (๐น(Walksโ๐บ)๐ โ (โฏโ(reverseโ๐)) = (โฏโ๐)) |
17 | 16 | oveq2d 7425 |
. . . . . 6
โข (๐น(Walksโ๐บ)๐ โ
(0..^(โฏโ(reverseโ๐))) = (0..^(โฏโ๐))) |
18 | | wlkcl 28872 |
. . . . . . . 8
โข (๐น(Walksโ๐บ)๐ โ (โฏโ๐น) โ
โ0) |
19 | 18 | nn0zd 12584 |
. . . . . . 7
โข (๐น(Walksโ๐บ)๐ โ (โฏโ๐น) โ โค) |
20 | | fzval3 13701 |
. . . . . . 7
โข
((โฏโ๐น)
โ โค โ (0...(โฏโ๐น)) = (0..^((โฏโ๐น) + 1))) |
21 | 19, 20 | syl 17 |
. . . . . 6
โข (๐น(Walksโ๐บ)๐ โ (0...(โฏโ๐น)) = (0..^((โฏโ๐น) + 1))) |
22 | 14, 17, 21 | 3eqtr4rd 2784 |
. . . . 5
โข (๐น(Walksโ๐บ)๐ โ (0...(โฏโ๐น)) =
(0..^(โฏโ(reverseโ๐)))) |
23 | 12, 22 | eqtrd 2773 |
. . . 4
โข (๐น(Walksโ๐บ)๐ โ
(0...(โฏโ(reverseโ๐น))) =
(0..^(โฏโ(reverseโ๐)))) |
24 | 23 | feq2d 6704 |
. . 3
โข (๐น(Walksโ๐บ)๐ โ ((reverseโ๐):(0...(โฏโ(reverseโ๐น)))โถ(Vtxโ๐บ) โ (reverseโ๐):(0..^(โฏโ(reverseโ๐)))โถ(Vtxโ๐บ))) |
25 | 9, 24 | mpbird 257 |
. 2
โข (๐น(Walksโ๐บ)๐ โ (reverseโ๐):(0...(โฏโ(reverseโ๐น)))โถ(Vtxโ๐บ)) |
26 | 11 | oveq2d 7425 |
. . . . . 6
โข (๐น(Walksโ๐บ)๐ โ
(0..^(โฏโ(reverseโ๐น))) = (0..^(โฏโ๐น))) |
27 | 26 | eleq2d 2820 |
. . . . 5
โข (๐น(Walksโ๐บ)๐ โ (๐ โ
(0..^(โฏโ(reverseโ๐น))) โ ๐ โ (0..^(โฏโ๐น)))) |
28 | 27 | biimpa 478 |
. . . 4
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ
(0..^(โฏโ(reverseโ๐น)))) โ ๐ โ (0..^(โฏโ๐น))) |
29 | | revfv 14713 |
. . . . . . . . . 10
โข ((๐น โ Word dom
(iEdgโ๐บ) โง ๐ โ
(0..^(โฏโ๐น)))
โ ((reverseโ๐น)โ๐) = (๐นโ(((โฏโ๐น) โ 1) โ ๐))) |
30 | 2, 29 | sylan 581 |
. . . . . . . . 9
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ((reverseโ๐น)โ๐) = (๐นโ(((โฏโ๐น) โ 1) โ ๐))) |
31 | | wlklenvm1 28879 |
. . . . . . . . . . . . 13
โข (๐น(Walksโ๐บ)๐ โ (โฏโ๐น) = ((โฏโ๐) โ 1)) |
32 | 31 | oveq1d 7424 |
. . . . . . . . . . . 12
โข (๐น(Walksโ๐บ)๐ โ ((โฏโ๐น) โ 1) = (((โฏโ๐) โ 1) โ
1)) |
33 | | lencl 14483 |
. . . . . . . . . . . . . 14
โข (๐ โ Word (Vtxโ๐บ) โ (โฏโ๐) โ
โ0) |
34 | 33 | nn0cnd 12534 |
. . . . . . . . . . . . 13
โข (๐ โ Word (Vtxโ๐บ) โ (โฏโ๐) โ
โ) |
35 | | sub1m1 12464 |
. . . . . . . . . . . . 13
โข
((โฏโ๐)
โ โ โ (((โฏโ๐) โ 1) โ 1) =
((โฏโ๐) โ
2)) |
36 | 6, 34, 35 | 3syl 18 |
. . . . . . . . . . . 12
โข (๐น(Walksโ๐บ)๐ โ (((โฏโ๐) โ 1) โ 1) =
((โฏโ๐) โ
2)) |
37 | 32, 36 | eqtrd 2773 |
. . . . . . . . . . 11
โข (๐น(Walksโ๐บ)๐ โ ((โฏโ๐น) โ 1) = ((โฏโ๐) โ 2)) |
38 | 37 | fvoveq1d 7431 |
. . . . . . . . . 10
โข (๐น(Walksโ๐บ)๐ โ (๐นโ(((โฏโ๐น) โ 1) โ ๐)) = (๐นโ(((โฏโ๐) โ 2) โ ๐))) |
39 | 38 | adantr 482 |
. . . . . . . . 9
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (๐นโ(((โฏโ๐น) โ 1) โ ๐)) = (๐นโ(((โฏโ๐) โ 2) โ ๐))) |
40 | 30, 39 | eqtrd 2773 |
. . . . . . . 8
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ((reverseโ๐น)โ๐) = (๐นโ(((โฏโ๐) โ 2) โ ๐))) |
41 | 40 | fveq2d 6896 |
. . . . . . 7
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)) = ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐)))) |
42 | 41 | adantr 482 |
. . . . . 6
โข (((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โง ((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1))) โ ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)) = ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐)))) |
43 | | fzonn0p1p1 13711 |
. . . . . . . . . . . . 13
โข (๐ โ
(0..^(โฏโ๐น))
โ (๐ + 1) โ
(0..^((โฏโ๐น) +
1))) |
44 | 43 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (๐ + 1) โ (0..^((โฏโ๐น) + 1))) |
45 | 14 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (0..^(โฏโ๐)) = (0..^((โฏโ๐น) + 1))) |
46 | 44, 45 | eleqtrrd 2837 |
. . . . . . . . . . 11
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (๐ + 1) โ (0..^(โฏโ๐))) |
47 | | revfv 14713 |
. . . . . . . . . . 11
โข ((๐ โ Word (Vtxโ๐บ) โง (๐ + 1) โ (0..^(โฏโ๐))) โ ((reverseโ๐)โ(๐ + 1)) = (๐โ(((โฏโ๐) โ 1) โ (๐ + 1)))) |
48 | 6, 46, 47 | syl2an2r 684 |
. . . . . . . . . 10
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ((reverseโ๐)โ(๐ + 1)) = (๐โ(((โฏโ๐) โ 1) โ (๐ + 1)))) |
49 | | elfzoelz 13632 |
. . . . . . . . . . . . . . . 16
โข (๐ โ
(0..^(โฏโ๐น))
โ ๐ โ
โค) |
50 | 49 | zcnd 12667 |
. . . . . . . . . . . . . . 15
โข (๐ โ
(0..^(โฏโ๐น))
โ ๐ โ
โ) |
51 | 50 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ๐ โ โ) |
52 | | 1cnd 11209 |
. . . . . . . . . . . . . 14
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ 1 โ
โ) |
53 | 51, 52 | addcomd 11416 |
. . . . . . . . . . . . 13
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (๐ + 1) = (1 + ๐)) |
54 | 53 | oveq2d 7425 |
. . . . . . . . . . . 12
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((โฏโ๐) โ 1) โ (๐ + 1)) = (((โฏโ๐) โ 1) โ (1 + ๐))) |
55 | 6, 34 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐น(Walksโ๐บ)๐ โ (โฏโ๐) โ โ) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (โฏโ๐) โ โ) |
57 | 56, 52 | subcld 11571 |
. . . . . . . . . . . . 13
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ((โฏโ๐) โ 1) โ
โ) |
58 | 57, 52, 51 | subsub4d 11602 |
. . . . . . . . . . . 12
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ((((โฏโ๐) โ 1) โ 1) โ
๐) = (((โฏโ๐) โ 1) โ (1 + ๐))) |
59 | 36 | oveq1d 7424 |
. . . . . . . . . . . . 13
โข (๐น(Walksโ๐บ)๐ โ ((((โฏโ๐) โ 1) โ 1) โ ๐) = (((โฏโ๐) โ 2) โ ๐)) |
60 | 59 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ((((โฏโ๐) โ 1) โ 1) โ
๐) = (((โฏโ๐) โ 2) โ ๐)) |
61 | 54, 58, 60 | 3eqtr2d 2779 |
. . . . . . . . . . 11
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((โฏโ๐) โ 1) โ (๐ + 1)) = (((โฏโ๐) โ 2) โ ๐)) |
62 | 61 | fveq2d 6896 |
. . . . . . . . . 10
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (๐โ(((โฏโ๐) โ 1) โ (๐ + 1))) = (๐โ(((โฏโ๐) โ 2) โ ๐))) |
63 | 48, 62 | eqtrd 2773 |
. . . . . . . . 9
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ((reverseโ๐)โ(๐ + 1)) = (๐โ(((โฏโ๐) โ 2) โ ๐))) |
64 | 63 | sneqd 4641 |
. . . . . . . 8
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ {((reverseโ๐)โ(๐ + 1))} = {(๐โ(((โฏโ๐) โ 2) โ ๐))}) |
65 | 64 | adantr 482 |
. . . . . . 7
โข (((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โง ((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1))) โ {((reverseโ๐)โ(๐ + 1))} = {(๐โ(((โฏโ๐) โ 2) โ ๐))}) |
66 | | sneq 4639 |
. . . . . . . 8
โข
(((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1)) โ {((reverseโ๐)โ๐)} = {((reverseโ๐)โ(๐ + 1))}) |
67 | 66 | adantl 483 |
. . . . . . 7
โข (((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โง ((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1))) โ {((reverseโ๐)โ๐)} = {((reverseโ๐)โ(๐ + 1))}) |
68 | | eqcom 2740 |
. . . . . . . . . 10
โข
(((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1)) โ ((reverseโ๐)โ(๐ + 1)) = ((reverseโ๐)โ๐)) |
69 | | fzossfzop1 13710 |
. . . . . . . . . . . . . . . 16
โข
((โฏโ๐น)
โ โ0 โ (0..^(โฏโ๐น)) โ (0..^((โฏโ๐น) + 1))) |
70 | 18, 69 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐น(Walksโ๐บ)๐ โ (0..^(โฏโ๐น)) โ
(0..^((โฏโ๐น) +
1))) |
71 | 70, 14 | sseqtrrd 4024 |
. . . . . . . . . . . . . 14
โข (๐น(Walksโ๐บ)๐ โ (0..^(โฏโ๐น)) โ
(0..^(โฏโ๐))) |
72 | 71 | sselda 3983 |
. . . . . . . . . . . . 13
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ๐ โ (0..^(โฏโ๐))) |
73 | | revfv 14713 |
. . . . . . . . . . . . 13
โข ((๐ โ Word (Vtxโ๐บ) โง ๐ โ (0..^(โฏโ๐))) โ ((reverseโ๐)โ๐) = (๐โ(((โฏโ๐) โ 1) โ ๐))) |
74 | 6, 72, 73 | syl2an2r 684 |
. . . . . . . . . . . 12
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ((reverseโ๐)โ๐) = (๐โ(((โฏโ๐) โ 1) โ ๐))) |
75 | 57, 51, 52 | sub32d 11603 |
. . . . . . . . . . . . . . 15
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ((((โฏโ๐) โ 1) โ ๐) โ 1) =
((((โฏโ๐)
โ 1) โ 1) โ ๐)) |
76 | 75 | oveq1d 7424 |
. . . . . . . . . . . . . 14
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((((โฏโ๐) โ 1) โ ๐) โ 1) + 1) =
(((((โฏโ๐)
โ 1) โ 1) โ ๐) + 1)) |
77 | 57, 51 | subcld 11571 |
. . . . . . . . . . . . . . 15
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((โฏโ๐) โ 1) โ ๐) โ
โ) |
78 | 77, 52 | npcand 11575 |
. . . . . . . . . . . . . 14
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((((โฏโ๐) โ 1) โ ๐) โ 1) + 1) =
(((โฏโ๐) โ
1) โ ๐)) |
79 | 59 | oveq1d 7424 |
. . . . . . . . . . . . . . 15
โข (๐น(Walksโ๐บ)๐ โ (((((โฏโ๐) โ 1) โ 1) โ ๐) + 1) = ((((โฏโ๐) โ 2) โ ๐) + 1)) |
80 | 79 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((((โฏโ๐) โ 1) โ 1) โ
๐) + 1) =
((((โฏโ๐)
โ 2) โ ๐) +
1)) |
81 | 76, 78, 80 | 3eqtr3d 2781 |
. . . . . . . . . . . . 13
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((โฏโ๐) โ 1) โ ๐) = ((((โฏโ๐) โ 2) โ ๐) + 1)) |
82 | 81 | fveq2d 6896 |
. . . . . . . . . . . 12
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (๐โ(((โฏโ๐) โ 1) โ ๐)) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1))) |
83 | 74, 82 | eqtrd 2773 |
. . . . . . . . . . 11
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ((reverseโ๐)โ๐) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1))) |
84 | 63, 83 | eqeq12d 2749 |
. . . . . . . . . 10
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((reverseโ๐)โ(๐ + 1)) = ((reverseโ๐)โ๐) โ (๐โ(((โฏโ๐) โ 2) โ ๐)) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1)))) |
85 | 68, 84 | bitrid 283 |
. . . . . . . . 9
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1)) โ (๐โ(((โฏโ๐) โ 2) โ ๐)) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1)))) |
86 | | wkslem1 28864 |
. . . . . . . . . . . 12
โข (๐ฅ = (((โฏโ๐) โ 2) โ ๐) โ (if-((๐โ๐ฅ) = (๐โ(๐ฅ + 1)), ((iEdgโ๐บ)โ(๐นโ๐ฅ)) = {(๐โ๐ฅ)}, {(๐โ๐ฅ), (๐โ(๐ฅ + 1))} โ ((iEdgโ๐บ)โ(๐นโ๐ฅ))) โ if-((๐โ(((โฏโ๐) โ 2) โ ๐)) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1)), ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐))) = {(๐โ(((โฏโ๐) โ 2) โ ๐))}, {(๐โ(((โฏโ๐) โ 2) โ ๐)), (๐โ((((โฏโ๐) โ 2) โ ๐) + 1))} โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐)))))) |
87 | 5, 1 | wlkprop 28868 |
. . . . . . . . . . . . . 14
โข (๐น(Walksโ๐บ)๐ โ (๐น โ Word dom (iEdgโ๐บ) โง ๐:(0...(โฏโ๐น))โถ(Vtxโ๐บ) โง โ๐ฅ โ (0..^(โฏโ๐น))if-((๐โ๐ฅ) = (๐โ(๐ฅ + 1)), ((iEdgโ๐บ)โ(๐นโ๐ฅ)) = {(๐โ๐ฅ)}, {(๐โ๐ฅ), (๐โ(๐ฅ + 1))} โ ((iEdgโ๐บ)โ(๐นโ๐ฅ))))) |
88 | 87 | simp3d 1145 |
. . . . . . . . . . . . 13
โข (๐น(Walksโ๐บ)๐ โ โ๐ฅ โ (0..^(โฏโ๐น))if-((๐โ๐ฅ) = (๐โ(๐ฅ + 1)), ((iEdgโ๐บ)โ(๐นโ๐ฅ)) = {(๐โ๐ฅ)}, {(๐โ๐ฅ), (๐โ(๐ฅ + 1))} โ ((iEdgโ๐บ)โ(๐นโ๐ฅ)))) |
89 | 88 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ โ๐ฅ โ (0..^(โฏโ๐น))if-((๐โ๐ฅ) = (๐โ(๐ฅ + 1)), ((iEdgโ๐บ)โ(๐นโ๐ฅ)) = {(๐โ๐ฅ)}, {(๐โ๐ฅ), (๐โ(๐ฅ + 1))} โ ((iEdgโ๐บ)โ(๐นโ๐ฅ)))) |
90 | 18 | nn0cnd 12534 |
. . . . . . . . . . . . . . . 16
โข (๐น(Walksโ๐บ)๐ โ (โฏโ๐น) โ โ) |
91 | 90 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (โฏโ๐น) โ โ) |
92 | 91, 51, 52 | sub32d 11603 |
. . . . . . . . . . . . . 14
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((โฏโ๐น) โ ๐) โ 1) = (((โฏโ๐น) โ 1) โ ๐)) |
93 | 37 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ((โฏโ๐น) โ 1) = ((โฏโ๐) โ 2)) |
94 | 93 | oveq1d 7424 |
. . . . . . . . . . . . . 14
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((โฏโ๐น) โ 1) โ ๐) = (((โฏโ๐) โ 2) โ ๐)) |
95 | 92, 94 | eqtrd 2773 |
. . . . . . . . . . . . 13
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((โฏโ๐น) โ ๐) โ 1) = (((โฏโ๐) โ 2) โ ๐)) |
96 | | ubmelm1fzo 13728 |
. . . . . . . . . . . . . 14
โข (๐ โ
(0..^(โฏโ๐น))
โ (((โฏโ๐น)
โ ๐) โ 1)
โ (0..^(โฏโ๐น))) |
97 | 96 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((โฏโ๐น) โ ๐) โ 1) โ (0..^(โฏโ๐น))) |
98 | 95, 97 | eqeltrrd 2835 |
. . . . . . . . . . . 12
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((โฏโ๐) โ 2) โ ๐) โ
(0..^(โฏโ๐น))) |
99 | 86, 89, 98 | rspcdva 3614 |
. . . . . . . . . . 11
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ if-((๐โ(((โฏโ๐) โ 2) โ ๐)) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1)), ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐))) = {(๐โ(((โฏโ๐) โ 2) โ ๐))}, {(๐โ(((โฏโ๐) โ 2) โ ๐)), (๐โ((((โฏโ๐) โ 2) โ ๐) + 1))} โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐))))) |
100 | | dfifp2 1064 |
. . . . . . . . . . 11
โข
(if-((๐โ(((โฏโ๐) โ 2) โ ๐)) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1)), ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐))) = {(๐โ(((โฏโ๐) โ 2) โ ๐))}, {(๐โ(((โฏโ๐) โ 2) โ ๐)), (๐โ((((โฏโ๐) โ 2) โ ๐) + 1))} โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐)))) โ (((๐โ(((โฏโ๐) โ 2) โ ๐)) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1)) โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐))) = {(๐โ(((โฏโ๐) โ 2) โ ๐))}) โง (ยฌ (๐โ(((โฏโ๐) โ 2) โ ๐)) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1)) โ {(๐โ(((โฏโ๐) โ 2) โ ๐)), (๐โ((((โฏโ๐) โ 2) โ ๐) + 1))} โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐)))))) |
101 | 99, 100 | sylib 217 |
. . . . . . . . . 10
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((๐โ(((โฏโ๐) โ 2) โ ๐)) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1)) โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐))) = {(๐โ(((โฏโ๐) โ 2) โ ๐))}) โง (ยฌ (๐โ(((โฏโ๐) โ 2) โ ๐)) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1)) โ {(๐โ(((โฏโ๐) โ 2) โ ๐)), (๐โ((((โฏโ๐) โ 2) โ ๐) + 1))} โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐)))))) |
102 | 101 | simpld 496 |
. . . . . . . . 9
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ ((๐โ(((โฏโ๐) โ 2) โ ๐)) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1)) โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐))) = {(๐โ(((โฏโ๐) โ 2) โ ๐))})) |
103 | 85, 102 | sylbid 239 |
. . . . . . . 8
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1)) โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐))) = {(๐โ(((โฏโ๐) โ 2) โ ๐))})) |
104 | 103 | imp 408 |
. . . . . . 7
โข (((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โง ((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1))) โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐))) = {(๐โ(((โฏโ๐) โ 2) โ ๐))}) |
105 | 65, 67, 104 | 3eqtr4rd 2784 |
. . . . . 6
โข (((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โง ((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1))) โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐))) = {((reverseโ๐)โ๐)}) |
106 | 42, 105 | eqtrd 2773 |
. . . . 5
โข (((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โง ((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1))) โ ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)) = {((reverseโ๐)โ๐)}) |
107 | 85 | notbid 318 |
. . . . . . . 8
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (ยฌ ((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1)) โ ยฌ (๐โ(((โฏโ๐) โ 2) โ ๐)) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1)))) |
108 | 101 | simprd 497 |
. . . . . . . 8
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (ยฌ (๐โ(((โฏโ๐) โ 2) โ ๐)) = (๐โ((((โฏโ๐) โ 2) โ ๐) + 1)) โ {(๐โ(((โฏโ๐) โ 2) โ ๐)), (๐โ((((โฏโ๐) โ 2) โ ๐) + 1))} โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐))))) |
109 | 107, 108 | sylbid 239 |
. . . . . . 7
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ (ยฌ ((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1)) โ {(๐โ(((โฏโ๐) โ 2) โ ๐)), (๐โ((((โฏโ๐) โ 2) โ ๐) + 1))} โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐))))) |
110 | 109 | imp 408 |
. . . . . 6
โข (((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โง ยฌ ((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1))) โ {(๐โ(((โฏโ๐) โ 2) โ ๐)), (๐โ((((โฏโ๐) โ 2) โ ๐) + 1))} โ ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐)))) |
111 | | prcom 4737 |
. . . . . . . 8
โข
{((reverseโ๐)โ(๐ + 1)), ((reverseโ๐)โ๐)} = {((reverseโ๐)โ๐), ((reverseโ๐)โ(๐ + 1))} |
112 | 63, 83 | preq12d 4746 |
. . . . . . . 8
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ {((reverseโ๐)โ(๐ + 1)), ((reverseโ๐)โ๐)} = {(๐โ(((โฏโ๐) โ 2) โ ๐)), (๐โ((((โฏโ๐) โ 2) โ ๐) + 1))}) |
113 | 111, 112 | eqtr3id 2787 |
. . . . . . 7
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ {((reverseโ๐)โ๐), ((reverseโ๐)โ(๐ + 1))} = {(๐โ(((โฏโ๐) โ 2) โ ๐)), (๐โ((((โฏโ๐) โ 2) โ ๐) + 1))}) |
114 | 113 | adantr 482 |
. . . . . 6
โข (((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โง ยฌ ((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1))) โ {((reverseโ๐)โ๐), ((reverseโ๐)โ(๐ + 1))} = {(๐โ(((โฏโ๐) โ 2) โ ๐)), (๐โ((((โฏโ๐) โ 2) โ ๐) + 1))}) |
115 | 41 | adantr 482 |
. . . . . 6
โข (((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โง ยฌ ((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1))) โ ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)) = ((iEdgโ๐บ)โ(๐นโ(((โฏโ๐) โ 2) โ ๐)))) |
116 | 110, 114,
115 | 3sstr4d 4030 |
. . . . 5
โข (((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โง ยฌ ((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1))) โ {((reverseโ๐)โ๐), ((reverseโ๐)โ(๐ + 1))} โ ((iEdgโ๐บ)โ((reverseโ๐น)โ๐))) |
117 | 106, 116 | ifpimpda 1082 |
. . . 4
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ (0..^(โฏโ๐น))) โ if-(((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1)), ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)) = {((reverseโ๐)โ๐)}, {((reverseโ๐)โ๐), ((reverseโ๐)โ(๐ + 1))} โ ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)))) |
118 | 28, 117 | syldan 592 |
. . 3
โข ((๐น(Walksโ๐บ)๐ โง ๐ โ
(0..^(โฏโ(reverseโ๐น)))) โ if-(((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1)), ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)) = {((reverseโ๐)โ๐)}, {((reverseโ๐)โ๐), ((reverseโ๐)โ(๐ + 1))} โ ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)))) |
119 | 118 | ralrimiva 3147 |
. 2
โข (๐น(Walksโ๐บ)๐ โ โ๐ โ
(0..^(โฏโ(reverseโ๐น)))if-(((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1)), ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)) = {((reverseโ๐)โ๐)}, {((reverseโ๐)โ๐), ((reverseโ๐)โ(๐ + 1))} โ ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)))) |
120 | | wlkv 28869 |
. . . 4
โข (๐น(Walksโ๐บ)๐ โ (๐บ โ V โง ๐น โ V โง ๐ โ V)) |
121 | 120 | simp1d 1143 |
. . 3
โข (๐น(Walksโ๐บ)๐ โ ๐บ โ V) |
122 | 5, 1 | iswlkg 28870 |
. . 3
โข (๐บ โ V โ
((reverseโ๐น)(Walksโ๐บ)(reverseโ๐) โ ((reverseโ๐น) โ Word dom (iEdgโ๐บ) โง (reverseโ๐):(0...(โฏโ(reverseโ๐น)))โถ(Vtxโ๐บ) โง โ๐ โ
(0..^(โฏโ(reverseโ๐น)))if-(((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1)), ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)) = {((reverseโ๐)โ๐)}, {((reverseโ๐)โ๐), ((reverseโ๐)โ(๐ + 1))} โ ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)))))) |
123 | 121, 122 | syl 17 |
. 2
โข (๐น(Walksโ๐บ)๐ โ ((reverseโ๐น)(Walksโ๐บ)(reverseโ๐) โ ((reverseโ๐น) โ Word dom (iEdgโ๐บ) โง (reverseโ๐):(0...(โฏโ(reverseโ๐น)))โถ(Vtxโ๐บ) โง โ๐ โ
(0..^(โฏโ(reverseโ๐น)))if-(((reverseโ๐)โ๐) = ((reverseโ๐)โ(๐ + 1)), ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)) = {((reverseโ๐)โ๐)}, {((reverseโ๐)โ๐), ((reverseโ๐)โ(๐ + 1))} โ ((iEdgโ๐บ)โ((reverseโ๐น)โ๐)))))) |
124 | 4, 25, 119, 123 | mpbir3and 1343 |
1
โข (๐น(Walksโ๐บ)๐ โ (reverseโ๐น)(Walksโ๐บ)(reverseโ๐)) |