Theorem upgrimwlklem1

Description: Lemma 1 for upgrimwlk and upgrimwlklen . (Contributed by AV, 25-Oct-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.f	|- ( ph -> F e. Word dom I )
Assertion	upgrimwlklem1	|- ( ph -> ( # ` 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.f	|- ( ph -> F e. Word dom I )
8		fvexd	|- ( ( ph /\ x e. dom F ) -> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) e. _V )
9	8	ralrimiva	|- ( ph -> A. x e. dom F ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) e. _V )
10		eqid	|- ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) ) = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) )
11	10	fnmpt	|- ( A. x e. dom F ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) e. _V -> ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) ) Fn dom F )
12	9 11	syl	|- ( ph -> ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) ) Fn dom F )
13	6	fneq1i	|- ( E Fn dom F <-> ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) ) Fn dom F )
14	12 13	sylibr	|- ( ph -> E Fn dom F )
15		hashfn	|- ( E Fn dom F -> ( # ` E ) = ( # ` dom F ) )
16	14 15	syl	|- ( ph -> ( # ` E ) = ( # ` dom F ) )
17		wrdf	|- ( F e. Word dom I -> F : ( 0 ..^ ( # ` F ) ) --> dom I )
18		ffun	|- ( F : ( 0 ..^ ( # ` F ) ) --> dom I -> Fun F )
19	7 17 18	3syl	|- ( ph -> Fun F )
20	19	funfnd	|- ( ph -> F Fn dom F )
21		hashfn	|- ( F Fn dom F -> ( # ` F ) = ( # ` dom F ) )
22	20 21	syl	|- ( ph -> ( # ` F ) = ( # ` dom F ) )
23	16 22	eqtr4d	|- ( ph -> ( # ` E ) = ( # ` F ) )