This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )