clwlknf1oclwwlknlem1

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

		Ref	Expression
	Assertion	clwlknf1oclwwlknlem1	⊢ ( ( 𝐶 ∈ ( ClWalks ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) ) → ( ♯ ‘ ( ( 2^nd ‘ 𝐶 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) ) ) = ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		clwlkwlk	⊢ ( 𝐶 ∈ ( ClWalks ‘ 𝐺 ) → 𝐶 ∈ ( Walks ‘ 𝐺 ) )
2		wlkcpr	⊢ ( 𝐶 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) )
3		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4	3	wlkpwrd	⊢ ( ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) → ( 2^nd ‘ 𝐶 ) ∈ Word ( Vtx ‘ 𝐺 ) )
5		lencl	⊢ ( ( 2^nd ‘ 𝐶 ) ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ∈ ℕ₀ )
6	4 5	syl	⊢ ( ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) → ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ∈ ℕ₀ )
7		wlklenvm1	⊢ ( ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) → ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) )
8	7	breq2d	⊢ ( ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) ↔ 1 ≤ ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) ) )
9		1red	⊢ ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ∈ ℕ₀ → 1 ∈ ℝ )
10		nn0re	⊢ ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ∈ ℕ₀ → ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ∈ ℝ )
11	9 9 10	leaddsub2d	⊢ ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ∈ ℕ₀ → ( ( 1 + 1 ) ≤ ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ↔ 1 ≤ ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) ) )
12		1p1e2	⊢ ( 1 + 1 ) = 2
13	12	breq1i	⊢ ( ( 1 + 1 ) ≤ ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ↔ 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) )
14	13	biimpi	⊢ ( ( 1 + 1 ) ≤ ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) → 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) )
15	11 14	syl6bir	⊢ ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ∈ ℕ₀ → ( 1 ≤ ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) → 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ) )
16	4 5 15	3syl	⊢ ( ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) → ( 1 ≤ ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) → 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ) )
17	8 16	sylbid	⊢ ( ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) → 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ) )
18	17	imp	⊢ ( ( ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) ) → 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) )
19		ige2m1fz	⊢ ( ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ∈ ℕ₀ ∧ 2 ≤ ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ) → ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) ∈ ( 0 ... ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ) )
20	6 18 19	syl2an2r	⊢ ( ( ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) ) → ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) ∈ ( 0 ... ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ) )
21		pfxlen	⊢ ( ( ( 2^nd ‘ 𝐶 ) ∈ Word ( Vtx ‘ 𝐺 ) ∧ ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) ∈ ( 0 ... ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) ) ) → ( ♯ ‘ ( ( 2^nd ‘ 𝐶 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) )
22	4 20 21	syl2an2r	⊢ ( ( ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) ) → ( ♯ ‘ ( ( 2^nd ‘ 𝐶 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) ) ) = ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) )
23	7	eqcomd	⊢ ( ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) → ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) = ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) )
24	23	adantr	⊢ ( ( ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) ) → ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) = ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) )
25	22 24	eqtrd	⊢ ( ( ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) ) → ( ♯ ‘ ( ( 2^nd ‘ 𝐶 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) ) ) = ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) )
26	25	ex	⊢ ( ( 1^st ‘ 𝐶 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝐶 ) → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) → ( ♯ ‘ ( ( 2^nd ‘ 𝐶 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) ) ) = ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) ) )
27	2 26	sylbi	⊢ ( 𝐶 ∈ ( Walks ‘ 𝐺 ) → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) → ( ♯ ‘ ( ( 2^nd ‘ 𝐶 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) ) ) = ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) ) )
28	1 27	syl	⊢ ( 𝐶 ∈ ( ClWalks ‘ 𝐺 ) → ( 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) → ( ♯ ‘ ( ( 2^nd ‘ 𝐶 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) ) ) = ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) ) )
29	28	imp	⊢ ( ( 𝐶 ∈ ( ClWalks ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) ) → ( ♯ ‘ ( ( 2^nd ‘ 𝐶 ) prefix ( ( ♯ ‘ ( 2^nd ‘ 𝐶 ) ) − 1 ) ) ) = ( ♯ ‘ ( 1^st ‘ 𝐶 ) ) )

Metamath Proof Explorer

Theorem clwlknf1oclwwlknlem1

Proof