Metamath Proof Explorer

Theorem upgrimwlk

Description: Graph isomorphisms between simple pseudographs map walks onto walks. (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 upgrimwlk 
|- ( ph -> E ( Walks ` H ) ( N o. P ) )

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 upgrimwlklem2 
 |-  ( ph -> E e. Word dom J )
11 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
12 11 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
13 7 12 syl 
 |-  ( ph -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
14 1 2 3 4 5 6 9 13 upgrimwlklem4 
 |-  ( ph -> ( N o. P ) : ( 0 ... ( # ` E ) ) --> ( Vtx ` H ) )
15 1 2 3 4 5 6 9 upgrimwlklem3 
 |-  ( ( ph /\ i e. ( 0 ..^ ( # ` E ) ) ) -> ( J ` ( E ` i ) ) = ( N " ( I ` ( F ` i ) ) ) )
16 1 2 3 4 5 6 7 upgrimwlklem5 
 |-  ( ( ph /\ i e. ( 0 ..^ ( # ` E ) ) ) -> ( N " ( I ` ( F ` i ) ) ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } )
17 15 16 eqtrd 
 |-  ( ( ph /\ i e. ( 0 ..^ ( # ` E ) ) ) -> ( J ` ( E ` i ) ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } )
18 17 ralrimiva 
 |-  ( ph -> A. i e. ( 0 ..^ ( # ` E ) ) ( J ` ( E ` i ) ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } )
19 uspgrupgr 
 |-  ( H e. USPGraph -> H e. UPGraph )
20 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
21 20 2 upgriswlk 
 |-  ( H e. UPGraph -> ( E ( Walks ` H ) ( N o. P ) <-> ( E e. Word dom J /\ ( N o. P ) : ( 0 ... ( # ` E ) ) --> ( Vtx ` H ) /\ A. i e. ( 0 ..^ ( # ` E ) ) ( J ` ( E ` i ) ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } ) ) )
22 4 19 21 3syl 
 |-  ( ph -> ( E ( Walks ` H ) ( N o. P ) <-> ( E e. Word dom J /\ ( N o. P ) : ( 0 ... ( # ` E ) ) --> ( Vtx ` H ) /\ A. i e. ( 0 ..^ ( # ` E ) ) ( J ` ( E ` i ) ) = { ( ( N o. P ) ` i ) , ( ( N o. P ) ` ( i + 1 ) ) } ) ) )
23 10 14 18 22 mpbir3and 
 |-  ( ph -> E ( Walks ` H ) ( N o. P ) )