Theorem upgrimwlklem1

Description: Lemma 1 for upgrimwlk and upgrimwlklen . (Contributed by AV, 25-Oct-2025)

	Ref	Expression
Hypotheses	upgrimwlk.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	upgrimwlk.j	⊢ 𝐽 = ( iEdg ‘ 𝐻 )
	upgrimwlk.g	⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
	upgrimwlk.h	⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
	upgrimwlk.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
	upgrimwlk.e	⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
	upgrimwlk.f	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
Assertion	upgrimwlklem1	⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )

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.f	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
8		fvexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ V )
9	8	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ dom 𝐹 ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ V )
10		eqid	⊢ ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
11	10	fnmpt	⊢ ( ∀ 𝑥 ∈ dom 𝐹 ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ V → ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) Fn dom 𝐹 )
12	9 11	syl	⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) Fn dom 𝐹 )
13	6	fneq1i	⊢ ( 𝐸 Fn dom 𝐹 ↔ ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) Fn dom 𝐹 )
14	12 13	sylibr	⊢ ( 𝜑 → 𝐸 Fn dom 𝐹 )
15		hashfn	⊢ ( 𝐸 Fn dom 𝐹 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ dom 𝐹 ) )
16	14 15	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ dom 𝐹 ) )
17		wrdf	⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
18		ffun	⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → Fun 𝐹 )
19	7 17 18	3syl	⊢ ( 𝜑 → Fun 𝐹 )
20	19	funfnd	⊢ ( 𝜑 → 𝐹 Fn dom 𝐹 )
21		hashfn	⊢ ( 𝐹 Fn dom 𝐹 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) )
22	20 21	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) )
23	16 22	eqtr4d	⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )