Metamath Proof Explorer

Theorem iwrdsplit

Description: Lemma for sseqp1 . (Contributed by Thierry Arnoux, 25-Apr-2019) (Proof shortened by AV, 14-Oct-2022)

Ref Expression
Hypotheses iwrdsplit.s ⊢ ( 𝜑 → 𝑆 ∈ V )
iwrdsplit.f ⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ 𝑆 )
iwrdsplit.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion iwrdsplit ( 𝜑 → ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ ⟨“ ( 𝐹 ‘ 𝑁 ) ”⟩ ) )

Proof

Step Hyp Ref Expression
1 iwrdsplit.s ⊢ ( 𝜑 → 𝑆 ∈ V )
2 iwrdsplit.f ⊢ ( 𝜑 → 𝐹 : ℕ0 ⟶ 𝑆 )
3 iwrdsplit.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 1nn0 ⊢ 1 ∈ ℕ0
5 4 a1i ⊢ ( 𝜑 → 1 ∈ ℕ0 )
6 3 5 nn0addcld ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
7 1 2 6 subiwrd ⊢ ( 𝜑 → ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∈ Word 𝑆 )
8 1re ⊢ 1 ∈ ℝ
9 nn0addge2 ⊢ ( ( 1 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → 1 ≤ ( 𝑁 + 1 ) )
10 8 3 9 sylancr ⊢ ( 𝜑 → 1 ≤ ( 𝑁 + 1 ) )
11 1 2 6 subiwrdlen ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( 𝑁 + 1 ) )
12 10 11 breqtrrd ⊢ ( 𝜑 → 1 ≤ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) )
13 wrdlenge1n0 ⊢ ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∈ Word 𝑆 → ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ≠ ∅ ↔ 1 ≤ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ) )
14 7 13 syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ≠ ∅ ↔ 1 ≤ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ) )
15 12 14 mpbird ⊢ ( 𝜑 → ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ≠ ∅ )
16 pfxlswccat ⊢ ( ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∈ Word 𝑆 ∧ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ≠ ∅ ) → ( ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) prefix ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) − 1 ) ) ++ ⟨“ ( lastS ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ”⟩ ) = ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
17 7 15 16 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) prefix ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) − 1 ) ) ++ ⟨“ ( lastS ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ”⟩ ) = ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) )
18 3 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
19 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
20 18 19 11 mvrraddd ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) − 1 ) = 𝑁 )
21 20 oveq2d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) prefix ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) − 1 ) ) = ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) prefix 𝑁 ) )
22 nn0fz0 ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( 0 ... 𝑁 ) )
23 3 22 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
24 elfz0add ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → ( 𝑁 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) )
25 24 imp ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
26 3 5 23 25 syl21anc ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
27 11 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ) = ( 0 ... ( 𝑁 + 1 ) ) )
28 26 27 eleqtrrd ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ) )
29 pfxres ⊢ ( ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ) ) → ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) prefix 𝑁 ) = ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ↾ ( 0 ..^ 𝑁 ) ) )
30 7 28 29 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) prefix 𝑁 ) = ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ↾ ( 0 ..^ 𝑁 ) ) )
31 fzossfzop1 ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) )
32 resabs1 ⊢ ( ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( 𝑁 + 1 ) ) → ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ↾ ( 0 ..^ 𝑁 ) ) = ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) )
33 3 31 32 3syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ↾ ( 0 ..^ 𝑁 ) ) = ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) )
34 21 30 33 3eqtrd ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) prefix ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) − 1 ) ) = ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) )
35 lsw ⊢ ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ∈ Word 𝑆 → ( lastS ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) − 1 ) ) )
36 7 35 syl ⊢ ( 𝜑 → ( lastS ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) − 1 ) ) )
37 20 fveq2d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ‘ ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) − 1 ) ) = ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ‘ 𝑁 ) )
38 fzonn0p1 ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) )
39 fvres ⊢ ( 𝑁 ∈ ( 0 ..^ ( 𝑁 + 1 ) ) → ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ‘ 𝑁 ) = ( 𝐹 ‘ 𝑁 ) )
40 3 38 39 3syl ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ‘ 𝑁 ) = ( 𝐹 ‘ 𝑁 ) )
41 36 37 40 3eqtrd ⊢ ( 𝜑 → ( lastS ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( 𝐹 ‘ 𝑁 ) )
42 41 s1eqd ⊢ ( 𝜑 → ⟨“ ( lastS ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ”⟩ = ⟨“ ( 𝐹 ‘ 𝑁 ) ”⟩ )
43 34 42 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) prefix ( ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) − 1 ) ) ++ ⟨“ ( lastS ‘ ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ”⟩ ) = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ ⟨“ ( 𝐹 ‘ 𝑁 ) ”⟩ ) )
44 17 43 eqtr3d ⊢ ( 𝜑 → ( 𝐹 ↾ ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ ⟨“ ( 𝐹 ‘ 𝑁 ) ”⟩ ) )