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 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ 𝐺 ) ) ‘ 𝑁 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑁 ) )