gpgprismgr4cycllem11

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

	Ref	Expression
Hypotheses	gpgprismgr4cycl.p	$⊢ P = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩$
	gpgprismgr4cycl.f	$⊢ F = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩$
	gpgprismgr4cycl.g	No typesetting found for \|- G = ( N gPetersenGr 1 ) with typecode \|-
Assertion	gpgprismgr4cycllem11	$⊢ N \in ℤ_{\geq 3} \to F Cycles (G) P$

Proof

Step	Hyp	Ref	Expression
1		gpgprismgr4cycl.p	$⊢ P = ⟨“ ⟨0, 0⟩ ⟨0, 1⟩ ⟨1, 1⟩ ⟨1, 0⟩ ⟨0, 0⟩ ”⟩$
2		gpgprismgr4cycl.f	$⊢ F = ⟨“ \{⟨0, 0⟩, ⟨0, 1⟩\} \{⟨0, 1⟩, ⟨1, 1⟩\} \{⟨1, 1⟩, ⟨1, 0⟩\} \{⟨1, 0⟩, ⟨0, 0⟩\} ”⟩$
3		gpgprismgr4cycl.g	Could not format G = ( N gPetersenGr 1 ) : No typesetting found for \|- G = ( N gPetersenGr 1 ) with typecode \|-
4	1	gpgprismgr4cycllem5	$⊢ P \in Word V$
5	4	a1i	$⊢ N \in ℤ_{\geq 3} \to P \in Word V$
6	1	gpgprismgr4cycllem4	$⊢ \|P\| = 5$
7	6	oveq1i	$⊢ \|P\| - 1 = 5 - 1$
8		5m1e4	$⊢ 5 - 1 = 4$
9	7 8	eqtri	$⊢ \|P\| - 1 = 4$
10	9	eqcomi	$⊢ 4 = \|P\| - 1$
11	1	gpgprismgr4cycllem7	$⊢ (x \in (0 ..^\|P\|) \land y \in (1 ..^4)) \to (x \neq y \to P (x) \neq P (y))$
12	11	adantl	$⊢ (N \in ℤ_{\geq 3} \land (x \in (0 ..^\|P\|) \land y \in (1 ..^4))) \to (x \neq y \to P (x) \neq P (y))$
13	12	ralrimivva	$⊢ N \in ℤ_{\geq 3} \to \forall x \in (0 ..^\|P\|) \forall y \in (1 ..^4) (x \neq y \to P (x) \neq P (y))$
14	2	gpgprismgr4cycllem1	$⊢ \|F\| = 4$
15	1 2 3	gpgprismgr4cycllem8	$⊢ N \in ℤ_{\geq 3} \to F \in Word dom iEdg (G)$
16	1 2 3	gpgprismgr4cycllem9	$⊢ N \in ℤ_{\geq 3} \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
17	1 2 3	gpgprismgr4cycllem10	$⊢ (N \in ℤ_{\geq 3} \land x \in (0 ..^\|F\|)) \to iEdg (G) (F (x)) = \{P (x), P (x + 1)\}$
18	17	ralrimiva	$⊢ N \in ℤ_{\geq 3} \to \forall x \in (0 ..^\|F\|) iEdg (G) (F (x)) = \{P (x), P (x + 1)\}$
19		gpgprismgrusgra	Could not format ( N e. ( ZZ>= ` 3 ) -> ( N gPetersenGr 1 ) e. USGraph ) : No typesetting found for \|- ( N e. ( ZZ>= ` 3 ) -> ( N gPetersenGr 1 ) e. USGraph ) with typecode \|-
20	3	eleq1i	Could not format ( G e. USGraph <-> ( N gPetersenGr 1 ) e. USGraph ) : No typesetting found for \|- ( G e. USGraph <-> ( N gPetersenGr 1 ) e. USGraph ) with typecode \|-
21		usgrupgr	$⊢ G \in USGraph \to G \in UPGraph$
22	20 21	sylbir	Could not format ( ( N gPetersenGr 1 ) e. USGraph -> G e. UPGraph ) : No typesetting found for \|- ( ( N gPetersenGr 1 ) e. USGraph -> G e. UPGraph ) with typecode \|-
23		eqid	$⊢ Vtx (G) = Vtx (G)$
24		eqid	$⊢ iEdg (G) = iEdg (G)$
25	23 24	upgriswlk	$⊢ G \in UPGraph \to (F Walks (G) P \leftrightarrow (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall x \in (0 ..^\|F\|) iEdg (G) (F (x)) = \{P (x), P (x + 1)\}))$
26	19 22 25	3syl	$⊢ N \in ℤ_{\geq 3} \to (F Walks (G) P \leftrightarrow (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall x \in (0 ..^\|F\|) iEdg (G) (F (x)) = \{P (x), P (x + 1)\}))$
27	15 16 18 26	mpbir3and	$⊢ N \in ℤ_{\geq 3} \to F Walks (G) P$
28	2	gpgprismgr4cycllem2	$⊢ Fun F^{-1}$
29		istrl	$⊢ F Trails (G) P \leftrightarrow (F Walks (G) P \land Fun F^{-1})$
30	27 28 29	sylanblrc	$⊢ N \in ℤ_{\geq 3} \to F Trails (G) P$
31	5 10 13 14 30	pthd	$⊢ N \in ℤ_{\geq 3} \to F Paths (G) P$
32	1	gpgprismgr4cycllem6	$⊢ P (0) = P (4)$
33	14	eqcomi	$⊢ 4 = \|F\|$
34	33	fveq2i	$⊢ P (4) = P (\|F\|)$
35	32 34	eqtri	$⊢ P (0) = P (\|F\|)$
36		iscycl	$⊢ F Cycles (G) P \leftrightarrow (F Paths (G) P \land P (0) = P (\|F\|))$
37	31 35 36	sylanblrc	$⊢ N \in ℤ_{\geq 3} \to F Cycles (G) P$

Metamath Proof Explorer

Theorem gpgprismgr4cycllem11

Proof