Metamath Proof Explorer

Theorem upgrimtrls

Description: Graph isomorphisms between simple pseudographs map trails onto trails. (Contributed by AV, 29-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 ) ) ) ) )
upgrimtrls.t 
|- ( ph -> F ( Trails ` G ) P )
Assertion upgrimtrls 
|- ( ph -> E ( Trails ` 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 upgrimtrls.t 
 |-  ( ph -> F ( Trails ` G ) P )
8 trliswlk 
 |-  ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
9 7 8 syl 
 |-  ( ph -> F ( Walks ` G ) P )
10 1 2 3 4 5 6 9 upgrimwlk 
 |-  ( ph -> E ( Walks ` H ) ( N o. P ) )
11 4 adantr 
 |-  ( ( ph /\ x e. dom F ) -> H e. USPGraph )
12 2 uspgrf1oedg 
 |-  ( H e. USPGraph -> J : dom J -1-1-onto-> ( Edg ` H ) )
13 11 12 syl 
 |-  ( ( ph /\ x e. dom F ) -> J : dom J -1-1-onto-> ( Edg ` H ) )
14 1 2 3 4 5 6 7 upgrimtrlslem1 
 |-  ( ( ph /\ x e. dom F ) -> ( N " ( I ` ( F ` x ) ) ) e. ( Edg ` H ) )
15 f1ocnvdm 
 |-  ( ( J : dom J -1-1-onto-> ( Edg ` H ) /\ ( N " ( I ` ( F ` x ) ) ) e. ( Edg ` H ) ) -> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) e. dom J )
16 13 14 15 syl2anc 
 |-  ( ( ph /\ x e. dom F ) -> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) e. dom J )
17 16 ralrimiva 
 |-  ( ph -> A. x e. dom F ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) e. dom J )
18 1 2 3 4 5 6 7 upgrimtrlslem2 
 |-  ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` y ) ) ) ) -> x = y ) )
19 18 ralrimivva 
 |-  ( ph -> A. x e. dom F A. y e. dom F ( ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` y ) ) ) ) -> x = y ) )
20 2fveq3 
 |-  ( x = y -> ( I ` ( F ` x ) ) = ( I ` ( F ` y ) ) )
21 20 imaeq2d 
 |-  ( x = y -> ( N " ( I ` ( F ` x ) ) ) = ( N " ( I ` ( F ` y ) ) ) )
22 21 fveq2d 
 |-  ( x = y -> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` y ) ) ) ) )
23 6 22 f1mpt 
 |-  ( E : dom F -1-1-> dom J <-> ( A. x e. dom F ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) e. dom J /\ A. x e. dom F A. y e. dom F ( ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` y ) ) ) ) -> x = y ) ) )
24 17 19 23 sylanbrc 
 |-  ( ph -> E : dom F -1-1-> dom J )
25 eqidd 
 |-  ( ph -> E = E )
26 1 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
27 7 8 26 3syl 
 |-  ( ph -> F e. Word dom I )
28 1 2 3 4 5 6 27 upgrimwlklem1 
 |-  ( ph -> ( # ` E ) = ( # ` F ) )
29 28 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` E ) ) = ( 0 ..^ ( # ` F ) ) )
30 wrddm 
 |-  ( F e. Word dom I -> dom F = ( 0 ..^ ( # ` F ) ) )
31 8 26 30 3syl 
 |-  ( F ( Trails ` G ) P -> dom F = ( 0 ..^ ( # ` F ) ) )
32 7 31 syl 
 |-  ( ph -> dom F = ( 0 ..^ ( # ` F ) ) )
33 29 32 eqtr4d 
 |-  ( ph -> ( 0 ..^ ( # ` E ) ) = dom F )
34 eqidd 
 |-  ( ph -> dom J = dom J )
35 25 33 34 f1eq123d 
 |-  ( ph -> ( E : ( 0 ..^ ( # ` E ) ) -1-1-> dom J <-> E : dom F -1-1-> dom J ) )
36 24 35 mpbird 
 |-  ( ph -> E : ( 0 ..^ ( # ` E ) ) -1-1-> dom J )
37 df-f1 
 |-  ( E : ( 0 ..^ ( # ` E ) ) -1-1-> dom J <-> ( E : ( 0 ..^ ( # ` E ) ) --> dom J /\ Fun `' E ) )
38 37 simprbi 
 |-  ( E : ( 0 ..^ ( # ` E ) ) -1-1-> dom J -> Fun `' E )
39 36 38 syl 
 |-  ( ph -> Fun `' E )
40 istrl 
 |-  ( E ( Trails ` H ) ( N o. P ) <-> ( E ( Walks ` H ) ( N o. P ) /\ Fun `' E ) )
41 10 39 40 sylanbrc 
 |-  ( ph -> E ( Trails ` H ) ( N o. P ) )