| Step |
Hyp |
Ref |
Expression |
| 1 |
|
upgrimwlk.i |
|- I = ( iEdg ` G ) |
| 2 |
|
upgrimwlk.j |
|- J = ( iEdg ` H ) |
| 3 |
|
upgrimwlk.g |
|- ( ph -> G e. USPGraph ) |
| 4 |
|
upgrimwlk.h |
|- ( ph -> H e. USPGraph ) |
| 5 |
|
upgrimwlk.n |
|- ( ph -> N e. ( G GraphIso H ) ) |
| 6 |
|
upgrimwlk.e |
|- E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) ) |
| 7 |
|
upgrimwlk.w |
|- ( ph -> F ( Walks ` G ) P ) |
| 8 |
1
|
wlkf |
|- ( F ( Walks ` G ) P -> F e. Word dom I ) |
| 9 |
7 8
|
syl |
|- ( ph -> F e. Word dom I ) |
| 10 |
1 2 3 4 5 6 9
|
upgrimwlklem1 |
|- ( ph -> ( # ` E ) = ( # ` F ) ) |
| 11 |
10
|
oveq2d |
|- ( ph -> ( 0 ..^ ( # ` E ) ) = ( 0 ..^ ( # ` F ) ) ) |
| 12 |
11
|
eleq2d |
|- ( ph -> ( i e. ( 0 ..^ ( # ` E ) ) <-> i e. ( 0 ..^ ( # ` F ) ) ) ) |
| 13 |
|
uspgrupgr |
|- ( G e. USPGraph -> G e. UPGraph ) |
| 14 |
3 13
|
syl |
|- ( ph -> G e. UPGraph ) |
| 15 |
1
|
upgrwlkedg |
|- ( ( G e. UPGraph /\ F ( Walks ` G ) P ) -> A. x e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` x ) ) = { ( P ` x ) , ( P ` ( x + 1 ) ) } ) |
| 16 |
14 7 15
|
syl2anc |
|- ( ph -> A. x e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` x ) ) = { ( P ` x ) , ( P ` ( x + 1 ) ) } ) |
| 17 |
|
2fveq3 |
|- ( x = i -> ( I ` ( F ` x ) ) = ( I ` ( F ` i ) ) ) |
| 18 |
|
fveq2 |
|- ( x = i -> ( P ` x ) = ( P ` i ) ) |
| 19 |
|
fvoveq1 |
|- ( x = i -> ( P ` ( x + 1 ) ) = ( P ` ( i + 1 ) ) ) |
| 20 |
18 19
|
preq12d |
|- ( x = i -> { ( P ` x ) , ( P ` ( x + 1 ) ) } = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) |
| 21 |
17 20
|
eqeq12d |
|- ( x = i -> ( ( I ` ( F ` x ) ) = { ( P ` x ) , ( P ` ( x + 1 ) ) } <-> ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) |
| 22 |
21
|
rspcv |
|- ( i e. ( 0 ..^ ( # ` F ) ) -> ( A. x e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` x ) ) = { ( P ` x ) , ( P ` ( x + 1 ) ) } -> ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) |
| 23 |
22
|
adantl |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( A. x e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` x ) ) = { ( P ` x ) , ( P ` ( x + 1 ) ) } -> ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) |
| 24 |
|
imaeq2 |
|- ( ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> ( N " ( I ` ( F ` i ) ) ) = ( N " { ( P ` i ) , ( P ` ( i + 1 ) ) } ) ) |
| 25 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
| 26 |
|
eqid |
|- ( Vtx ` H ) = ( Vtx ` H ) |
| 27 |
25 26
|
grimf1o |
|- ( N e. ( G GraphIso H ) -> N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) ) |
| 28 |
|
f1ofn |
|- ( N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> N Fn ( Vtx ` G ) ) |
| 29 |
5 27 28
|
3syl |
|- ( ph -> N Fn ( Vtx ` G ) ) |
| 30 |
29
|
adantr |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> N Fn ( Vtx ` G ) ) |
| 31 |
25
|
wlkp |
|- ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) |
| 32 |
7 31
|
syl |
|- ( ph -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) |
| 33 |
32
|
adantr |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) |
| 34 |
|
elfzofz |
|- ( i e. ( 0 ..^ ( # ` F ) ) -> i e. ( 0 ... ( # ` F ) ) ) |
| 35 |
34
|
adantl |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> i e. ( 0 ... ( # ` F ) ) ) |
| 36 |
33 35
|
ffvelcdmd |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` i ) e. ( Vtx ` G ) ) |
| 37 |
|
fzofzp1 |
|- ( i e. ( 0 ..^ ( # ` F ) ) -> ( i + 1 ) e. ( 0 ... ( # ` F ) ) ) |
| 38 |
37
|
adantl |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( i + 1 ) e. ( 0 ... ( # ` F ) ) ) |
| 39 |
33 38
|
ffvelcdmd |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` ( i + 1 ) ) e. ( Vtx ` G ) ) |
| 40 |
|
fnimapr |
|- ( ( N Fn ( Vtx ` G ) /\ ( P ` i ) e. ( Vtx ` G ) /\ ( P ` ( i + 1 ) ) e. ( Vtx ` G ) ) -> ( N " { ( P ` i ) , ( P ` ( i + 1 ) ) } ) = { ( N ` ( P ` i ) ) , ( N ` ( P ` ( i + 1 ) ) ) } ) |
| 41 |
30 36 39 40
|
syl3anc |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( N " { ( P ` i ) , ( P ` ( i + 1 ) ) } ) = { ( N ` ( P ` i ) ) , ( N ` ( P ` ( i + 1 ) ) ) } ) |
| 42 |
7
|
adantr |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> F ( Walks ` G ) P ) |
| 43 |
42 31
|
syl |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) |
| 44 |
43 35
|
fvco3d |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( N o. P ) ` i ) = ( N ` ( P ` i ) ) ) |
| 45 |
33 38
|
fvco3d |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( N o. P ) ` ( i + 1 ) ) = ( N ` ( P ` ( i + 1 ) ) ) ) |
| 46 |
44 45
|
preq12d |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } = { ( N ` ( P ` i ) ) , ( N ` ( P ` ( i + 1 ) ) ) } ) |
| 47 |
41 46
|
eqtr4d |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( N " { ( P ` i ) , ( P ` ( i + 1 ) ) } ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } ) |
| 48 |
24 47
|
sylan9eqr |
|- ( ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) /\ ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) -> ( N " ( I ` ( F ` i ) ) ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } ) |
| 49 |
48
|
ex |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( ( I ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } -> ( N " ( I ` ( F ` i ) ) ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } ) ) |
| 50 |
23 49
|
syld |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( A. x e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` x ) ) = { ( P ` x ) , ( P ` ( x + 1 ) ) } -> ( N " ( I ` ( F ` i ) ) ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } ) ) |
| 51 |
50
|
ex |
|- ( ph -> ( i e. ( 0 ..^ ( # ` F ) ) -> ( A. x e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` x ) ) = { ( P ` x ) , ( P ` ( x + 1 ) ) } -> ( N " ( I ` ( F ` i ) ) ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } ) ) ) |
| 52 |
16 51
|
mpid |
|- ( ph -> ( i e. ( 0 ..^ ( # ` F ) ) -> ( N " ( I ` ( F ` i ) ) ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } ) ) |
| 53 |
12 52
|
sylbid |
|- ( ph -> ( i e. ( 0 ..^ ( # ` E ) ) -> ( N " ( I ` ( F ` i ) ) ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } ) ) |
| 54 |
53
|
imp |
|- ( ( ph /\ i e. ( 0 ..^ ( # ` E ) ) ) -> ( N " ( I ` ( F ` i ) ) ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } ) |