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 ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ₀ )
20	7 15 19	3syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ₀ )
21		0elfz	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ₀ → 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 ... ( ♯ ‘ 𝐹 ) ) )
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 ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )

Metamath Proof Explorer

Theorem upgrimcycls

Proof