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

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 ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
upgrimwlk.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
upgrimwlk.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
upgrimwlk.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
upgrimwlk.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
upgrimwlk.e ⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
upgrimwlk.w ⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
Assertion upgrimwlk ( 𝜑 → 𝐸 ( 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 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
9 7 8 syl ⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
10 1 2 3 4 5 6 9 upgrimwlklem2 ⊢ ( 𝜑 → 𝐸 ∈ Word dom 𝐽 )
11 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
12 11 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
13 7 12 syl ⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
14 1 2 3 4 5 6 9 13 upgrimwlklem4 ⊢ ( 𝜑 → ( 𝑁 ∘ 𝑃 ) : ( 0 ... ( ♯ ‘ 𝐸 ) ) ⟶ ( Vtx ‘ 𝐻 ) )
15 1 2 3 4 5 6 9 upgrimwlklem3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐽 ‘ ( 𝐸 ‘ 𝑖 ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) )
16 1 2 3 4 5 6 7 upgrimwlklem5 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } )
17 15 16 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐽 ‘ ( 𝐸 ‘ 𝑖 ) ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } )
18 17 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ( 𝐽 ‘ ( 𝐸 ‘ 𝑖 ) ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } )
19 uspgrupgr ⊢ ( 𝐻 ∈ USPGraph → 𝐻 ∈ UPGraph )
20 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
21 20 2 upgriswlk ⊢ ( 𝐻 ∈ UPGraph → ( 𝐸 ( Walks ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ↔ ( 𝐸 ∈ Word dom 𝐽 ∧ ( 𝑁 ∘ 𝑃 ) : ( 0 ... ( ♯ ‘ 𝐸 ) ) ⟶ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ( 𝐽 ‘ ( 𝐸 ‘ 𝑖 ) ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } ) ) )
22 4 19 21 3syl ⊢ ( 𝜑 → ( 𝐸 ( Walks ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ↔ ( 𝐸 ∈ Word dom 𝐽 ∧ ( 𝑁 ∘ 𝑃 ) : ( 0 ... ( ♯ ‘ 𝐸 ) ) ⟶ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ( 𝐽 ‘ ( 𝐸 ‘ 𝑖 ) ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑖 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( 𝑖 + 1 ) ) } ) ) )
23 10 14 18 22 mpbir3and ⊢ ( 𝜑 → 𝐸 ( Walks ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )