Metamath Proof Explorer

Theorem signstres

Description: Restriction of a zero skipping sign to a subword. (Contributed by Thierry Arnoux, 11-Oct-2018)

Ref Expression
Hypotheses signsv.p ⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
signsv.w ⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
signsv.t ⊢ 𝑇 = ( 𝑓 ∈ Word ℝ ↦ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝑓 ‘ 𝑖 ) ) ) ) ) )
signsv.v ⊢ 𝑉 = ( 𝑓 ∈ Word ℝ ↦ Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇 ‘ 𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
Assertion signstres ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) = ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 signsv.p ⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
2 signsv.w ⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
3 signsv.t ⊢ 𝑇 = ( 𝑓 ∈ Word ℝ ↦ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝑓 ‘ 𝑖 ) ) ) ) ) )
4 signsv.v ⊢ 𝑉 = ( 𝑓 ∈ Word ℝ ↦ Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇 ‘ 𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
5 1 2 3 4 signstf ⊢ ( 𝐹 ∈ Word ℝ → ( 𝑇 ‘ 𝐹 ) ∈ Word ℝ )
6 wrdf ⊢ ( ( 𝑇 ‘ 𝐹 ) ∈ Word ℝ → ( 𝑇 ‘ 𝐹 ) : ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐹 ) ) ) ⟶ ℝ )
7 ffn ⊢ ( ( 𝑇 ‘ 𝐹 ) : ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐹 ) ) ) ⟶ ℝ → ( 𝑇 ‘ 𝐹 ) Fn ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐹 ) ) ) )
8 5 6 7 3syl ⊢ ( 𝐹 ∈ Word ℝ → ( 𝑇 ‘ 𝐹 ) Fn ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐹 ) ) ) )
9 1 2 3 4 signstlen ⊢ ( 𝐹 ∈ Word ℝ → ( ♯ ‘ ( 𝑇 ‘ 𝐹 ) ) = ( ♯ ‘ 𝐹 ) )
10 9 oveq2d ⊢ ( 𝐹 ∈ Word ℝ → ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐹 ) ) ) = ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
11 10 fneq2d ⊢ ( 𝐹 ∈ Word ℝ → ( ( 𝑇 ‘ 𝐹 ) Fn ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ 𝐹 ) ) ) ↔ ( 𝑇 ‘ 𝐹 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) )
12 8 11 mpbid ⊢ ( 𝐹 ∈ Word ℝ → ( 𝑇 ‘ 𝐹 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
13 fnresin ⊢ ( ( 𝑇 ‘ 𝐹 ) Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∩ ( 0 ..^ 𝑁 ) ) )
14 12 13 syl ⊢ ( 𝐹 ∈ Word ℝ → ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∩ ( 0 ..^ 𝑁 ) ) )
15 14 adantr ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∩ ( 0 ..^ 𝑁 ) ) )
16 elfzuz3 ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
17 fzoss2 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
18 16 17 syl ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
19 18 adantl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
20 incom ⊢ ( ( 0 ..^ 𝑁 ) ∩ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∩ ( 0 ..^ 𝑁 ) )
21 df-ss ⊢ ( ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ↔ ( ( 0 ..^ 𝑁 ) ∩ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( 0 ..^ 𝑁 ) )
22 21 biimpi ⊢ ( ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 0 ..^ 𝑁 ) ∩ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( 0 ..^ 𝑁 ) )
23 20 22 eqtr3id ⊢ ( ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∩ ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 ) )
24 23 fneq2d ⊢ ( ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → ( ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∩ ( 0 ..^ 𝑁 ) ) ↔ ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) ) )
25 19 24 syl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∩ ( 0 ..^ 𝑁 ) ) ↔ ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) ) )
26 15 25 mpbid ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) )
27 wrdres ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ∈ Word ℝ )
28 1 2 3 4 signstf ⊢ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ∈ Word ℝ → ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ∈ Word ℝ )
29 wrdf ⊢ ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ∈ Word ℝ → ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) : ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) ) ⟶ ℝ )
30 ffn ⊢ ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) : ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) ) ⟶ ℝ → ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) Fn ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) ) )
31 27 28 29 30 4syl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) Fn ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) ) )
32 1 2 3 4 signstlen ⊢ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ∈ Word ℝ → ( ♯ ‘ ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) = ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) )
33 27 32 syl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) = ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) )
34 wrdfn ⊢ ( 𝐹 ∈ Word ℝ → 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
35 fnssres ⊢ ( ( 𝐹 Fn ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ∧ ( 0 ..^ 𝑁 ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) )
36 34 18 35 syl2an ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) )
37 hashfn ⊢ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
38 36 37 syl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) = ( ♯ ‘ ( 0 ..^ 𝑁 ) ) )
39 elfznn0 ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → 𝑁 ∈ ℕ0 )
40 hashfzo0 ⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
41 39 40 syl ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
42 41 adantl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 0 ..^ 𝑁 ) ) = 𝑁 )
43 33 38 42 3eqtrd ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) = 𝑁 )
44 43 oveq2d ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) ) = ( 0 ..^ 𝑁 ) )
45 44 fneq2d ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) Fn ( 0 ..^ ( ♯ ‘ ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) ) ↔ ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) Fn ( 0 ..^ 𝑁 ) ) )
46 31 45 mpbid ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) Fn ( 0 ..^ 𝑁 ) )
47 fvres ⊢ ( 𝑚 ∈ ( 0 ..^ 𝑁 ) → ( ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑚 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑚 ) )
48 47 ad3antlr ⊢ ( ( ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑚 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑔 ∈ Word ℝ ) ∧ 𝐹 = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) ) → ( ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑚 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑚 ) )
49 simpr ⊢ ( ( ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑚 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑔 ∈ Word ℝ ) ∧ 𝐹 = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) ) → 𝐹 = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) )
50 49 fveq2d ⊢ ( ( ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑚 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑔 ∈ Word ℝ ) ∧ 𝐹 = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) ) → ( 𝑇 ‘ 𝐹 ) = ( 𝑇 ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) ) )
51 50 fveq1d ⊢ ( ( ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑚 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑔 ∈ Word ℝ ) ∧ 𝐹 = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) ) → ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑚 ) = ( ( 𝑇 ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) ) ‘ 𝑚 ) )
52 27 ad3antrrr ⊢ ( ( ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑚 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑔 ∈ Word ℝ ) ∧ 𝐹 = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) ) → ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ∈ Word ℝ )
53 simplr ⊢ ( ( ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑚 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑔 ∈ Word ℝ ) ∧ 𝐹 = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) ) → 𝑔 ∈ Word ℝ )
54 38 42 eqtrd ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) = 𝑁 )
55 54 oveq2d ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) = ( 0 ..^ 𝑁 ) )
56 55 eleq2d ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) ↔ 𝑚 ∈ ( 0 ..^ 𝑁 ) ) )
57 56 biimpar ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑚 ∈ ( 0 ..^ 𝑁 ) ) → 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) )
58 57 ad2antrr ⊢ ( ( ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑚 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑔 ∈ Word ℝ ) ∧ 𝐹 = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) ) → 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) )
59 1 2 3 4 signstfvc ⊢ ( ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ∈ Word ℝ ∧ 𝑔 ∈ Word ℝ ∧ 𝑚 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ) ) → ( ( 𝑇 ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) ) ‘ 𝑚 ) = ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ‘ 𝑚 ) )
60 52 53 58 59 syl3anc ⊢ ( ( ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑚 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑔 ∈ Word ℝ ) ∧ 𝐹 = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) ) → ( ( 𝑇 ‘ ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) ) ‘ 𝑚 ) = ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ‘ 𝑚 ) )
61 48 51 60 3eqtrd ⊢ ( ( ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑚 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑔 ∈ Word ℝ ) ∧ 𝐹 = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) ) → ( ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑚 ) = ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ‘ 𝑚 ) )
62 wrdsplex ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ∃ 𝑔 ∈ Word ℝ 𝐹 = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) )
63 62 adantr ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑚 ∈ ( 0 ..^ 𝑁 ) ) → ∃ 𝑔 ∈ Word ℝ 𝐹 = ( ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ++ 𝑔 ) )
64 61 63 r19.29a ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) ∧ 𝑚 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑚 ) = ( ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) ‘ 𝑚 ) )
65 26 46 64 eqfnfvd ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ 𝐹 ) ↾ ( 0 ..^ 𝑁 ) ) = ( 𝑇 ‘ ( 𝐹 ↾ ( 0 ..^ 𝑁 ) ) ) )