Theorem wlkiswwlks2lem1

Description: Lemma 1 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 20-Jul-2018)

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

Proof

Step	Hyp	Ref	Expression
1		wlkiswwlks2lem.f	⊢ 𝐹 = ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ↦ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) )
2		lencl	⊢ ( 𝑃 ∈ Word 𝑉 → ( ♯ ‘ 𝑃 ) ∈ ℕ0 )
3		elnnnn0c	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) )
4	3	biimpri	⊢ ( ( ( ♯ ‘ 𝑃 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℕ )
5	2 4	sylan	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝑃 ) ∈ ℕ )
6		nnm1nn0	⊢ ( ( ♯ ‘ 𝑃 ) ∈ ℕ → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ0 )
7	5 6	syl	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ0 )
8		fvex	⊢ ( ◡ 𝐸 ‘ { ( 𝑃 ‘ 𝑥 ) , ( 𝑃 ‘ ( 𝑥 + 1 ) ) } ) ∈ V
9	8 1	fnmpti	⊢ 𝐹 Fn ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) )
10		ffzo0hash	⊢ ( ( ( ( ♯ ‘ 𝑃 ) − 1 ) ∈ ℕ0 ∧ 𝐹 Fn ( 0 ..^ ( ( ♯ ‘ 𝑃 ) − 1 ) ) ) → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )
11	7 9 10	sylancl	⊢ ( ( 𝑃 ∈ Word 𝑉 ∧ 1 ≤ ( ♯ ‘ 𝑃 ) ) → ( ♯ ‘ 𝐹 ) = ( ( ♯ ‘ 𝑃 ) − 1 ) )