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 ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )

Metamath Proof Explorer

Theorem upgrimwlk

Proof