Theorem upgrimwlklem3

Description: Lemma 3 for upgrimwlk . (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	upgrimwlklem3	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐽 ‘ ( 𝐸 ‘ 𝑋 ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )

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	6	a1i	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
9		2fveq3	⊢ ( 𝑥 = 𝑋 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) )
10	9	imaeq2d	⊢ ( 𝑥 = 𝑋 → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
11	10	fveq2d	⊢ ( 𝑥 = 𝑋 → ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )
12	11	adantl	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) ∧ 𝑥 = 𝑋 ) → ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )
13	1 2 3 4 5 6 7	upgrimwlklem1	⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )
14	13	oveq2d	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
15		wrdf	⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
16		fdm	⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
17	16	eqcomd	⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
18	15 17	syl	⊢ ( 𝐹 ∈ Word dom 𝐼 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
19	7 18	syl	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = dom 𝐹 )
20	14 19	eqtrd	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) = dom 𝐹 )
21	20	eleq2d	⊢ ( 𝜑 → ( 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ↔ 𝑋 ∈ dom 𝐹 ) )
22	21	biimpa	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → 𝑋 ∈ dom 𝐹 )
23		fvexd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) ∈ V )
24	8 12 22 23	fvmptd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐸 ‘ 𝑋 ) = ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) )
25	24	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐽 ‘ ( 𝐸 ‘ 𝑋 ) ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) ) )
26	4	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → 𝐻 ∈ USPGraph )
27	2	uspgrf1oedg	⊢ ( 𝐻 ∈ USPGraph → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
28	26 27	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
29		uspgruhgr	⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph )
30	3 29	syl	⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
31		uspgruhgr	⊢ ( 𝐻 ∈ USPGraph → 𝐻 ∈ UHGraph )
32	4 31	syl	⊢ ( 𝜑 → 𝐻 ∈ UHGraph )
33	30 32	jca	⊢ ( 𝜑 → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) )
35	5	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
36	1	uhgrfun	⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
37	30 36	syl	⊢ ( 𝜑 → Fun 𝐼 )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → Fun 𝐼 )
39	13 7	wrdfd	⊢ ( 𝜑 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ dom 𝐼 )
40	39	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ dom 𝐼 )
41	1	iedgedg	⊢ ( ( Fun 𝐼 ∧ ( 𝐹 ‘ 𝑋 ) ∈ dom 𝐼 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ( Edg ‘ 𝐺 ) )
42	38 40 41	syl2anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ( Edg ‘ 𝐺 ) )
43		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
44		eqid	⊢ ( Edg ‘ 𝐻 ) = ( Edg ‘ 𝐻 )
45	43 44	uhgrimedgi	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ ( Edg ‘ 𝐻 ) )
46	34 35 42 45	syl12anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ ( Edg ‘ 𝐻 ) )
47		f1ocnvfv2	⊢ ( ( 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ ( Edg ‘ 𝐻 ) ) → ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
48	28 46 47	syl2anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
49	25 48	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ) → ( 𝐽 ‘ ( 𝐸 ‘ 𝑋 ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) )