Metamath Proof Explorer

Theorem upgrimtrlslem2

Description: Lemma 2 for upgrimtrls . (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 upgrimtrlslem2 
|- ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` y ) ) ) ) -> x = y ) )

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 2 uspgrf1oedg 
 |-  ( H e. USPGraph -> J : dom J -1-1-onto-> ( Edg ` H ) )
9 f1of1 
 |-  ( J : dom J -1-1-onto-> ( Edg ` H ) -> J : dom J -1-1-> ( Edg ` H ) )
10 4 8 9 3syl 
 |-  ( ph -> J : dom J -1-1-> ( Edg ` H ) )
11 1 2 3 4 5 6 7 upgrimtrlslem1 
 |-  ( ( ph /\ x e. dom F ) -> ( N " ( I ` ( F ` x ) ) ) e. ( Edg ` H ) )
12 edgval 
 |-  ( Edg ` H ) = ran ( iEdg ` H )
13 2 eqcomi 
 |-  ( iEdg ` H ) = J
14 13 rneqi 
 |-  ran ( iEdg ` H ) = ran J
15 12 14 eqtri 
 |-  ( Edg ` H ) = ran J
16 11 15 eleqtrdi 
 |-  ( ( ph /\ x e. dom F ) -> ( N " ( I ` ( F ` x ) ) ) e. ran J )
17 1 2 3 4 5 6 7 upgrimtrlslem1 
 |-  ( ( ph /\ y e. dom F ) -> ( N " ( I ` ( F ` y ) ) ) e. ( Edg ` H ) )
18 17 15 eleqtrdi 
 |-  ( ( ph /\ y e. dom F ) -> ( N " ( I ` ( F ` y ) ) ) e. ran J )
19 16 18 anim12dan 
 |-  ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( N " ( I ` ( F ` x ) ) ) e. ran J /\ ( N " ( I ` ( F ` y ) ) ) e. ran J ) )
20 f1ocnvfvrneq 
 |-  ( ( J : dom J -1-1-> ( Edg ` H ) /\ ( ( N " ( I ` ( F ` x ) ) ) e. ran J /\ ( N " ( I ` ( F ` y ) ) ) e. ran J ) ) -> ( ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` y ) ) ) ) -> ( N " ( I ` ( F ` x ) ) ) = ( N " ( I ` ( F ` y ) ) ) ) )
21 10 19 20 syl2an2r 
 |-  ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` y ) ) ) ) -> ( N " ( I ` ( F ` x ) ) ) = ( N " ( I ` ( F ` y ) ) ) ) )
22 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
23 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
24 22 23 grimf1o 
 |-  ( N e. ( G GraphIso H ) -> N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) )
25 f1of1 
 |-  ( N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> N : ( Vtx ` G ) -1-1-> ( Vtx ` H ) )
26 5 24 25 3syl 
 |-  ( ph -> N : ( Vtx ` G ) -1-1-> ( Vtx ` H ) )
27 uspgruhgr 
 |-  ( G e. USPGraph -> G e. UHGraph )
28 3 27 syl 
 |-  ( ph -> G e. UHGraph )
29 trliswlk 
 |-  ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
30 1 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
31 wrdf 
 |-  ( F e. Word dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I )
32 id 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I )
33 32 ffdmd 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> F : dom F --> dom I )
34 30 31 33 3syl 
 |-  ( F ( Walks ` G ) P -> F : dom F --> dom I )
35 7 29 34 3syl 
 |-  ( ph -> F : dom F --> dom I )
36 35 ffvelcdmda 
 |-  ( ( ph /\ x e. dom F ) -> ( F ` x ) e. dom I )
37 22 1 uhgrss 
 |-  ( ( G e. UHGraph /\ ( F ` x ) e. dom I ) -> ( I ` ( F ` x ) ) C_ ( Vtx ` G ) )
38 28 36 37 syl2an2r 
 |-  ( ( ph /\ x e. dom F ) -> ( I ` ( F ` x ) ) C_ ( Vtx ` G ) )
