dlwwlknondlwlknonf1olem1

Description: Lemma 1 for dlwwlknondlwlknonf1o . (Contributed by AV, 29-May-2022) (Revised by AV, 1-Nov-2022)

		Ref	Expression
	Assertion	dlwwlknondlwlknonf1olem1	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ‘ ( 𝑁 − 2 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑁 − 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		clwlkwlk	⊢ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) → 𝑐 ∈ ( Walks ‘ 𝐺 ) )
2		wlkcpr	⊢ ( 𝑐 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) )
3	1 2	sylib	⊢ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) → ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) )
4		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5	4	wlkpwrd	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) )
6	3 5	syl	⊢ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) → ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) )
7	6	3ad2ant2	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) )
8		eluzge2nn0	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 2 ) → 𝑁 ∈ ℕ₀ )
9	8	3ad2ant3	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → 𝑁 ∈ ℕ₀ )
10		eleq1	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ₀ ↔ 𝑁 ∈ ℕ₀ ) )
11	10	3ad2ant1	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ₀ ↔ 𝑁 ∈ ℕ₀ ) )
12	9 11	mpbird	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ₀ )
13		nn0fz0	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ℕ₀ ↔ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
14	12 13	sylib	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
15		fzelp1	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) → ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 0 ... ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) )
16	14 15	syl	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 0 ... ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) )
17		wlklenvp1	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) = ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) )
18	17	eqcomd	⊢ ( ( 1^st ‘ 𝑐 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑐 ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) = ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) )
19	3 18	syl	⊢ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) = ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) )
20	19	oveq2d	⊢ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) → ( 0 ... ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) = ( 0 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) )
21	20	eleq2d	⊢ ( 𝑐 ∈ ( ClWalks ‘ 𝐺 ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 0 ... ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 0 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ) )
22	21	3ad2ant2	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 0 ... ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) + 1 ) ) ↔ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 0 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ) )
23	16 22	mpbid	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 0 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) )
24		2nn	⊢ 2 ∈ ℕ
25	24	a1i	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 2 ) → 2 ∈ ℕ )
26		eluz2nn	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 2 ) → 𝑁 ∈ ℕ )
27		eluzle	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 2 ) → 2 ≤ 𝑁 )
28		elfz1b	⊢ ( 2 ∈ ( 1 ... 𝑁 ) ↔ ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 2 ≤ 𝑁 ) )
29	25 26 27 28	syl3anbrc	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 2 ) → 2 ∈ ( 1 ... 𝑁 ) )
30		ubmelfzo	⊢ ( 2 ∈ ( 1 ... 𝑁 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ 𝑁 ) )
31	29 30	syl	⊢ ( 𝑁 ∈ ( ℤ_≥ ‘ 2 ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ 𝑁 ) )
32	31	3ad2ant3	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ 𝑁 ) )
33		oveq2	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) = ( 0 ..^ 𝑁 ) )
34	33	eleq2d	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 → ( ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ↔ ( 𝑁 − 2 ) ∈ ( 0 ..^ 𝑁 ) ) )
35	34	3ad2ant1	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ↔ ( 𝑁 − 2 ) ∈ ( 0 ..^ 𝑁 ) ) )
36	32 35	mpbird	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) )
37		pfxfv	⊢ ( ( ( 2^nd ‘ 𝑐 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ∈ ( 0 ... ( ♯ ‘ ( 2^nd ‘ 𝑐 ) ) ) ∧ ( 𝑁 − 2 ) ∈ ( 0 ..^ ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ) → ( ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ‘ ( 𝑁 − 2 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑁 − 2 ) ) )
38	7 23 36 37	syl3anc	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) = 𝑁 ∧ 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( ℤ_≥ ‘ 2 ) ) → ( ( ( 2^nd ‘ 𝑐 ) prefix ( ♯ ‘ ( 1^st ‘ 𝑐 ) ) ) ‘ ( 𝑁 − 2 ) ) = ( ( 2^nd ‘ 𝑐 ) ‘ ( 𝑁 − 2 ) ) )

Metamath Proof Explorer

Theorem dlwwlknondlwlknonf1olem1

Proof