Theorem wlkdlem2

Description: Lemma 2 for wlkd . (Contributed by AV, 7-Feb-2021)

	Ref	Expression
Hypotheses	wlkd.p	⊢ ( 𝜑 → 𝑃 ∈ Word V )
	wlkd.f	⊢ ( 𝜑 → 𝐹 ∈ Word V )
	wlkd.l	⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
	wlkd.e	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
Assertion	wlkdlem2	⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		wlkd.p	⊢ ( 𝜑 → 𝑃 ∈ Word V )
2		wlkd.f	⊢ ( 𝜑 → 𝐹 ∈ Word V )
3		wlkd.l	⊢ ( 𝜑 → ( ♯ ‘ 𝑃 ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
4		wlkd.e	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
5		fzo0end	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
6		fveq2	⊢ ( 𝑘 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
7		fvoveq1	⊢ ( 𝑘 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) )
8	6 7	preq12d	⊢ ( 𝑘 = ( ( ♯ ‘ 𝐹 ) − 1 ) → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } )
9		2fveq3	⊢ ( 𝑘 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
10	8 9	sseq12d	⊢ ( 𝑘 = ( ( ♯ ‘ 𝐹 ) − 1 ) → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
11	10	rspcv	⊢ ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
12	5 11	syl	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
13		fvex	⊢ ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ V
14		fvex	⊢ ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) ∈ V
15	13 14	prss	⊢ ( ( ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∧ ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ↔ { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
16		nncn	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ♯ ‘ 𝐹 ) ∈ ℂ )
17		npcan1	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℂ → ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐹 ) )
18	16 17	syl	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐹 ) )
19	18	fveq2d	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) )
20	19	eleq1d	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↔ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
21	20	biimpd	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
22	21	adantld	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∧ ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
23	15 22	syl5bir	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( { ( 𝑃 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , ( 𝑃 ‘ ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
24	12 23	syld	⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
25	4 24	syl5com	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
26		fvex	⊢ ( 𝑃 ‘ 𝑘 ) ∈ V
27		fvex	⊢ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ V
28	26 27	prss	⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) ↔ { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
29		simpl	⊢ ( ( ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ∧ ( 𝑃 ‘ ( 𝑘 + 1 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
30	28 29	sylbir	⊢ ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
31	30	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
32	31	ralimdva	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )
33	4 32	mpd	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
34	25 33	jca	⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃 ‘ 𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ) )