39 35 ffvelcdmda 
 |-  ( ( ph /\ y e. dom F ) -> ( F ` y ) e. dom I )
40 22 1 uhgrss 
 |-  ( ( G e. UHGraph /\ ( F ` y ) e. dom I ) -> ( I ` ( F ` y ) ) C_ ( Vtx ` G ) )
41 28 39 40 syl2an2r 
 |-  ( ( ph /\ y e. dom F ) -> ( I ` ( F ` y ) ) C_ ( Vtx ` G ) )
42 38 41 anim12dan 
 |-  ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( I ` ( F ` x ) ) C_ ( Vtx ` G ) /\ ( I ` ( F ` y ) ) C_ ( Vtx ` G ) ) )
43 f1imaeq 
 |-  ( ( N : ( Vtx ` G ) -1-1-> ( Vtx ` H ) /\ ( ( I ` ( F ` x ) ) C_ ( Vtx ` G ) /\ ( I ` ( F ` y ) ) C_ ( Vtx ` G ) ) ) -> ( ( N " ( I ` ( F ` x ) ) ) = ( N " ( I ` ( F ` y ) ) ) <-> ( I ` ( F ` x ) ) = ( I ` ( F ` y ) ) ) )
44 26 42 43 syl2an2r 
 |-  ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( N " ( I ` ( F ` x ) ) ) = ( N " ( I ` ( F ` y ) ) ) <-> ( I ` ( F ` x ) ) = ( I ` ( F ` y ) ) ) )
45 1 uspgrf1oedg 
 |-  ( G e. USPGraph -> I : dom I -1-1-onto-> ( Edg ` G ) )
46 f1of1 
 |-  ( I : dom I -1-1-onto-> ( Edg ` G ) -> I : dom I -1-1-> ( Edg ` G ) )
47 3 45 46 3syl 
 |-  ( ph -> I : dom I -1-1-> ( Edg ` G ) )
48 1 trlf1 
 |-  ( F ( Trails ` G ) P -> F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I )
49 f1f 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I )
50 fdm 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> dom F = ( 0 ..^ ( # ` F ) ) )
51 50 eqcomd 
 |-  ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> ( 0 ..^ ( # ` F ) ) = dom F )
52 49 51 syl 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> ( 0 ..^ ( # ` F ) ) = dom F )
53 f1eq2 
 |-  ( ( 0 ..^ ( # ` F ) ) = dom F -> ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I <-> F : dom F -1-1-> dom I ) )
54 53 biimpcd 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> ( ( 0 ..^ ( # ` F ) ) = dom F -> F : dom F -1-1-> dom I ) )
55 52 54 mpd 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-> dom I -> F : dom F -1-1-> dom I )
56 7 48 55 3syl 
 |-  ( ph -> F : dom F -1-1-> dom I )
57 47 56 jca 
 |-  ( ph -> ( I : dom I -1-1-> ( Edg ` G ) /\ F : dom F -1-1-> dom I ) )
58 f1cofveqaeq 
 |-  ( ( ( I : dom I -1-1-> ( Edg ` G ) /\ F : dom F -1-1-> dom I ) /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( I ` ( F ` x ) ) = ( I ` ( F ` y ) ) -> x = y ) )
59 57 58 sylan 
 |-  ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( I ` ( F ` x ) ) = ( I ` ( F ` y ) ) -> x = y ) )
60 44 59 sylbid 
 |-  ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( N " ( I ` ( F ` x ) ) ) = ( N " ( I ` ( F ` y ) ) ) -> x = y ) )
61 21 60 syld 
 |-  ( ( ph /\ ( x e. dom F /\ y e. dom F ) ) -> ( ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) = ( `' J ` ( N " ( I ` ( F ` y ) ) ) ) -> x = y ) )