upgrimtrls

Description: Graph isomorphisms between simple pseudographs map trails onto trails. (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	upgrimtrls	⊢ ( 𝜑 → 𝐸 ( Trails ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )

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		trliswlk	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
9	7 8	syl	⊢ ( 𝜑 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
10	1 2 3 4 5 6 9	upgrimwlk	⊢ ( 𝜑 → 𝐸 ( Walks ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )
11	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐻 ∈ USPGraph )
12	2	uspgrf1oedg	⊢ ( 𝐻 ∈ USPGraph → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
13	11 12	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
14	1 2 3 4 5 6 7	upgrimtrlslem1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( Edg ‘ 𝐻 ) )
15		f1ocnvdm	⊢ ( ( 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ ( Edg ‘ 𝐻 ) ) → ( ^◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ dom 𝐽 )
16	13 14 15	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( ^◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ dom 𝐽 )
17	16	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ dom 𝐹 ( ^◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ dom 𝐽 )
18	1 2 3 4 5 6 7	upgrimtrlslem2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) ) → ( ( ^◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ^◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝑥 = 𝑦 ) )
19	18	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ dom 𝐹 ( ( ^◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ^◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝑥 = 𝑦 ) )
20		2fveq3	⊢ ( 𝑥 = 𝑦 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) )
21	20	imaeq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
22	21	fveq2d	⊢ ( 𝑥 = 𝑦 → ( ^◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ^◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) )
23	6 22	f1mpt	⊢ ( 𝐸 : dom 𝐹 –1-1→ dom 𝐽 ↔ ( ∀ 𝑥 ∈ dom 𝐹 ( ^◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) ∈ dom 𝐽 ∧ ∀ 𝑥 ∈ dom 𝐹 ∀ 𝑦 ∈ dom 𝐹 ( ( ^◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( ^◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑦 ) ) ) ) → 𝑥 = 𝑦 ) ) )
24	17 19 23	sylanbrc	⊢ ( 𝜑 → 𝐸 : dom 𝐹 –1-1→ dom 𝐽 )
25		eqidd	⊢ ( 𝜑 → 𝐸 = 𝐸 )
26	1	wlkf	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
27	7 8 26	3syl	⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
28	1 2 3 4 5 6 27	upgrimwlklem1	⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )
29	28	oveq2d	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
30		wrddm	⊢ ( 𝐹 ∈ Word dom 𝐼 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
31	8 26 30	3syl	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
32	7 31	syl	⊢ ( 𝜑 → dom 𝐹 = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
33	29 32	eqtr4d	⊢ ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝐸 ) ) = dom 𝐹 )
34		eqidd	⊢ ( 𝜑 → dom 𝐽 = dom 𝐽 )
35	25 33 34	f1eq123d	⊢ ( 𝜑 → ( 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) –1-1→ dom 𝐽 ↔ 𝐸 : dom 𝐹 –1-1→ dom 𝐽 ) )
36	24 35	mpbird	⊢ ( 𝜑 → 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) –1-1→ dom 𝐽 )
37		df-f1	⊢ ( 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) –1-1→ dom 𝐽 ↔ ( 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ dom 𝐽 ∧ Fun ^◡ 𝐸 ) )
38	37	simprbi	⊢ ( 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) –1-1→ dom 𝐽 → Fun ^◡ 𝐸 )
39	36 38	syl	⊢ ( 𝜑 → Fun ^◡ 𝐸 )
40		istrl	⊢ ( 𝐸 ( Trails ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ↔ ( 𝐸 ( Walks ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ∧ Fun ^◡ 𝐸 ) )
41	10 39 40	sylanbrc	⊢ ( 𝜑 → 𝐸 ( Trails ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )

Metamath Proof Explorer

Theorem upgrimtrls

Proof