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

Metamath Proof Explorer

Theorem upgrimwlklen

Description: Graph isomorphisms between simple pseudographs map walks onto walks of the same length. (Contributed by AV, 6-Nov-2025)

Ref Expression
Hypotheses upgrimwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
upgrimwlk.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
upgrimwlk.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
upgrimwlk.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
upgrimwlk.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
upgrimwlk.e ⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
upgrimwlk.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
Assertion upgrimwlklen ( 𝜑 → ( 𝐸 ( Walks ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ∧ ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) ) )

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 upgrimwlk.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
8 1 2 3 4 5 6 7 upgrimwlk ⊢ ( 𝜑 → 𝐸 ( Walks ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )
9 1 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
10 7 9 syl ⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
11 1 2 3 4 5 6 10 upgrimwlklem1 ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )
12 8 11 jca ⊢ ( 𝜑 → ( 𝐸 ( Walks ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ∧ ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) ) )