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 ⊢ φ → S ∈ V
iwrdsplit.f ⊢ φ → F : ℕ 0 ⟶ S
iwrdsplit.n ⊢ φ → N ∈ ℕ 0
Assertion iwrdsplit ⊢ φ → F ↾ 0 ..^ N + 1 = F ↾ 0 ..^ N ++ ⟨“ F ⁡ N ”⟩

Proof

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