Metamath Proof Explorer

Theorem upgrimtrlslem1

Description: Lemma 1 for upgrimtrls . (Contributed by AV, 29-Oct-2025)

Ref Expression
Hypotheses upgrimwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
upgrimwlk.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
upgrimwlk.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
upgrimwlk.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
upgrimwlk.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
upgrimwlk.e ⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
upgrimtrls.t ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
Assertion upgrimtrlslem1 ( ( 𝜑 ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ ( Edg ‘ 𝐻 ) )

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 upgrimtrls.t ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
8 uspgruhgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph )
9 3 8 syl ⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
10 uspgruhgr ⊢ ( 𝐻 ∈ USPGraph → 𝐻 ∈ UHGraph )
11 4 10 syl ⊢ ( 𝜑 → 𝐻 ∈ UHGraph )
12 9 11 jca ⊢ ( 𝜑 → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) )
14 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ dom 𝐹 ) → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
15 1 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
16 9 15 syl ⊢ ( 𝜑 → Fun 𝐼 )
17 trliswlk ⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
18 1 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
19 wrdf ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⟶ dom 𝐼 )
20 19 ffdmd ⊢ ( 𝐹 ∈ Word dom 𝐼 → 𝐹 : dom 𝐹 ⟶ dom 𝐼 )
21 18 20 syl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 : dom 𝐹 ⟶ dom 𝐼 )
22 7 17 21 3syl ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ dom 𝐼 )
23 22 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑋 ) ∈ dom 𝐼 )
24 1 iedgedg ⊢ ( ( Fun 𝐼 ∧ ( 𝐹 ‘ 𝑋 ) ∈ dom 𝐼 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ( Edg ‘ 𝐺 ) )
25 16 23 24 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ( Edg ‘ 𝐺 ) )
26 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
27 eqid ⊢ ( Edg ‘ 𝐻 ) = ( Edg ‘ 𝐻 )
28 26 27 uhgrimedgi ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ ( Edg ‘ 𝐻 ) )
29 13 14 25 28 syl12anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑋 ) ) ) ∈ ( Edg ‘ 𝐻 ) )