Metamath Proof Explorer

Theorem upgrimpthslem2

Description: Lemma 2 for upgrimpths . (Contributed by AV, 31-Oct-2025)

Ref Expression
Hypotheses upgrimwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
upgrimwlk.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
upgrimwlk.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
upgrimwlk.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
upgrimwlk.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
upgrimwlk.e ⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
upgrimpths.p ⊢ ( 𝜑 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
Assertion upgrimpthslem2 ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∧ ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 upgrimwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 upgrimwlk.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
3 upgrimwlk.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
4 upgrimwlk.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
5 upgrimwlk.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
6 upgrimwlk.e ⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
7 upgrimpths.p ⊢ ( 𝜑 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
8 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
9 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
10 8 9 grimf1o ⊢ ( 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) )
11 f1of1 ⊢ ( 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝑁 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) )
12 5 10 11 3syl ⊢ ( 𝜑 → 𝑁 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑁 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) )
14 pthiswlk ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
15 8 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
16 15 adantr ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
17 fzo0ss1 ⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
18 fzossfz ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) )
19 17 18 sstri ⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) )
20 19 sseli ⊢ ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑋 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
21 20 adantl ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑋 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
22 16 21 ffvelcdmd ⊢ ( ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐺 ) )
23 22 ex ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑃 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐺 ) ) )
24 7 14 23 3syl ⊢ ( 𝜑 → ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑃 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐺 ) ) )
25 24 imp ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐺 ) )
26 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
27 0elfz ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
28 26 27 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
29 15 28 ffvelcdmd ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
30 7 14 29 3syl ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
32 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
34 7 14 26 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
35 34 27 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
37 elfzole1 ⊢ ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 1 ≤ 𝑋 )
38 elfzoelz ⊢ ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑋 ∈ ℤ )
39 zgt0ge1 ⊢ ( 𝑋 ∈ ℤ → ( 0 < 𝑋 ↔ 1 ≤ 𝑋 ) )
40 38 39 syl ⊢ ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 0 < 𝑋 ↔ 1 ≤ 𝑋 ) )
41 simpr ⊢ ( ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 < 𝑋 ) → 0 < 𝑋 )
42 41 gt0ne0d ⊢ ( ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 < 𝑋 ) → 𝑋 ≠ 0 )
43 42 ex ⊢ ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 0 < 𝑋 → 𝑋 ≠ 0 ) )
44 40 43 sylbird ⊢ ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 1 ≤ 𝑋 → 𝑋 ≠ 0 ) )
45 37 44 mpd ⊢ ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑋 ≠ 0 )
46 45 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑋 ≠ 0 )
47 pthdivtx ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝑋 ≠ 0 ) ) → ( 𝑃 ‘ 𝑋 ) ≠ ( 𝑃 ‘ 0 ) )
48 32 33 36 46 47 syl13anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 𝑋 ) ≠ ( 𝑃 ‘ 0 ) )
49 dff14i ⊢ ( ( 𝑁 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) ∧ ( ( 𝑃 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 𝑋 ) ≠ ( 𝑃 ‘ 0 ) ) ) → ( 𝑁 ‘ ( 𝑃 ‘ 𝑋 ) ) ≠ ( 𝑁 ‘ ( 𝑃 ‘ 0 ) ) )
50 13 25 31 48 49 syl13anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑁 ‘ ( 𝑃 ‘ 𝑋 ) ) ≠ ( 𝑁 ‘ ( 𝑃 ‘ 0 ) ) )
51 nn0fz0 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
52 26 51 sylib ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
53 15 52 ffvelcdmd ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) )
54 7 14 53 3syl ⊢ ( 𝜑 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) )
55 54 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) )
56 34 51 sylib ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
58 38 zred ⊢ ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑋 ∈ ℝ )
59 elfzolt2 ⊢ ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑋 < ( ♯ ‘ 𝐹 ) )
60 58 59 ltned ⊢ ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → 𝑋 ≠ ( ♯ ‘ 𝐹 ) )
61 60 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑋 ≠ ( ♯ ‘ 𝐹 ) )
62 pthdivtx ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ 𝑋 ≠ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 𝑋 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
63 32 33 57 61 62 syl13anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑃 ‘ 𝑋 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
64 dff14i ⊢ ( ( 𝑁 : ( Vtx ‘ 𝐺 ) –1-1→ ( Vtx ‘ 𝐻 ) ∧ ( ( 𝑃 ‘ 𝑋 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ 𝑋 ) ≠ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑁 ‘ ( 𝑃 ‘ 𝑋 ) ) ≠ ( 𝑁 ‘ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
65 13 25 55 63 64 syl13anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑁 ‘ ( 𝑃 ‘ 𝑋 ) ) ≠ ( 𝑁 ‘ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
66 7 14 15 3syl ⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
68 20 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑋 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
69 67 68 fvco3d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) = ( 𝑁 ‘ ( 𝑃 ‘ 𝑋 ) ) )
70 67 36 fvco3d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) = ( 𝑁 ‘ ( 𝑃 ‘ 0 ) ) )
71 69 70 neeq12d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) ≠ ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ↔ ( 𝑁 ‘ ( 𝑃 ‘ 𝑋 ) ) ≠ ( 𝑁 ‘ ( 𝑃 ‘ 0 ) ) ) )
72 67 57 fvco3d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑁 ‘ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
73 69 72 neeq12d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) ≠ ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑁 ‘ ( 𝑃 ‘ 𝑋 ) ) ≠ ( 𝑁 ‘ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
74 71 73 anbi12d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) ≠ ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∧ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) ≠ ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) ↔ ( ( 𝑁 ‘ ( 𝑃 ‘ 𝑋 ) ) ≠ ( 𝑁 ‘ ( 𝑃 ‘ 0 ) ) ∧ ( 𝑁 ‘ ( 𝑃 ‘ 𝑋 ) ) ≠ ( 𝑁 ‘ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) ) )
75 50 65 74 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) ≠ ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∧ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) ≠ ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) )
76 df-ne ⊢ ( ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) ≠ ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ↔ ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) )
77 df-ne ⊢ ( ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) ≠ ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ↔ ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) )
78 76 77 anbi12i ⊢ ( ( ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) ≠ ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∧ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) ≠ ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) ↔ ( ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∧ ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) )
79 75 78 sylib ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∧ ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑋 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) )