Metamath Proof Explorer

Theorem upgrimwlklem5

Description: Lemma 5 for upgrimwlk . (Contributed by AV, 28-Oct-2025)

Ref Expression
Hypotheses upgrimwlk.i 
|- I = ( iEdg ` G )
upgrimwlk.j 
|- J = ( iEdg ` H )
upgrimwlk.g 
|- ( ph -> G e. USPGraph )
upgrimwlk.h 
|- ( ph -> H e. USPGraph )
upgrimwlk.n 
|- ( ph -> N e. ( G GraphIso H ) )
upgrimwlk.e 
|- E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) )
upgrimwlk.w 
|- ( ph -> F ( Walks ` G ) P )
Assertion upgrimwlklem5 
|- ( ( ph /\ i e. ( 0 ..^ ( # ` E ) ) ) -> ( N " ( I ` ( F ` i ) ) ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } )

Proof

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 ) ) } )