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 ⊢ I = iEdg ⁡ G
upgrimwlk.j ⊢ J = iEdg ⁡ H
upgrimwlk.g ⊢ φ → G ∈ USHGraph
upgrimwlk.h ⊢ φ → H ∈ USHGraph
upgrimwlk.n ⊢ φ → N ∈ G GraphIso H
upgrimwlk.e ⊢ E = x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x
upgrimwlk.w ⊢ φ → F Walks ⁡ G P
Assertion upgrimwlklen ⊢ φ → E Walks ⁡ H N ∘ P ∧ E = F

Proof

Step Hyp Ref Expression
1 upgrimwlk.i ⊢ I = iEdg ⁡ G
2 upgrimwlk.j ⊢ J = iEdg ⁡ H
3 upgrimwlk.g ⊢ φ → G ∈ USHGraph
4 upgrimwlk.h ⊢ φ → H ∈ USHGraph
5 upgrimwlk.n ⊢ φ → N ∈ G GraphIso H
6 upgrimwlk.e ⊢ E = x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x
7 upgrimwlk.w ⊢ φ → F Walks ⁡ G P
8 1 2 3 4 5 6 7 upgrimwlk ⊢ φ → E Walks ⁡ H N ∘ P
9 1 wlkf ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I
10 7 9 syl ⊢ φ → F ∈ Word dom ⁡ I
11 1 2 3 4 5 6 10 upgrimwlklem1 ⊢ φ → E = F
12 8 11 jca ⊢ φ → E Walks ⁡ H N ∘ P ∧ E = F