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 ⊢ I = iEdg ⁡ G
upgrimwlk.j ⊢ J = iEdg ⁡ H
upgrimwlk.g ⊢ φ → G ∈ USHGraph
upgrimwlk.h ⊢ φ → H ∈ USHGraph
upgrimwlk.n ⊢ φ → N ∈ G GraphIso H
upgrimwlk.e ⊢ E = x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x
upgrimcycls.c ⊢ φ → F Cycles ⁡ G P
Assertion upgrimcycls ⊢ φ → E Cycles ⁡ H N ∘ P

Proof

Step Hyp Ref Expression
1 upgrimwlk.i ⊢ I = iEdg ⁡ G
2 upgrimwlk.j ⊢ J = iEdg ⁡ H
3 upgrimwlk.g ⊢ φ → G ∈ USHGraph
4 upgrimwlk.h ⊢ φ → H ∈ USHGraph
5 upgrimwlk.n ⊢ φ → N ∈ G GraphIso H
6 upgrimwlk.e ⊢ E = x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x
7 upgrimcycls.c ⊢ φ → F Cycles ⁡ G P
8 cyclispth ⊢ F Cycles ⁡ G P → F Paths ⁡ G P
9 7 8 syl ⊢ φ → F Paths ⁡ G P
10 1 2 3 4 5 6 9 upgrimpths ⊢ φ → E Paths ⁡ H N ∘ P
11 iscycl ⊢ F Cycles ⁡ G P ↔ F Paths ⁡ G P ∧ P ⁡ 0 = P ⁡ F
12 11 simprbi ⊢ F Cycles ⁡ G P → P ⁡ 0 = P ⁡ F
13 7 12 syl ⊢ φ → P ⁡ 0 = P ⁡ F
14 13 fveq2d ⊢ φ → N ⁡ P ⁡ 0 = N ⁡ P ⁡ F
15 cycliswlk ⊢ F Cycles ⁡ G P → F Walks ⁡ G P
16 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
17 16 wlkp ⊢ F Walks ⁡ G P → P : 0 … F ⟶ Vtx ⁡ G
18 7 15 17 3syl ⊢ φ → P : 0 … F ⟶ Vtx ⁡ G
19 wlkcl ⊢ F Walks ⁡ G P → F ∈ ℕ 0
20 7 15 19 3syl ⊢ φ → F ∈ ℕ 0
21 0elfz ⊢ F ∈ ℕ 0 → 0 ∈ 0 … F
22 20 21 syl ⊢ φ → 0 ∈ 0 … F
23 18 22 fvco3d ⊢ φ → N ∘ P ⁡ 0 = N ⁡ P ⁡ 0
24 1 wlkf ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I
25 7 15 24 3syl ⊢ φ → F ∈ Word dom ⁡ I
26 1 2 3 4 5 6 25 upgrimwlklem1 ⊢ φ → E = F
27 26 fveq2d ⊢ φ → N ∘ P ⁡ E = N ∘ P ⁡ F
28 nn0fz0 ⊢ F ∈ ℕ 0 ↔ F ∈ 0 … F
29 20 28 sylib ⊢ φ → F ∈ 0 … F
30 18 29 fvco3d ⊢ φ → N ∘ P ⁡ F = N ⁡ P ⁡ F
31 27 30 eqtrd ⊢ φ → N ∘ P ⁡ E = N ⁡ P ⁡ F
32 14 23 31 3eqtr4d ⊢ φ → N ∘ P ⁡ 0 = N ∘ P ⁡ E
33 iscycl ⊢ E Cycles ⁡ H N ∘ P ↔ E Paths ⁡ H N ∘ P ∧ N ∘ P ⁡ 0 = N ∘ P ⁡ E
34 10 32 33 sylanbrc ⊢ φ → E Cycles ⁡ H N ∘ P