Metamath Proof Explorer


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 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝑃𝑘 ) ∈ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) )