Theorem gpgprismgr4cycllem11

Description: Lemma 11 for gpgprismgr4cycl0 . (Contributed by AV, 5-Nov-2025)

	Ref	Expression
Hypotheses	gpgprismgr4cycl.p	⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩
	gpgprismgr4cycl.f	⊢ 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩
	gpgprismgr4cycl.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 1 )
Assertion	gpgprismgr4cycllem11	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycl.p	⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩
2		gpgprismgr4cycl.f	⊢ 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩
3		gpgprismgr4cycl.g	⊢ 𝐺 = ( 𝑁 gPetersenGr 1 )
4	1	gpgprismgr4cycllem5	⊢ 𝑃 ∈ Word V
5	4	a1i	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑃 ∈ Word V )
6	1	gpgprismgr4cycllem4	⊢ ( ♯ ‘ 𝑃 ) = 5
7	6	oveq1i	⊢ ( ( ♯ ‘ 𝑃 ) − 1 ) = ( 5 − 1 )
8		5m1e4	⊢ ( 5 − 1 ) = 4
9	7 8	eqtri	⊢ ( ( ♯ ‘ 𝑃 ) − 1 ) = 4
10	9	eqcomi	⊢ 4 = ( ( ♯ ‘ 𝑃 ) − 1 )
11	1	gpgprismgr4cycllem7	⊢ ( ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( 1 ..^ 4 ) ) → ( 𝑥 ≠ 𝑦 → ( 𝑃 ‘ 𝑥 ) ≠ ( 𝑃 ‘ 𝑦 ) ) )
12	11	adantl	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∧ 𝑦 ∈ ( 1 ..^ 4 ) ) ) → ( 𝑥 ≠ 𝑦 → ( 𝑃 ‘ 𝑥 ) ≠ ( 𝑃 ‘ 𝑦 ) ) )
13	12	ralrimivva	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ∀ 𝑦 ∈ ( 1 ..^ 4 ) ( 𝑥 ≠ 𝑦 → ( 𝑃 ‘ 𝑥 ) ≠ ( 𝑃 ‘ 𝑦 ) ) )
14	2	gpgprismgr4cycllem1	⊢ ( ♯ ‘ 𝐹 ) = 4
15	1 2 3	gpgprismgr4cycllem8	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )
16	1 2 3	gpgprismgr4cycllem9	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
17	1 2 3	gpgprismgr4cycllem10	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } )
18	17	ralrimiva	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } )
19		gpgprismgrusgra	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 gPetersenGr 1 ) ∈ USGraph )
20	3	eleq1i	⊢ ( 𝐺 ∈ USGraph ↔ ( 𝑁 gPetersenGr 1 ) ∈ USGraph )
21		usgrupgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph )
22	20 21	sylbir	⊢ ( ( 𝑁 gPetersenGr 1 ) ∈ USGraph → 𝐺 ∈ UPGraph )
23		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
24		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
25	23 24	upgriswlk	⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) )
26	19 22 25	3syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( ( iEdg ‘ 𝐺 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ) )
27	15 16 18 26	mpbir3and	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
28	2	gpgprismgr4cycllem2	⊢ Fun ◡ 𝐹
29		istrl	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝐹 ) )
30	27 28 29	sylanblrc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
31	5 10 13 14 30	pthd	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
32	1	gpgprismgr4cycllem6	⊢ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 4 )
33	14	eqcomi	⊢ 4 = ( ♯ ‘ 𝐹 )
34	33	fveq2i	⊢ ( 𝑃 ‘ 4 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) )
35	32 34	eqtri	⊢ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) )
36		iscycl	⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
37	31 35 36	sylanblrc	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 )