Metamath Proof Explorer

Theorem upgrimpths

Description: Graph isomorphisms between simple pseudographs map paths onto paths. (Contributed by AV, 31-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 ) ) ) ) )
upgrimpths.p 
|- ( ph -> F ( Paths ` G ) P )
Assertion upgrimpths 
|- ( ph -> E ( Paths ` 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 upgrimpths.p 
 |-  ( ph -> F ( Paths ` G ) P )
8 pthistrl 
 |-  ( F ( Paths ` G ) P -> F ( Trails ` G ) P )
9 7 8 syl 
 |-  ( ph -> F ( Trails ` G ) P )
10 1 2 3 4 5 6 9 upgrimtrls 
 |-  ( ph -> E ( Trails ` H ) ( N o. P ) )
11 1 2 3 4 5 6 7 upgrimpthslem1 
 |-  ( ph -> Fun `' ( ( N o. P ) |` ( 1 ..^ ( # ` F ) ) ) )
12 pthiswlk 
 |-  ( F ( Paths ` G ) P -> F ( Walks ` G ) P )
13 1 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
14 7 12 13 3syl 
 |-  ( ph -> F e. Word dom I )
15 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
16 15 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
17 7 12 16 3syl 
 |-  ( ph -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
18 1 2 3 4 5 6 14 17 upgrimwlklem4 
 |-  ( ph -> ( N o. P ) : ( 0 ... ( # ` E ) ) --> ( Vtx ` H ) )
19 18 ffnd 
 |-  ( ph -> ( N o. P ) Fn ( 0 ... ( # ` E ) ) )
20 1 2 3 4 5 6 14 upgrimwlklem1 
 |-  ( ph -> ( # ` E ) = ( # ` F ) )
21 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
22 7 12 21 3syl 
 |-  ( ph -> ( # ` F ) e. NN0 )
23 20 22 eqeltrd 
 |-  ( ph -> ( # ` E ) e. NN0 )
24 0elfz 
 |-  ( ( # ` E ) e. NN0 -> 0 e. ( 0 ... ( # ` E ) ) )
25 23 24 syl 
 |-  ( ph -> 0 e. ( 0 ... ( # ` E ) ) )
26 nn0fz0 
 |-  ( ( # ` F ) e. NN0 <-> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
27 22 26 sylib 
 |-  ( ph -> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
28 20 oveq2d 
 |-  ( ph -> ( 0 ... ( # ` E ) ) = ( 0 ... ( # ` F ) ) )
29 27 28 eleqtrrd 
 |-  ( ph -> ( # ` F ) e. ( 0 ... ( # ` E ) ) )
30 fnimapr 
 |-  ( ( ( N o. P ) Fn ( 0 ... ( # ` E ) ) /\ 0 e. ( 0 ... ( # ` E ) ) /\ ( # ` F ) e. ( 0 ... ( # ` E ) ) ) -> ( ( N o. P ) " { 0 , ( # ` F ) } ) = { ( ( N o. P ) ` 0 ) , ( ( N o. P ) ` ( # ` F ) ) } )
31 19 25 29 30 syl3anc 
 |-  ( ph -> ( ( N o. P ) " { 0 , ( # ` F ) } ) = { ( ( N o. P ) ` 0 ) , ( ( N o. P ) ` ( # ` F ) ) } )
32 31 eleq2d 
 |-  ( ph -> ( x e. ( ( N o. P ) " { 0 , ( # ` F ) } ) <-> x e. { ( ( N o. P ) ` 0 ) , ( ( N o. P ) ` ( # ` F ) ) } ) )
33 vex 
 |-  x e. _V
34 33 elpr 
 |-  ( x e. { ( ( N o. P ) ` 0 ) , ( ( N o. P ) ` ( # ` F ) ) } <-> ( x = ( ( N o. P ) ` 0 ) \/ x = ( ( N o. P ) ` ( # ` F ) ) ) )
35 32 34 bitrdi 
 |-  ( ph -> ( x e. ( ( N o. P ) " { 0 , ( # ` F ) } ) <-> ( x = ( ( N o. P ) ` 0 ) \/ x = ( ( N o. P ) ` ( # ` F ) ) ) ) )
36 1 2 3 4 5 6 7 upgrimpthslem2 
 |-  ( ( ph /\ y e. ( 1 ..^ ( # ` F ) ) ) -> ( -. ( ( N o. P ) ` y ) = ( ( N o. P ) ` 0 ) /\ -. ( ( N o. P ) ` y ) = ( ( N o. P ) ` ( # ` F ) ) ) )
37 36 simpld 
 |-  ( ( ph /\ y e. ( 1 ..^ ( # ` F ) ) ) -> -. ( ( N o. P ) ` y ) = ( ( N o. P ) ` 0 ) )
38 eqeq2 
 |-  ( x = ( ( N o. P ) ` 0 ) -> ( ( ( N o. P ) ` y ) = x <-> ( ( N o. P ) ` y ) = ( ( N o. P ) ` 0 ) ) )
39 38 notbid 
 |-  ( x = ( ( N o. P ) ` 0 ) -> ( -. ( ( N o. P ) ` y ) = x <-> -. ( ( N o. P ) ` y ) = ( ( N o. P ) ` 0 ) ) )
40 37 39 syl5ibrcom 
 |-  ( ( ph /\ y e. ( 1 ..^ ( # ` F ) ) ) -> ( x = ( ( N o. P ) ` 0 ) -> -. ( ( N o. P ) ` y ) = x ) )
41 36 simprd 
 |-  ( ( ph /\ y e. ( 1 ..^ ( # ` F ) ) ) -> -. ( ( N o. P ) ` y ) = ( ( N o. P ) ` ( # ` F ) ) )
42 eqeq2 
 |-  ( x = ( ( N o. P ) ` ( # ` F ) ) -> ( ( ( N o. P ) ` y ) = x <-> ( ( N o. P ) ` y ) = ( ( N o. P ) ` ( # ` F ) ) ) )
43 42 notbid 
 |-  ( x = ( ( N o. P ) ` ( # ` F ) ) -> ( -. ( ( N o. P ) ` y ) = x <-> -. ( ( N o. P ) ` y ) = ( ( N o. P ) ` ( # ` F ) ) ) )
44 41 43 syl5ibrcom 
 |-  ( ( ph /\ y e. ( 1 ..^ ( # ` F ) ) ) -> ( x = ( ( N o. P ) ` ( # ` F ) ) -> -. ( ( N o. P ) ` y ) = x ) )
45 40 44 jaod 
 |-  ( ( ph /\ y e. ( 1 ..^ ( # ` F ) ) ) -> ( ( x = ( ( N o. P ) ` 0 ) \/ x = ( ( N o. P ) ` ( # ` F ) ) ) -> -. ( ( N o. P ) ` y ) = x ) )
46 45 impancom 
 |-  ( ( ph /\ ( x = ( ( N o. P ) ` 0 ) \/ x = ( ( N o. P ) ` ( # ` F ) ) ) ) -> ( y e. ( 1 ..^ ( # ` F ) ) -> -. ( ( N o. P ) ` y ) = x ) )
47 46 imp 
 |-  ( ( ( ph /\ ( x = ( ( N o. P ) ` 0 ) \/ x = ( ( N o. P ) ` ( # ` F ) ) ) ) /\ y e. ( 1 ..^ ( # ` F ) ) ) -> -. ( ( N o. P ) ` y ) = x )
48 47 nrexdv 
 |-  ( ( ph /\ ( x = ( ( N o. P ) ` 0 ) \/ x = ( ( N o. P ) ` ( # ` F ) ) ) ) -> -. E. y e. ( 1 ..^ ( # ` F ) ) ( ( N o. P ) ` y ) = x )
49 20 eqcomd 
 |-  ( ph -> ( # ` F ) = ( # ` E ) )
50 49 oveq2d 
 |-  ( ph -> ( 0 ... ( # ` F ) ) = ( 0 ... ( # ` E ) ) )
51 50 feq2d 
 |-  ( ph -> ( ( N o. P ) : ( 0 ... ( # ` F ) ) --> ( Vtx ` H ) <-> ( N o. P ) : ( 0 ... ( # ` E ) ) --> ( Vtx ` H ) ) )
52 18 51 mpbird 
 |-  ( ph -> ( N o. P ) : ( 0 ... ( # ` F ) ) --> ( Vtx ` H ) )
53 52 ffnd 
 |-  ( ph -> ( N o. P ) Fn ( 0 ... ( # ` F ) ) )
54 53 adantr 
 |-  ( ( ph /\ ( x = ( ( N o. P ) ` 0 ) \/ x = ( ( N o. P ) ` ( # ` F ) ) ) ) -> ( N o. P ) Fn ( 0 ... ( # ` F ) ) )
55 fzo0ss1 
 |-  ( 1 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` F ) )
56 fzossfz 
 |-  ( 0 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
57 55 56 sstri 
 |-  ( 1 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
58 57 a1i 
 |-  ( ( ph /\ ( x = ( ( N o. P ) ` 0 ) \/ x = ( ( N o. P ) ` ( # ` F ) ) ) ) -> ( 1 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) ) )
59 54 58 fvelimabd 
 |-  ( ( ph /\ ( x = ( ( N o. P ) ` 0 ) \/ x = ( ( N o. P ) ` ( # ` F ) ) ) ) -> ( x e. ( ( N o. P ) " ( 1 ..^ ( # ` F ) ) ) <-> E. y e. ( 1 ..^ ( # ` F ) ) ( ( N o. P ) ` y ) = x ) )
60 48 59 mtbird 
 |-  ( ( ph /\ ( x = ( ( N o. P ) ` 0 ) \/ x = ( ( N o. P ) ` ( # ` F ) ) ) ) -> -. x e. ( ( N o. P ) " ( 1 ..^ ( # ` F ) ) ) )
61 60 ex 
 |-  ( ph -> ( ( x = ( ( N o. P ) ` 0 ) \/ x = ( ( N o. P ) ` ( # ` F ) ) ) -> -. x e. ( ( N o. P ) " ( 1 ..^ ( # ` F ) ) ) ) )
62 35 61 sylbid 
 |-  ( ph -> ( x e. ( ( N o. P ) " { 0 , ( # ` F ) } ) -> -. x e. ( ( N o. P ) " ( 1 ..^ ( # ` F ) ) ) ) )
63 62 ralrimiv 
 |-  ( ph -> A. x e. ( ( N o. P ) " { 0 , ( # ` F ) } ) -. x e. ( ( N o. P ) " ( 1 ..^ ( # ` F ) ) ) )
64 disj 
 |-  ( ( ( ( N o. P ) " { 0 , ( # ` F ) } ) i^i ( ( N o. P ) " ( 1 ..^ ( # ` F ) ) ) ) = (/) <-> A. x e. ( ( N o. P ) " { 0 , ( # ` F ) } ) -. x e. ( ( N o. P ) " ( 1 ..^ ( # ` F ) ) ) )
65 63 64 sylibr 
 |-  ( ph -> ( ( ( N o. P ) " { 0 , ( # ` F ) } ) i^i ( ( N o. P ) " ( 1 ..^ ( # ` F ) ) ) ) = (/) )
66 20 oveq2d 
 |-  ( ph -> ( 1 ..^ ( # ` E ) ) = ( 1 ..^ ( # ` F ) ) )
67 66 reseq2d 
 |-  ( ph -> ( ( N o. P ) |` ( 1 ..^ ( # ` E ) ) ) = ( ( N o. P ) |` ( 1 ..^ ( # ` F ) ) ) )
68 67 cnveqd 
 |-  ( ph -> `' ( ( N o. P ) |` ( 1 ..^ ( # ` E ) ) ) = `' ( ( N o. P ) |` ( 1 ..^ ( # ` F ) ) ) )
69 68 funeqd 
 |-  ( ph -> ( Fun `' ( ( N o. P ) |` ( 1 ..^ ( # ` E ) ) ) <-> Fun `' ( ( N o. P ) |` ( 1 ..^ ( # ` F ) ) ) ) )
70 preq2 
 |-  ( ( # ` E ) = ( # ` F ) -> { 0 , ( # ` E ) } = { 0 , ( # ` F ) } )
71 70 imaeq2d 
 |-  ( ( # ` E ) = ( # ` F ) -> ( ( N o. P ) " { 0 , ( # ` E ) } ) = ( ( N o. P ) " { 0 , ( # ` F ) } ) )
72 oveq2 
 |-  ( ( # ` E ) = ( # ` F ) -> ( 1 ..^ ( # ` E ) ) = ( 1 ..^ ( # ` F ) ) )
73 72 imaeq2d 
 |-  ( ( # ` E ) = ( # ` F ) -> ( ( N o. P ) " ( 1 ..^ ( # ` E ) ) ) = ( ( N o. P ) " ( 1 ..^ ( # ` F ) ) ) )
74 71 73 ineq12d 
 |-  ( ( # ` E ) = ( # ` F ) -> ( ( ( N o. P ) " { 0 , ( # ` E ) } ) i^i ( ( N o. P ) " ( 1 ..^ ( # ` E ) ) ) ) = ( ( ( N o. P ) " { 0 , ( # ` F ) } ) i^i ( ( N o. P ) " ( 1 ..^ ( # ` F ) ) ) ) )
75 74 eqeq1d 
 |-  ( ( # ` E ) = ( # ` F ) -> ( ( ( ( N o. P ) " { 0 , ( # ` E ) } ) i^i ( ( N o. P ) " ( 1 ..^ ( # ` E ) ) ) ) = (/) <-> ( ( ( N o. P ) " { 0 , ( # ` F ) } ) i^i ( ( N o. P ) " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
76 20 75 syl 
 |-  ( ph -> ( ( ( ( N o. P ) " { 0 , ( # ` E ) } ) i^i ( ( N o. P ) " ( 1 ..^ ( # ` E ) ) ) ) = (/) <-> ( ( ( N o. P ) " { 0 , ( # ` F ) } ) i^i ( ( N o. P ) " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
77 69 76 3anbi23d 
 |-  ( ph -> ( ( E ( Trails ` H ) ( N o. P ) /\ Fun `' ( ( N o. P ) |` ( 1 ..^ ( # ` E ) ) ) /\ ( ( ( N o. P ) " { 0 , ( # ` E ) } ) i^i ( ( N o. P ) " ( 1 ..^ ( # ` E ) ) ) ) = (/) ) <-> ( E ( Trails ` H ) ( N o. P ) /\ Fun `' ( ( N o. P ) |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( ( N o. P ) " { 0 , ( # ` F ) } ) i^i ( ( N o. P ) " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) ) )
78 10 11 65 77 mpbir3and 
 |-  ( ph -> ( E ( Trails ` H ) ( N o. P ) /\ Fun `' ( ( N o. P ) |` ( 1 ..^ ( # ` E ) ) ) /\ ( ( ( N o. P ) " { 0 , ( # ` E ) } ) i^i ( ( N o. P ) " ( 1 ..^ ( # ` E ) ) ) ) = (/) ) )
79 ispth 
 |-  ( E ( Paths ` H ) ( N o. P ) <-> ( E ( Trails ` H ) ( N o. P ) /\ Fun `' ( ( N o. P ) |` ( 1 ..^ ( # ` E ) ) ) /\ ( ( ( N o. P ) " { 0 , ( # ` E ) } ) i^i ( ( N o. P ) " ( 1 ..^ ( # ` E ) ) ) ) = (/) ) )
80 78 79 sylibr 
 |-  ( ph -> E ( Paths ` H ) ( N o. P ) )