Metamath Proof Explorer

Theorem upgrimpthslem1

Description: Lemma 1 for upgrimpths . (Contributed by AV, 30-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 upgrimpthslem1 ( 𝜑 → Fun ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )

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 ispth ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
9 8 simp2bi ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
10 7 9 syl ⊢ ( 𝜑 → Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
11 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
12 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
13 11 12 grimf1o ⊢ ( 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) )
14 dff1o3 ⊢ ( 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ↔ ( 𝑁 : ( Vtx ‘ 𝐺 ) –onto→ ( Vtx ‘ 𝐻 ) ∧ Fun ◡ 𝑁 ) )
15 14 simprbi ⊢ ( 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → Fun ◡ 𝑁 )
16 5 13 15 3syl ⊢ ( 𝜑 → Fun ◡ 𝑁 )
17 funco ⊢ ( ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ Fun ◡ 𝑁 ) → Fun ( ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∘ ◡ 𝑁 ) )
18 10 16 17 syl2anc ⊢ ( 𝜑 → Fun ( ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∘ ◡ 𝑁 ) )
19 resco ⊢ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( 𝑁 ∘ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
20 19 cnveqi ⊢ ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ◡ ( 𝑁 ∘ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
21 cnvco ⊢ ◡ ( 𝑁 ∘ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ( ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∘ ◡ 𝑁 )
22 20 21 eqtri ⊢ ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∘ ◡ 𝑁 )
23 22 funeqi ⊢ ( Fun ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ Fun ( ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∘ ◡ 𝑁 ) )
24 18 23 sylibr ⊢ ( 𝜑 → Fun ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )