This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem upgrimspths

Description: Graph isomorphisms between simple pseudographs map simple paths onto simple paths. (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 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
upgrimspths.s ⊢ ( 𝜑 → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 )
Assertion upgrimspths ( 𝜑 → 𝐸 ( SPaths ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )

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 upgrimspths.s ⊢ ( 𝜑 → 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 )
8 spthispth ⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
9 pthistrl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
10 7 8 9 3syl ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
11 1 2 3 4 5 6 10 upgrimtrls ⊢ ( 𝜑 → 𝐸 ( Trails ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )
12 isspth ⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) )
13 12 simprbi ⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → Fun ◡ 𝑃 )
14 7 13 syl ⊢ ( 𝜑 → Fun ◡ 𝑃 )
15 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
16 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
17 15 16 grimf1o ⊢ ( 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) )
18 dff1o3 ⊢ ( 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ↔ ( 𝑁 : ( Vtx ‘ 𝐺 ) –onto→ ( Vtx ‘ 𝐻 ) ∧ Fun ◡ 𝑁 ) )
19 18 simprbi ⊢ ( 𝑁 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → Fun ◡ 𝑁 )
20 5 17 19 3syl ⊢ ( 𝜑 → Fun ◡ 𝑁 )
21 funco ⊢ ( ( Fun ◡ 𝑃 ∧ Fun ◡ 𝑁 ) → Fun ( ◡ 𝑃 ∘ ◡ 𝑁 ) )
22 14 20 21 syl2anc ⊢ ( 𝜑 → Fun ( ◡ 𝑃 ∘ ◡ 𝑁 ) )
23 cnvco ⊢ ◡ ( 𝑁 ∘ 𝑃 ) = ( ◡ 𝑃 ∘ ◡ 𝑁 )
24 23 funeqi ⊢ ( Fun ◡ ( 𝑁 ∘ 𝑃 ) ↔ Fun ( ◡ 𝑃 ∘ ◡ 𝑁 ) )
25 22 24 sylibr ⊢ ( 𝜑 → Fun ◡ ( 𝑁 ∘ 𝑃 ) )
26 isspth ⊢ ( 𝐸 ( SPaths ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ↔ ( 𝐸 ( Trails ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ∧ Fun ◡ ( 𝑁 ∘ 𝑃 ) ) )
27 11 25 26 sylanbrc ⊢ ( 𝜑 → 𝐸 ( SPaths ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )