Step |
Hyp |
Ref |
Expression |
1 |
|
wlkcpr |
|- ( W e. ( Walks ` G ) <-> ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) ) |
2 |
|
eqid |
|- ( iEdg ` G ) = ( iEdg ` G ) |
3 |
2
|
wlkf |
|- ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> ( 1st ` W ) e. Word dom ( iEdg ` G ) ) |
4 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
5 |
4
|
wlkp |
|- ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) ) |
6 |
3 5
|
jca |
|- ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) ) ) |
7 |
|
feq3 |
|- ( ( Vtx ` G ) = (/) -> ( ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) <-> ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> (/) ) ) |
8 |
|
f00 |
|- ( ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> (/) <-> ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) ) |
9 |
7 8
|
bitrdi |
|- ( ( Vtx ` G ) = (/) -> ( ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) <-> ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) ) ) |
10 |
|
0z |
|- 0 e. ZZ |
11 |
|
nn0z |
|- ( ( # ` ( 1st ` W ) ) e. NN0 -> ( # ` ( 1st ` W ) ) e. ZZ ) |
12 |
|
fzn |
|- ( ( 0 e. ZZ /\ ( # ` ( 1st ` W ) ) e. ZZ ) -> ( ( # ` ( 1st ` W ) ) < 0 <-> ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) ) |
13 |
10 11 12
|
sylancr |
|- ( ( # ` ( 1st ` W ) ) e. NN0 -> ( ( # ` ( 1st ` W ) ) < 0 <-> ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) ) |
14 |
|
nn0nlt0 |
|- ( ( # ` ( 1st ` W ) ) e. NN0 -> -. ( # ` ( 1st ` W ) ) < 0 ) |
15 |
14
|
pm2.21d |
|- ( ( # ` ( 1st ` W ) ) e. NN0 -> ( ( # ` ( 1st ` W ) ) < 0 -> ( 1st ` W ) = (/) ) ) |
16 |
13 15
|
sylbird |
|- ( ( # ` ( 1st ` W ) ) e. NN0 -> ( ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) -> ( 1st ` W ) = (/) ) ) |
17 |
16
|
com12 |
|- ( ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) -> ( ( # ` ( 1st ` W ) ) e. NN0 -> ( 1st ` W ) = (/) ) ) |
18 |
17
|
adantl |
|- ( ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) -> ( ( # ` ( 1st ` W ) ) e. NN0 -> ( 1st ` W ) = (/) ) ) |
19 |
|
lencl |
|- ( ( 1st ` W ) e. Word dom ( iEdg ` G ) -> ( # ` ( 1st ` W ) ) e. NN0 ) |
20 |
18 19
|
impel |
|- ( ( ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) /\ ( 1st ` W ) e. Word dom ( iEdg ` G ) ) -> ( 1st ` W ) = (/) ) |
21 |
|
simpll |
|- ( ( ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) /\ ( 1st ` W ) e. Word dom ( iEdg ` G ) ) -> ( 2nd ` W ) = (/) ) |
22 |
20 21
|
jca |
|- ( ( ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) /\ ( 1st ` W ) e. Word dom ( iEdg ` G ) ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) ) |
23 |
22
|
ex |
|- ( ( ( 2nd ` W ) = (/) /\ ( 0 ... ( # ` ( 1st ` W ) ) ) = (/) ) -> ( ( 1st ` W ) e. Word dom ( iEdg ` G ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) ) ) |
24 |
9 23
|
syl6bi |
|- ( ( Vtx ` G ) = (/) -> ( ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) -> ( ( 1st ` W ) e. Word dom ( iEdg ` G ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) ) ) ) |
25 |
24
|
impcomd |
|- ( ( Vtx ` G ) = (/) -> ( ( ( 1st ` W ) e. Word dom ( iEdg ` G ) /\ ( 2nd ` W ) : ( 0 ... ( # ` ( 1st ` W ) ) ) --> ( Vtx ` G ) ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) ) ) |
26 |
6 25
|
syl5 |
|- ( ( Vtx ` G ) = (/) -> ( ( 1st ` W ) ( Walks ` G ) ( 2nd ` W ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) ) ) |
27 |
1 26
|
syl5bi |
|- ( ( Vtx ` G ) = (/) -> ( W e. ( Walks ` G ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) ) ) |
28 |
27
|
imp |
|- ( ( ( Vtx ` G ) = (/) /\ W e. ( Walks ` G ) ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) ) |