Metamath Proof Explorer

Theorem upgrimpthslem2

Description: Lemma 2 for upgrimpths . (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 upgrimpthslem2 
|- ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( -. ( ( N o. P ) ` X ) = ( ( N o. P ) ` 0 ) /\ -. ( ( N o. P ) ` X ) = ( ( N o. P ) ` ( # ` F ) ) ) )

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 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
9 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
10 8 9 grimf1o 
 |-  ( N e. ( G GraphIso H ) -> N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) )
11 f1of1 
 |-  ( N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> N : ( Vtx ` G ) -1-1-> ( Vtx ` H ) )
12 5 10 11 3syl 
 |-  ( ph -> N : ( Vtx ` G ) -1-1-> ( Vtx ` H ) )
13 12 adantr 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> N : ( Vtx ` G ) -1-1-> ( Vtx ` H ) )
14 pthiswlk 
 |-  ( F ( Paths ` G ) P -> F ( Walks ` G ) P )
15 8 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
16 15 adantr 
 |-  ( ( F ( Walks ` G ) P /\ X e. ( 1 ..^ ( # ` F ) ) ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
17 fzo0ss1 
 |-  ( 1 ..^ ( # ` F ) ) C_ ( 0 ..^ ( # ` F ) )
18 fzossfz 
 |-  ( 0 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
19 17 18 sstri 
 |-  ( 1 ..^ ( # ` F ) ) C_ ( 0 ... ( # ` F ) )
20 19 sseli 
 |-  ( X e. ( 1 ..^ ( # ` F ) ) -> X e. ( 0 ... ( # ` F ) ) )
21 20 adantl 
 |-  ( ( F ( Walks ` G ) P /\ X e. ( 1 ..^ ( # ` F ) ) ) -> X e. ( 0 ... ( # ` F ) ) )
22 16 21 ffvelcdmd 
 |-  ( ( F ( Walks ` G ) P /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( P ` X ) e. ( Vtx ` G ) )
23 22 ex 
 |-  ( F ( Walks ` G ) P -> ( X e. ( 1 ..^ ( # ` F ) ) -> ( P ` X ) e. ( Vtx ` G ) ) )
24 7 14 23 3syl 
 |-  ( ph -> ( X e. ( 1 ..^ ( # ` F ) ) -> ( P ` X ) e. ( Vtx ` G ) ) )
25 24 imp 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( P ` X ) e. ( Vtx ` G ) )
26 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
27 0elfz 
 |-  ( ( # ` F ) e. NN0 -> 0 e. ( 0 ... ( # ` F ) ) )
28 26 27 syl 
 |-  ( F ( Walks ` G ) P -> 0 e. ( 0 ... ( # ` F ) ) )
29 15 28 ffvelcdmd 
 |-  ( F ( Walks ` G ) P -> ( P ` 0 ) e. ( Vtx ` G ) )
30 7 14 29 3syl 
 |-  ( ph -> ( P ` 0 ) e. ( Vtx ` G ) )
31 30 adantr 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( P ` 0 ) e. ( Vtx ` G ) )
32 7 adantr 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> F ( Paths ` G ) P )
33 simpr 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> X e. ( 1 ..^ ( # ` F ) ) )
34 7 14 26 3syl 
 |-  ( ph -> ( # ` F ) e. NN0 )
35 34 27 syl 
 |-  ( ph -> 0 e. ( 0 ... ( # ` F ) ) )
36 35 adantr 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> 0 e. ( 0 ... ( # ` F ) ) )
37 elfzole1 
 |-  ( X e. ( 1 ..^ ( # ` F ) ) -> 1 <_ X )
38 elfzoelz 
 |-  ( X e. ( 1 ..^ ( # ` F ) ) -> X e. ZZ )
39 zgt0ge1 
 |-  ( X e. ZZ -> ( 0 < X <-> 1 <_ X ) )
40 38 39 syl 
 |-  ( X e. ( 1 ..^ ( # ` F ) ) -> ( 0 < X <-> 1 <_ X ) )
41 simpr 
 |-  ( ( X e. ( 1 ..^ ( # ` F ) ) /\ 0 < X ) -> 0 < X )
42 41 gt0ne0d 
 |-  ( ( X e. ( 1 ..^ ( # ` F ) ) /\ 0 < X ) -> X =/= 0 )
43 42 ex 
 |-  ( X e. ( 1 ..^ ( # ` F ) ) -> ( 0 < X -> X =/= 0 ) )
44 40 43 sylbird 
 |-  ( X e. ( 1 ..^ ( # ` F ) ) -> ( 1 <_ X -> X =/= 0 ) )
45 37 44 mpd 
 |-  ( X e. ( 1 ..^ ( # ` F ) ) -> X =/= 0 )
46 45 adantl 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> X =/= 0 )
47 pthdivtx 
 |-  ( ( F ( Paths ` G ) P /\ ( X e. ( 1 ..^ ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) /\ X =/= 0 ) ) -> ( P ` X ) =/= ( P ` 0 ) )
48 32 33 36 46 47 syl13anc 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( P ` X ) =/= ( P ` 0 ) )
49 dff14i 
 |-  ( ( N : ( Vtx ` G ) -1-1-> ( Vtx ` H ) /\ ( ( P ` X ) e. ( Vtx ` G ) /\ ( P ` 0 ) e. ( Vtx ` G ) /\ ( P ` X ) =/= ( P ` 0 ) ) ) -> ( N ` ( P ` X ) ) =/= ( N ` ( P ` 0 ) ) )
50 13 25 31 48 49 syl13anc 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( N ` ( P ` X ) ) =/= ( N ` ( P ` 0 ) ) )
51 nn0fz0 
 |-  ( ( # ` F ) e. NN0 <-> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
52 26 51 sylib 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
53 15 52 ffvelcdmd 
 |-  ( F ( Walks ` G ) P -> ( P ` ( # ` F ) ) e. ( Vtx ` G ) )
54 7 14 53 3syl 
 |-  ( ph -> ( P ` ( # ` F ) ) e. ( Vtx ` G ) )
55 54 adantr 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( P ` ( # ` F ) ) e. ( Vtx ` G ) )
56 34 51 sylib 
 |-  ( ph -> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
57 56 adantr 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
58 38 zred 
 |-  ( X e. ( 1 ..^ ( # ` F ) ) -> X e. RR )
59 elfzolt2 
 |-  ( X e. ( 1 ..^ ( # ` F ) ) -> X < ( # ` F ) )
60 58 59 ltned 
 |-  ( X e. ( 1 ..^ ( # ` F ) ) -> X =/= ( # ` F ) )
61 60 adantl 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> X =/= ( # ` F ) )
62 pthdivtx 
 |-  ( ( F ( Paths ` G ) P /\ ( X e. ( 1 ..^ ( # ` F ) ) /\ ( # ` F ) e. ( 0 ... ( # ` F ) ) /\ X =/= ( # ` F ) ) ) -> ( P ` X ) =/= ( P ` ( # ` F ) ) )
63 32 33 57 61 62 syl13anc 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( P ` X ) =/= ( P ` ( # ` F ) ) )
64 dff14i 
 |-  ( ( N : ( Vtx ` G ) -1-1-> ( Vtx ` H ) /\ ( ( P ` X ) e. ( Vtx ` G ) /\ ( P ` ( # ` F ) ) e. ( Vtx ` G ) /\ ( P ` X ) =/= ( P ` ( # ` F ) ) ) ) -> ( N ` ( P ` X ) ) =/= ( N ` ( P ` ( # ` F ) ) ) )
65 13 25 55 63 64 syl13anc 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( N ` ( P ` X ) ) =/= ( N ` ( P ` ( # ` F ) ) ) )
66 7 14 15 3syl 
 |-  ( ph -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
67 66 adantr 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
68 20 adantl 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> X e. ( 0 ... ( # ` F ) ) )
69 67 68 fvco3d 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( ( N o. P ) ` X ) = ( N ` ( P ` X ) ) )
70 67 36 fvco3d 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( ( N o. P ) ` 0 ) = ( N ` ( P ` 0 ) ) )
71 69 70 neeq12d 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( ( ( N o. P ) ` X ) =/= ( ( N o. P ) ` 0 ) <-> ( N ` ( P ` X ) ) =/= ( N ` ( P ` 0 ) ) ) )
72 67 57 fvco3d 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( ( N o. P ) ` ( # ` F ) ) = ( N ` ( P ` ( # ` F ) ) ) )
73 69 72 neeq12d 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( ( ( N o. P ) ` X ) =/= ( ( N o. P ) ` ( # ` F ) ) <-> ( N ` ( P ` X ) ) =/= ( N ` ( P ` ( # ` F ) ) ) ) )
74 71 73 anbi12d 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( ( ( ( N o. P ) ` X ) =/= ( ( N o. P ) ` 0 ) /\ ( ( N o. P ) ` X ) =/= ( ( N o. P ) ` ( # ` F ) ) ) <-> ( ( N ` ( P ` X ) ) =/= ( N ` ( P ` 0 ) ) /\ ( N ` ( P ` X ) ) =/= ( N ` ( P ` ( # ` F ) ) ) ) ) )
75 50 65 74 mpbir2and 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( ( ( N o. P ) ` X ) =/= ( ( N o. P ) ` 0 ) /\ ( ( N o. P ) ` X ) =/= ( ( N o. P ) ` ( # ` F ) ) ) )
76 df-ne 
 |-  ( ( ( N o. P ) ` X ) =/= ( ( N o. P ) ` 0 ) <-> -. ( ( N o. P ) ` X ) = ( ( N o. P ) ` 0 ) )
77 df-ne 
 |-  ( ( ( N o. P ) ` X ) =/= ( ( N o. P ) ` ( # ` F ) ) <-> -. ( ( N o. P ) ` X ) = ( ( N o. P ) ` ( # ` F ) ) )
78 76 77 anbi12i 
 |-  ( ( ( ( N o. P ) ` X ) =/= ( ( N o. P ) ` 0 ) /\ ( ( N o. P ) ` X ) =/= ( ( N o. P ) ` ( # ` F ) ) ) <-> ( -. ( ( N o. P ) ` X ) = ( ( N o. P ) ` 0 ) /\ -. ( ( N o. P ) ` X ) = ( ( N o. P ) ` ( # ` F ) ) ) )
79 75 78 sylib 
 |-  ( ( ph /\ X e. ( 1 ..^ ( # ` F ) ) ) -> ( -. ( ( N o. P ) ` X ) = ( ( N o. P ) ` 0 ) /\ -. ( ( N o. P ) ` X ) = ( ( N o. P ) ` ( # ` F ) ) ) )