Theorem clwlkclwwlklem2a2

Description: Lemma 2 for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 21-Jun-2018)

	Ref	Expression
Hypothesis	clwlkclwwlklem2.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
Assertion	clwlkclwwlklem2a2	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )

Proof

Step	Hyp	Ref	Expression
1		clwlkclwwlklem2.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) )
2		lencl	⊢ ( 𝑃 ∈ Word 𝑉 → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
3		nn0z	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℤ )
4	3	adantr	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℤ )
5		0red	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 0 ∈ ℝ )
6		2re	⊢ 2 ∈ ℝ
7	6	a1i	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 2 ∈ ℝ )
8		nn0re	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 → ( ♯ ‘ 𝑃 ) ∈ ℝ )
9	8	adantr	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℝ )
10		2pos	⊢ 0 < 2
11	10	a1i	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 0 < 2 )
12		simpr	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
13	5 7 9 11 12	ltletrd	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 0 < ( ♯ ‘ 𝑃 ) )
14		elnnz	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑃 ) ∈ ℤ ∧ 0 < ( ♯ ‘ 𝑃 ) ) )
15	4 13 14	sylanbrc	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℕ )
16	2 15	sylan	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℕ )
17		nnm1nn0	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ0 )
18	16 17	syl	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ0 )
19		fvex	⊢ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ V
20		fvex	⊢ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ∈ V
21	19 20	ifex	⊢ if ( 𝑥 < ( ( ♯ ‘ 𝑃 ) − 2 ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) , ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ 0 ) } ) ) ∈ V
22	21 1	fnmpti	⊢ 𝐹 Fn ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) )
23		ffzo0hash	⊢ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ0 ∧ 𝐹 Fn ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
24	18 22 23	sylancl	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )