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	|- ( ph -> G e. USPGraph )
	upgrimwlk.h	|- ( ph -> H e. USPGraph )
	upgrimwlk.n	|- ( ph -> N e. ( G GraphIso H ) )
	upgrimwlk.e	|- E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) )
	upgrimwlk.w	|- ( ph -> F ( Walks ` G ) P )
Assertion	upgrimwlklen	|- ( ph -> ( E ( Walks ` H ) ( N o. P ) /\ ( # ` E ) = ( # ` F ) ) )

Proof

Step	Hyp	Ref	Expression
1		upgrimwlk.i	|- I = ( iEdg ` G )
2		upgrimwlk.j	|- J = ( iEdg ` H )
3		upgrimwlk.g	|- ( ph -> G e. USPGraph )
4		upgrimwlk.h	|- ( ph -> H e. USPGraph )
5		upgrimwlk.n	|- ( ph -> N e. ( G GraphIso H ) )
6		upgrimwlk.e	|- E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) )
7		upgrimwlk.w	|- ( ph -> F ( Walks ` G ) P )
8	1 2 3 4 5 6 7	upgrimwlk	|- ( ph -> E ( Walks ` H ) ( N o. P ) )
9	1	wlkf	|- ( F ( Walks ` G ) P -> F e. Word dom I )
10	7 9	syl	|- ( ph -> F e. Word dom I )
11	1 2 3 4 5 6 10	upgrimwlklem1	|- ( ph -> ( # ` E ) = ( # ` F ) )
12	8 11	jca	|- ( ph -> ( E ( Walks ` H ) ( N o. P ) /\ ( # ` E ) = ( # ` F ) ) )