Step | Hyp | Ref
| Expression |
1 | | wlkres.h |
. . 3
..^ |
2 | | wlkres.d |
. . . . . . . 8
Walks |
3 | | wlkres.i |
. . . . . . . . 9
iEdg |
4 | 3 | wlkf 26510 |
. . . . . . . 8
Walks Word |
5 | | wrdfn 13319 |
. . . . . . . 8
Word
..^ |
6 | 2, 4, 5 | 3syl 18 |
. . . . . . 7
..^ |
7 | | wlkres.n |
. . . . . . . 8
..^ |
8 | | elfzouz2 12484 |
. . . . . . . 8
..^
|
9 | | fzoss2 12496 |
. . . . . . . 8
..^ ..^ |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . 7
..^ ..^ |
11 | | fnssres 6004 |
. . . . . . 7
..^ ..^ ..^ ..^ ..^ |
12 | 6, 10, 11 | syl2anc 693 |
. . . . . 6
..^ ..^ |
13 | | simpr 477 |
. . . . . . . . . . . 12
..^ ..^ |
14 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
15 | 14 | eqeq1d 2624 |
. . . . . . . . . . . . 13
..^
..^ |
16 | 15 | adantl 482 |
. . . . . . . . . . . 12
..^
..^
..^ |
17 | | fvres 6207 |
. . . . . . . . . . . . . 14
..^
..^ |
18 | 17 | adantl 482 |
. . . . . . . . . . . . 13
..^ ..^ |
19 | 18 | eqcomd 2628 |
. . . . . . . . . . . 12
..^ ..^ |
20 | 13, 16, 19 | rspcedvd 3317 |
. . . . . . . . . . 11
..^ ..^ ..^ |
21 | 6 | adantr 481 |
. . . . . . . . . . . 12
..^ ..^ |
22 | 10 | adantr 481 |
. . . . . . . . . . . 12
..^ ..^
..^ |
23 | 21, 22 | fvelimabd 6254 |
. . . . . . . . . . 11
..^
..^ ..^
..^
..^ |
24 | 20, 23 | mpbird 247 |
. . . . . . . . . 10
..^ ..^ ..^ |
25 | 2, 4 | syl 17 |
. . . . . . . . . . . . 13
Word |
26 | | wrdf 13310 |
. . . . . . . . . . . . . 14
Word
..^
|
27 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . 17
..^
..^ |
28 | 27 | expcom 451 |
. . . . . . . . . . . . . . . 16
..^
..^
|
29 | 10 | sselda 3603 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
30 | 28, 29 | syl11 33 |
. . . . . . . . . . . . . . 15
..^
..^
|
31 | 30 | expd 452 |
. . . . . . . . . . . . . 14
..^
..^ |
32 | 26, 31 | syl 17 |
. . . . . . . . . . . . 13
Word
..^ |
33 | 25, 32 | mpcom 38 |
. . . . . . . . . . . 12
..^ |
34 | 33 | imp 445 |
. . . . . . . . . . 11
..^ |
35 | 18, 34 | eqeltrd 2701 |
. . . . . . . . . 10
..^ ..^ |
36 | 24, 35 | elind 3798 |
. . . . . . . . 9
..^ ..^ ..^ |
37 | | dmres 5419 |
. . . . . . . . 9
..^ ..^
|
38 | 36, 37 | syl6eleqr 2712 |
. . . . . . . 8
..^ ..^ ..^ |
39 | | wlkres.e |
. . . . . . . . . . 11
iEdg ..^ |
40 | 39 | dmeqd 5326 |
. . . . . . . . . 10
iEdg ..^ |
41 | 40 | eleq2d 2687 |
. . . . . . . . 9
..^ iEdg
..^ ..^ |
42 | 41 | adantr 481 |
. . . . . . . 8
..^
..^ iEdg
..^ ..^ |
43 | 38, 42 | mpbird 247 |
. . . . . . 7
..^ ..^ iEdg |
44 | 43 | ralrimiva 2966 |
. . . . . 6
..^ ..^ iEdg |
45 | | ffnfv 6388 |
. . . . . 6
..^..^ iEdg ..^ ..^
..^
..^ iEdg |
46 | 12, 44, 45 | sylanbrc 698 |
. . . . 5
..^..^
iEdg |
47 | | fzossfz 12488 |
. . . . . . . . 9
..^ |
48 | 47, 7 | sseldi 3601 |
. . . . . . . 8
|
49 | | wlkreslem0 26565 |
. . . . . . . 8
Word
..^ |
50 | 25, 48, 49 | syl2anc 693 |
. . . . . . 7
..^ |
51 | 50 | oveq2d 6666 |
. . . . . 6
..^ ..^ ..^ |
52 | 51 | feq2d 6031 |
. . . . 5
..^..^ ..^ iEdg
..^..^ iEdg |
53 | 46, 52 | mpbird 247 |
. . . 4
..^..^ ..^ iEdg |
54 | | iswrdb 13311 |
. . . 4
..^ Word iEdg
..^..^ ..^ iEdg |
55 | 53, 54 | sylibr 224 |
. . 3
..^ Word
iEdg |
56 | 1, 55 | syl5eqel 2705 |
. 2
Word iEdg |
57 | | wlkres.v |
. . . . . . . 8
Vtx |
58 | 57 | wlkp 26512 |
. . . . . . 7
Walks |
59 | 2, 58 | syl 17 |
. . . . . 6
|
60 | | wlkres.s |
. . . . . . 7
Vtx |
61 | 60 | feq3d 6032 |
. . . . . 6
Vtx
|
62 | 59, 61 | mpbird 247 |
. . . . 5
Vtx |
63 | | elfzuz3 12339 |
. . . . . 6
|
64 | | fzss2 12381 |
. . . . . 6
|
65 | 48, 63, 64 | 3syl 18 |
. . . . 5
|
66 | 62, 65 | fssresd 6071 |
. . . 4
Vtx |
67 | 1 | fveq2i 6194 |
. . . . . . 7
..^ |
68 | 67, 50 | syl5eq 2668 |
. . . . . 6
|
69 | 68 | oveq2d 6666 |
. . . . 5
|
70 | 69 | feq2d 6031 |
. . . 4
Vtx
Vtx |
71 | 66, 70 | mpbird 247 |
. . 3
Vtx |
72 | | wlkres.q |
. . . 4
|
73 | 72 | feq1i 6036 |
. . 3
Vtx
Vtx |
74 | 71, 73 | sylibr 224 |
. 2
Vtx |
75 | | wlkv 26508 |
. . . . . . 7
Walks
|
76 | 57, 3 | iswlk 26506 |
. . . . . . . 8
Walks Word ..^if- |
77 | 76 | biimpd 219 |
. . . . . . 7
Walks Word ..^if- |
78 | 75, 77 | mpcom 38 |
. . . . . 6
Walks Word ..^if- |
79 | 2, 78 | syl 17 |
. . . . 5
Word ..^if- |
80 | 79 | adantr 481 |
. . . 4
..^ Word ..^if- |
81 | 68 | oveq2d 6666 |
. . . . . . . . . . 11
..^ ..^ |
82 | 81 | eleq2d 2687 |
. . . . . . . . . 10
..^
..^ |
83 | 72 | fveq1i 6192 |
. . . . . . . . . . . . 13
|
84 | | fzossfz 12488 |
. . . . . . . . . . . . . . . 16
..^ |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . 15
..^ |
86 | 85 | sselda 3603 |
. . . . . . . . . . . . . 14
..^ |
87 | 86 | fvresd 6208 |
. . . . . . . . . . . . 13
..^ |
88 | 83, 87 | syl5req 2669 |
. . . . . . . . . . . 12
..^ |
89 | 72 | fveq1i 6192 |
. . . . . . . . . . . . 13
|
90 | | fzofzp1 12565 |
. . . . . . . . . . . . . . 15
..^
|
91 | 90 | adantl 482 |
. . . . . . . . . . . . . 14
..^ |
92 | 91 | fvresd 6208 |
. . . . . . . . . . . . 13
..^ |
93 | 89, 92 | syl5req 2669 |
. . . . . . . . . . . 12
..^
|
94 | 88, 93 | jca 554 |
. . . . . . . . . . 11
..^
|
95 | 94 | ex 450 |
. . . . . . . . . 10
..^
|
96 | 82, 95 | sylbid 230 |
. . . . . . . . 9
..^
|
97 | 96 | imp 445 |
. . . . . . . 8
..^
|
98 | 25 | ancli 574 |
. . . . . . . . . . . . . 14
Word |
99 | 26 | ffund 6049 |
. . . . . . . . . . . . . . . . 17
Word
|
100 | 99 | adantl 482 |
. . . . . . . . . . . . . . . 16
Word |
101 | 100 | adantr 481 |
. . . . . . . . . . . . . . 15
Word
..^ |
102 | | fdm 6051 |
. . . . . . . . . . . . . . . . . 18
..^
..^ |
103 | | sseq2 3627 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
..^ ..^ |
104 | 10, 103 | syl5ibr 236 |
. . . . . . . . . . . . . . . . . 18
..^ ..^
|
105 | 26, 102, 104 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
Word
..^
|
106 | 105 | impcom 446 |
. . . . . . . . . . . . . . . 16
Word ..^ |
107 | 106 | adantr 481 |
. . . . . . . . . . . . . . 15
Word
..^ ..^
|
108 | | simpr 477 |
. . . . . . . . . . . . . . 15
Word
..^
..^ |
109 | 101, 107,
108 | resfvresima 6494 |
. . . . . . . . . . . . . 14
Word
..^ ..^ ..^ |
110 | 98, 109 | sylan 488 |
. . . . . . . . . . . . 13
..^ ..^
..^ |
111 | 110 | eqcomd 2628 |
. . . . . . . . . . . 12
..^
..^ ..^ |
112 | 111 | ex 450 |
. . . . . . . . . . 11
..^
..^ ..^ |
113 | 82, 112 | sylbid 230 |
. . . . . . . . . 10
..^ ..^ ..^ |
114 | 113 | imp 445 |
. . . . . . . . 9
..^
..^ ..^ |
115 | 39 | adantr 481 |
. . . . . . . . . 10
..^ iEdg ..^ |
116 | 1 | fveq1i 6192 |
. . . . . . . . . . 11
..^ |
117 | 116 | a1i 11 |
. . . . . . . . . 10
..^
..^ |
118 | 115, 117 | fveq12d 6197 |
. . . . . . . . 9
..^ iEdg ..^ ..^ |
119 | 114, 118 | eqtr4d 2659 |
. . . . . . . 8
..^ iEdg |
120 | 97, 119 | jca 554 |
. . . . . . 7
..^
iEdg |
121 | 7, 8 | syl 17 |
. . . . . . . . . . 11
|
122 | 1 | a1i 11 |
. . . . . . . . . . . . . 14
..^ |
123 | 122 | fveq2d 6195 |
. . . . . . . . . . . . 13
..^ |
124 | 123, 50 | eqtrd 2656 |
. . . . . . . . . . . 12
|
125 | 124 | fveq2d 6195 |
. . . . . . . . . . 11
|
126 | 121, 125 | eleqtrrd 2704 |
. . . . . . . . . 10
|
127 | | fzoss2 12496 |
. . . . . . . . . 10
..^ ..^ |
128 | 126, 127 | syl 17 |
. . . . . . . . 9
..^ ..^ |
129 | 128 | sselda 3603 |
. . . . . . . 8
..^
..^ |
130 | | wkslem1 26503 |
. . . . . . . . 9
if-
if-
|
131 | 130 | rspcv 3305 |
. . . . . . . 8
..^
..^if- if-
|
132 | 129, 131 | syl 17 |
. . . . . . 7
..^ ..^if- if-
|
133 | | eqeq12 2635 |
. . . . . . . . . 10
|
134 | 133 | adantr 481 |
. . . . . . . . 9
iEdg |
135 | | simpr 477 |
. . . . . . . . . 10
iEdg iEdg |
136 | | sneq 4187 |
. . . . . . . . . . . 12
|
137 | 136 | adantr 481 |
. . . . . . . . . . 11
|
138 | 137 | adantr 481 |
. . . . . . . . . 10
iEdg |
139 | 135, 138 | eqeq12d 2637 |
. . . . . . . . 9
iEdg
iEdg |
140 | | preq12 4270 |
. . . . . . . . . . 11
|
141 | 140 | adantr 481 |
. . . . . . . . . 10
iEdg |
142 | 141, 135 | sseq12d 3634 |
. . . . . . . . 9
iEdg
iEdg |
143 | 134, 139,
142 | ifpbi123d 1027 |
. . . . . . . 8
iEdg if-
if- iEdg
iEdg |
144 | 143 | biimpd 219 |
. . . . . . 7
iEdg if-
if- iEdg
iEdg |
145 | 120, 132,
144 | sylsyld 61 |
. . . . . 6
..^ ..^if- if-
iEdg iEdg |
146 | 145 | com12 32 |
. . . . 5
..^if- ..^ if- iEdg
iEdg |
147 | 146 | 3ad2ant3 1084 |
. . . 4
Word ..^if-
..^ if- iEdg
iEdg |
148 | 80, 147 | mpcom 38 |
. . 3
..^ if- iEdg
iEdg |
149 | 148 | ralrimiva 2966 |
. 2
..^if-
iEdg iEdg |
150 | 57, 3, 2, 7, 60, 39, 1, 72 | wlkreslem 26566 |
. . 3
|
151 | | eqid 2622 |
. . . 4
Vtx Vtx |
152 | | eqid 2622 |
. . . 4
iEdg iEdg |
153 | 151, 152 | iswlk 26506 |
. . 3
Walks Word iEdg Vtx
..^if-
iEdg iEdg |
154 | 150, 153 | syl 17 |
. 2
Walks
Word iEdg
Vtx ..^if-
iEdg iEdg |
155 | 56, 74, 149, 154 | mpbir3and 1245 |
1
Walks |