Step |
Hyp |
Ref |
Expression |
1 |
|
wlkn0 |
|- ( F ( Walks ` G ) P -> P =/= (/) ) |
2 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
3 |
|
eqid |
|- ( iEdg ` G ) = ( iEdg ` G ) |
4 |
2 3
|
upgriswlk |
|- ( G e. UPGraph -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) ) |
5 |
|
simpr |
|- ( ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) /\ P =/= (/) ) -> P =/= (/) ) |
6 |
|
ffz0iswrd |
|- ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> P e. Word ( Vtx ` G ) ) |
7 |
6
|
3ad2ant2 |
|- ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> P e. Word ( Vtx ` G ) ) |
8 |
7
|
ad2antlr |
|- ( ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) /\ P =/= (/) ) -> P e. Word ( Vtx ` G ) ) |
9 |
|
upgruhgr |
|- ( G e. UPGraph -> G e. UHGraph ) |
10 |
3
|
uhgrfun |
|- ( G e. UHGraph -> Fun ( iEdg ` G ) ) |
11 |
|
funfn |
|- ( Fun ( iEdg ` G ) <-> ( iEdg ` G ) Fn dom ( iEdg ` G ) ) |
12 |
11
|
biimpi |
|- ( Fun ( iEdg ` G ) -> ( iEdg ` G ) Fn dom ( iEdg ` G ) ) |
13 |
9 10 12
|
3syl |
|- ( G e. UPGraph -> ( iEdg ` G ) Fn dom ( iEdg ` G ) ) |
14 |
13
|
ad2antlr |
|- ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ G e. UPGraph ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( iEdg ` G ) Fn dom ( iEdg ` G ) ) |
15 |
|
wrdsymbcl |
|- ( ( F e. Word dom ( iEdg ` G ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` i ) e. dom ( iEdg ` G ) ) |
16 |
15
|
ad4ant14 |
|- ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ G e. UPGraph ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` i ) e. dom ( iEdg ` G ) ) |
17 |
|
fnfvelrn |
|- ( ( ( iEdg ` G ) Fn dom ( iEdg ` G ) /\ ( F ` i ) e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` ( F ` i ) ) e. ran ( iEdg ` G ) ) |
18 |
14 16 17
|
syl2anc |
|- ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ G e. UPGraph ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` i ) ) e. ran ( iEdg ` G ) ) |
19 |
|
edgval |
|- ( Edg ` G ) = ran ( iEdg ` G ) |
20 |
18 19
|
eleqtrrdi |
|- ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ G e. UPGraph ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` G ) ` ( F ` i ) ) e. ( Edg ` G ) ) |
21 |
|
eleq1 |
|- ( { ( P ` i ) , ( P ` ( i + 1 ) ) } = ( ( iEdg ` G ) ` ( F ` i ) ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( ( iEdg ` G ) ` ( F ` i ) ) e. ( Edg ` G ) ) ) |
22 |
21
|
eqcoms |
|- ( ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) <-> ( ( iEdg ` G ) ` ( F ` i ) ) e. ( Edg ` G ) ) ) |
23 |
20 22
|
syl5ibrcom |
|- ( ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ G e. UPGraph ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) |
24 |
23
|
ralimdva |
|- ( ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ G e. UPGraph ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) |
25 |
24
|
ex |
|- ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( G e. UPGraph -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) ) |
26 |
25
|
com23 |
|- ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> ( G e. UPGraph -> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) ) |
27 |
26
|
3impia |
|- ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( G e. UPGraph -> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) |
28 |
27
|
impcom |
|- ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) -> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) |
29 |
|
lencl |
|- ( F e. Word dom ( iEdg ` G ) -> ( # ` F ) e. NN0 ) |
30 |
|
ffz0hash |
|- ( ( ( # ` F ) e. NN0 /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( # ` P ) = ( ( # ` F ) + 1 ) ) |
31 |
30
|
ex |
|- ( ( # ` F ) e. NN0 -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( # ` P ) = ( ( # ` F ) + 1 ) ) ) |
32 |
|
oveq1 |
|- ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( ( # ` P ) - 1 ) = ( ( ( # ` F ) + 1 ) - 1 ) ) |
33 |
|
nn0cn |
|- ( ( # ` F ) e. NN0 -> ( # ` F ) e. CC ) |
34 |
|
pncan1 |
|- ( ( # ` F ) e. CC -> ( ( ( # ` F ) + 1 ) - 1 ) = ( # ` F ) ) |
35 |
33 34
|
syl |
|- ( ( # ` F ) e. NN0 -> ( ( ( # ` F ) + 1 ) - 1 ) = ( # ` F ) ) |
36 |
32 35
|
sylan9eqr |
|- ( ( ( # ` F ) e. NN0 /\ ( # ` P ) = ( ( # ` F ) + 1 ) ) -> ( ( # ` P ) - 1 ) = ( # ` F ) ) |
37 |
36
|
ex |
|- ( ( # ` F ) e. NN0 -> ( ( # ` P ) = ( ( # ` F ) + 1 ) -> ( ( # ` P ) - 1 ) = ( # ` F ) ) ) |
38 |
31 37
|
syld |
|- ( ( # ` F ) e. NN0 -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( # ` P ) - 1 ) = ( # ` F ) ) ) |
39 |
29 38
|
syl |
|- ( F e. Word dom ( iEdg ` G ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( # ` P ) - 1 ) = ( # ` F ) ) ) |
40 |
39
|
imp |
|- ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( ( # ` P ) - 1 ) = ( # ` F ) ) |
41 |
40
|
oveq2d |
|- ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( 0 ..^ ( ( # ` P ) - 1 ) ) = ( 0 ..^ ( # ` F ) ) ) |
42 |
41
|
raleqdv |
|- ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) |
43 |
42
|
3adant3 |
|- ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) |
44 |
43
|
adantl |
|- ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) -> ( A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) <-> A. i e. ( 0 ..^ ( # ` F ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) |
45 |
28 44
|
mpbird |
|- ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) |
46 |
45
|
adantr |
|- ( ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) /\ P =/= (/) ) -> A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) |
47 |
|
eqid |
|- ( Edg ` G ) = ( Edg ` G ) |
48 |
2 47
|
iswwlks |
|- ( P e. ( WWalks ` G ) <-> ( P =/= (/) /\ P e. Word ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ( Edg ` G ) ) ) |
49 |
5 8 46 48
|
syl3anbrc |
|- ( ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) /\ P =/= (/) ) -> P e. ( WWalks ` G ) ) |
50 |
49
|
ex |
|- ( ( G e. UPGraph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) -> ( P =/= (/) -> P e. ( WWalks ` G ) ) ) |
51 |
50
|
ex |
|- ( G e. UPGraph -> ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( P =/= (/) -> P e. ( WWalks ` G ) ) ) ) |
52 |
4 51
|
sylbid |
|- ( G e. UPGraph -> ( F ( Walks ` G ) P -> ( P =/= (/) -> P e. ( WWalks ` G ) ) ) ) |
53 |
1 52
|
mpdi |
|- ( G e. UPGraph -> ( F ( Walks ` G ) P -> P e. ( WWalks ` G ) ) ) |