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=\mathrm{iEdg}\left(G\right)$$
	upgrimwlk.j	$$⊢J=\mathrm{iEdg}\left(H\right)$$
	upgrimwlk.g	$$⊢\phi \to G\in \mathrm{USHGraph}$$
	upgrimwlk.h	$$⊢\phi \to H\in \mathrm{USHGraph}$$
	upgrimwlk.n	$$⊢\phi \to N\in \left(G\mathrm{GraphIso}H\right)$$
	upgrimwlk.e	$$⊢E=\left(x\in \mathrm{dom}F⟼J^{-1}\left(N\left[I\left(F\left(x\right)\right)\right]\right)\right)$$
	upgrimwlk.w	$$⊢\phi \to F\mathrm{Walks}\left(G\right)P$$
Assertion	upgrimwlklen	$$⊢\phi \to \left(E\mathrm{Walks}\left(H\right)\left(N\circ P\right)\wedge \left|E\right|=\left|F\right|\right)$$

Proof

Step	Hyp	Ref	Expression
1		upgrimwlk.i	$$⊢I=\mathrm{iEdg}\left(G\right)$$
2		upgrimwlk.j	$$⊢J=\mathrm{iEdg}\left(H\right)$$
3		upgrimwlk.g	$$⊢\phi \to G\in \mathrm{USHGraph}$$
4		upgrimwlk.h	$$⊢\phi \to H\in \mathrm{USHGraph}$$
5		upgrimwlk.n	$$⊢\phi \to N\in \left(G\mathrm{GraphIso}H\right)$$
6		upgrimwlk.e	$$⊢E=\left(x\in \mathrm{dom}F⟼J^{-1}\left(N\left[I\left(F\left(x\right)\right)\right]\right)\right)$$
7		upgrimwlk.w	$$⊢\phi \to F\mathrm{Walks}\left(G\right)P$$
8	1 2 3 4 5 6 7	upgrimwlk	$$⊢\phi \to E\mathrm{Walks}\left(H\right)\left(N\circ P\right)$$
9	1	wlkf	$$⊢F\mathrm{Walks}\left(G\right)P\to F\in \mathrm{Word}\mathrm{dom}I$$
10	7 9	syl	$$⊢\phi \to F\in \mathrm{Word}\mathrm{dom}I$$
11	1 2 3 4 5 6 10	upgrimwlklem1	$$⊢\phi \to \left|E\right|=\left|F\right|$$
12	8 11	jca	$$⊢\phi \to \left(E\mathrm{Walks}\left(H\right)\left(N\circ P\right)\wedge \left|E\right|=\left|F\right|\right)$$