Metamath Proof Explorer

Theorem signstfvc

Description: Zero-skipping sign in a word compared to a shorter word. (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 signstfvc ( ( 𝐹 ∈ Word ℝ ∧ 𝐺 ∈ Word ℝ ∧ 𝑁 ∈ ( 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 oveq2 ⊢ ( 𝑔 = ∅ → ( 𝐹 ++ 𝑔 ) = ( 𝐹 ++ ∅ ) )
6 5 fveq2d ⊢ ( 𝑔 = ∅ → ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) = ( 𝑇 ‘ ( 𝐹 ++ ∅ ) ) )
7 6 fveq1d ⊢ ( 𝑔 = ∅ → ( ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ ( 𝐹 ++ ∅ ) ) ‘ 𝑁 ) )
8 7 eqeq1d ⊢ ( 𝑔 = ∅ → ( ( ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ↔ ( ( 𝑇 ‘ ( 𝐹 ++ ∅ ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) )
9 8 imbi2d ⊢ ( 𝑔 = ∅ → ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) ↔ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ ∅ ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) ) )
10 oveq2 ⊢ ( 𝑔 = 𝑒 → ( 𝐹 ++ 𝑔 ) = ( 𝐹 ++ 𝑒 ) )
11 10 fveq2d ⊢ ( 𝑔 = 𝑒 → ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) = ( 𝑇 ‘ ( 𝐹 ++ 𝑒 ) ) )
12 11 fveq1d ⊢ ( 𝑔 = 𝑒 → ( ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ ( 𝐹 ++ 𝑒 ) ) ‘ 𝑁 ) )
13 12 eqeq1d ⊢ ( 𝑔 = 𝑒 → ( ( ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ↔ ( ( 𝑇 ‘ ( 𝐹 ++ 𝑒 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) )
14 13 imbi2d ⊢ ( 𝑔 = 𝑒 → ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) ↔ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ 𝑒 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) ) )
15 oveq2 ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( 𝐹 ++ 𝑔 ) = ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) )
16 15 fveq2d ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) = ( 𝑇 ‘ ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) )
17 16 fveq1d ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ‘ 𝑁 ) )
18 17 eqeq1d ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( ( ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ↔ ( ( 𝑇 ‘ ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) )
19 18 imbi2d ⊢ ( 𝑔 = ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) → ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) ↔ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) ) )
20 oveq2 ⊢ ( 𝑔 = 𝐺 → ( 𝐹 ++ 𝑔 ) = ( 𝐹 ++ 𝐺 ) )
21 20 fveq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) = ( 𝑇 ‘ ( 𝐹 ++ 𝐺 ) ) )
22 21 fveq1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ ( 𝐹 ++ 𝐺 ) ) ‘ 𝑁 ) )
23 22 eqeq1d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ↔ ( ( 𝑇 ‘ ( 𝐹 ++ 𝐺 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) )
24 23 imbi2d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ 𝑔 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) ↔ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ 𝐺 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) ) )
25 ccatrid ⊢ ( 𝐹 ∈ Word ℝ → ( 𝐹 ++ ∅ ) = 𝐹 )
26 25 fveq2d ⊢ ( 𝐹 ∈ Word ℝ → ( 𝑇 ‘ ( 𝐹 ++ ∅ ) ) = ( 𝑇 ‘ 𝐹 ) )
27 26 fveq1d ⊢ ( 𝐹 ∈ Word ℝ → ( ( 𝑇 ‘ ( 𝐹 ++ ∅ ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) )
28 27 adantr ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ ∅ ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) )
29 s1cl ⊢ ( 𝑘 ∈ ℝ → ⟨“ 𝑘 ”⟩ ∈ Word ℝ )
30 ccatass ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ∧ ⟨“ 𝑘 ”⟩ ∈ Word ℝ ) → ( ( 𝐹 ++ 𝑒 ) ++ ⟨“ 𝑘 ”⟩ ) = ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) )
31 29 30 syl3an3 ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝐹 ++ 𝑒 ) ++ ⟨“ 𝑘 ”⟩ ) = ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) )
32 31 3expb ⊢ ( ( 𝐹 ∈ Word ℝ ∧ ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ) → ( ( 𝐹 ++ 𝑒 ) ++ ⟨“ 𝑘 ”⟩ ) = ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) )
33 32 adantlr ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ) → ( ( 𝐹 ++ 𝑒 ) ++ ⟨“ 𝑘 ”⟩ ) = ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) )
34 33 fveq2d ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ) → ( 𝑇 ‘ ( ( 𝐹 ++ 𝑒 ) ++ ⟨“ 𝑘 ”⟩ ) ) = ( 𝑇 ‘ ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) )
35 34 fveq1d ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ) → ( ( 𝑇 ‘ ( ( 𝐹 ++ 𝑒 ) ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ‘ 𝑁 ) )
36 ccatcl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ) → ( 𝐹 ++ 𝑒 ) ∈ Word ℝ )
37 36 ad2ant2r ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ) → ( 𝐹 ++ 𝑒 ) ∈ Word ℝ )
38 simprr ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ) → 𝑘 ∈ ℝ )
39 lencl ⊢ ( 𝐹 ∈ Word ℝ → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
40 39 nn0zd ⊢ ( 𝐹 ∈ Word ℝ → ( ♯ ‘ 𝐹 ) ∈ ℤ )
41 40 adantr ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ) → ( ♯ ‘ 𝐹 ) ∈ ℤ )
42 lencl ⊢ ( ( 𝐹 ++ 𝑒 ) ∈ Word ℝ → ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) ∈ ℕ0 )
43 36 42 syl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ) → ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) ∈ ℕ0 )
44 43 nn0zd ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ) → ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) ∈ ℤ )
45 39 nn0red ⊢ ( 𝐹 ∈ Word ℝ → ( ♯ ‘ 𝐹 ) ∈ ℝ )
46 lencl ⊢ ( 𝑒 ∈ Word ℝ → ( ♯ ‘ 𝑒 ) ∈ ℕ0 )
47 nn0addge1 ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℝ ∧ ( ♯ ‘ 𝑒 ) ∈ ℕ0 ) → ( ♯ ‘ 𝐹 ) ≤ ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ 𝑒 ) ) )
48 45 46 47 syl2an ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ) → ( ♯ ‘ 𝐹 ) ≤ ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ 𝑒 ) ) )
49 ccatlen ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ) → ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) = ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ 𝑒 ) ) )
50 48 49 breqtrrd ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ) → ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) )
51 eluz2 ⊢ ( ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( ( ♯ ‘ 𝐹 ) ∈ ℤ ∧ ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) ∈ ℤ ∧ ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) ) )
52 41 44 50 51 syl3anbrc ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ) → ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝐹 ) ) )
53 fzoss2 ⊢ ( ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝐹 ) ) → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) ) )
54 52 53 syl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ) → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) ) )
55 54 ad2ant2r ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ) → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) ) )
56 simplr ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
57 55 56 sseldd ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ) → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) ) )
58 1 2 3 4 signstfvp ⊢ ( ( ( 𝐹 ++ 𝑒 ) ∈ Word ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ ( 𝐹 ++ 𝑒 ) ) ) ) → ( ( 𝑇 ‘ ( ( 𝐹 ++ 𝑒 ) ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ ( 𝐹 ++ 𝑒 ) ) ‘ 𝑁 ) )
59 37 38 57 58 syl3anc ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ) → ( ( 𝑇 ‘ ( ( 𝐹 ++ 𝑒 ) ++ ⟨“ 𝑘 ”⟩ ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ ( 𝐹 ++ 𝑒 ) ) ‘ 𝑁 ) )
60 35 59 eqtr3d ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ ( 𝐹 ++ 𝑒 ) ) ‘ 𝑁 ) )
61 id ⊢ ( ( ( 𝑇 ‘ ( 𝐹 ++ 𝑒 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) → ( ( 𝑇 ‘ ( 𝐹 ++ 𝑒 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) )
62 60 61 sylan9eq ⊢ ( ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ) ∧ ( ( 𝑇 ‘ ( 𝐹 ++ 𝑒 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) )
63 62 ex ⊢ ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) ) → ( ( ( 𝑇 ‘ ( 𝐹 ++ 𝑒 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) → ( ( 𝑇 ‘ ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) )
64 63 expcom ⊢ ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) → ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑇 ‘ ( 𝐹 ++ 𝑒 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) → ( ( 𝑇 ‘ ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) ) )
65 64 a2d ⊢ ( ( 𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ) → ( ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ 𝑒 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) → ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ ( 𝑒 ++ ⟨“ 𝑘 ”⟩ ) ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) ) )
66 9 14 19 24 28 65 wrdind ⊢ ( 𝐺 ∈ Word ℝ → ( ( 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ 𝐺 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) ) )
67 66 3impib ⊢ ( ( 𝐺 ∈ Word ℝ ∧ 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ 𝐺 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) )
68 67 3com12 ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐺 ∈ Word ℝ ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ 𝐺 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) )