Metamath Proof Explorer

Theorem upgrimwlk

Description: Graph isomorphisms between simple pseudographs map walks onto walks. (Contributed by AV, 28-Oct-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 upgrimwlk ⊢ φ → E Walks ⁡ H N ∘ P

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 wlkf ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I
9 7 8 syl ⊢ φ → F ∈ Word dom ⁡ I
10 1 2 3 4 5 6 9 upgrimwlklem2 ⊢ φ → E ∈ Word dom ⁡ J
11 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
12 11 wlkp ⊢ F Walks ⁡ G P → P : 0 … F ⟶ Vtx ⁡ G
13 7 12 syl ⊢ φ → P : 0 … F ⟶ Vtx ⁡ G
14 1 2 3 4 5 6 9 13 upgrimwlklem4 ⊢ φ → N ∘ P : 0 … E ⟶ Vtx ⁡ H
15 1 2 3 4 5 6 9 upgrimwlklem3 ⊢ φ ∧ i ∈ 0 ..^ E → J ⁡ E ⁡ i = N I ⁡ F ⁡ i
16 1 2 3 4 5 6 7 upgrimwlklem5 ⊢ φ ∧ i ∈ 0 ..^ E → N I ⁡ F ⁡ i = N ∘ P ⁡ i N ∘ P ⁡ i + 1
17 15 16 eqtrd ⊢ φ ∧ i ∈ 0 ..^ E → J ⁡ E ⁡ i = N ∘ P ⁡ i N ∘ P ⁡ i + 1
18 17 ralrimiva ⊢ φ → ∀ i ∈ 0 ..^ E J ⁡ E ⁡ i = N ∘ P ⁡ i N ∘ P ⁡ i + 1
19 uspgrupgr ⊢ H ∈ USHGraph → H ∈ UPGraph
20 eqid ⊢ Vtx ⁡ H = Vtx ⁡ H
21 20 2 upgriswlk ⊢ H ∈ UPGraph → E Walks ⁡ H N ∘ P ↔ E ∈ Word dom ⁡ J ∧ N ∘ P : 0 … E ⟶ Vtx ⁡ H ∧ ∀ i ∈ 0 ..^ E J ⁡ E ⁡ i = N ∘ P ⁡ i N ∘ P ⁡ i + 1
22 4 19 21 3syl ⊢ φ → E Walks ⁡ H N ∘ P ↔ E ∈ Word dom ⁡ J ∧ N ∘ P : 0 … E ⟶ Vtx ⁡ H ∧ ∀ i ∈ 0 ..^ E J ⁡ E ⁡ i = N ∘ P ⁡ i N ∘ P ⁡ i + 1
23 10 14 18 22 mpbir3and ⊢ φ → E Walks ⁡ H N ∘ P