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

Metamath Proof Explorer

Theorem upgrimcycls

Description: Graph isomorphisms between simple pseudographs map cycles onto cycles. (Contributed by AV, 31-Oct-2025)

Ref Expression
Hypotheses upgrimwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
upgrimwlk.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
upgrimwlk.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
upgrimwlk.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
upgrimwlk.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
upgrimwlk.e ⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
upgrimcycls.c ⊢ ( 𝜑 → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 )
Assertion upgrimcycls ( 𝜑 → 𝐸 ( Cycles ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )

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 upgrimcycls.c ⊢ ( 𝜑 → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 )
8 cyclispth ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
9 7 8 syl ⊢ ( 𝜑 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
10 1 2 3 4 5 6 9 upgrimpths ⊢ ( 𝜑 → 𝐸 ( Paths ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )
11 iscycl ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
12 11 simprbi ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
13 7 12 syl ⊢ ( 𝜑 → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
14 13 fveq2d ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑃 ‘ 0 ) ) = ( 𝑁 ‘ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
15 cycliswlk ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
16 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
17 16 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
18 7 15 17 3syl ⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
19 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
20 7 15 19 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
21 0elfz ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
22 20 21 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
23 18 22 fvco3d ⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) = ( 𝑁 ‘ ( 𝑃 ‘ 0 ) ) )
24 1 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
25 7 15 24 3syl ⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
26 1 2 3 4 5 6 25 upgrimwlklem1 ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )
27 26 fveq2d ⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐸 ) ) = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) )
28 nn0fz0 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
29 20 28 sylib ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
30 18 29 fvco3d ⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑁 ‘ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
31 27 30 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐸 ) ) = ( 𝑁 ‘ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
32 14 23 31 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐸 ) ) )
33 iscycl ⊢ ( 𝐸 ( Cycles ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ↔ ( 𝐸 ( Paths ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ∧ ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐸 ) ) ) )
34 10 32 33 sylanbrc ⊢ ( 𝜑 → 𝐸 ( Cycles ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )