signstfvc - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > signstfvc		Structured version Visualization version GIF version

Theorem signstfvc 30651

Description: Zero-skipping sign in a word compared to a shorter word. (Contributed by Thierry Arnoux, 11-Oct-2018.)

**Hypotheses**
Ref	Expression
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**
Ref	Expression
signstfvc	⊢ ((𝐹 ∈ Word ℝ ∧ 𝐺 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁))

Distinct variable groups: 𝑎,𝑏, ⨣ 𝑓,𝑖,𝑛,𝐹 𝑓,𝑊,𝑖,𝑛 𝑖,𝑁,𝑛 Allowed substitution hints: ⨣ (𝑓,𝑖,𝑗,𝑛) 𝑇(𝑓,𝑖,𝑗,𝑛,𝑎,𝑏) 𝐹(𝑗,𝑎,𝑏) 𝐺(𝑓,𝑖,𝑗,𝑛,𝑎,𝑏) 𝑁(𝑓,𝑗,𝑎,𝑏) 𝑉(𝑓,𝑖,𝑗,𝑛,𝑎,𝑏) 𝑊(𝑗,𝑎,𝑏)

Proof of Theorem signstfvc Dummy variables 𝑒 𝑔 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 6658	. . . . . . . 8 ⊢ (𝑔 = ∅ → (𝐹 ++ 𝑔) = (𝐹 ++ ∅))
2	1	fveq2d 6195	. . . . . . 7 ⊢ (𝑔 = ∅ → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ ∅)))
3	2	fveq1d 6193	. . . . . 6 ⊢ (𝑔 = ∅ → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ ∅))‘𝑁))
4	3	eqeq1d 2624	. . . . 5 ⊢ (𝑔 = ∅ → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))
5	4	imbi2d 330	. . . 4 ⊢ (𝑔 = ∅ → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁))))
6		oveq2 6658	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (𝐹 ++ 𝑔) = (𝐹 ++ 𝑒))
7	6	fveq2d 6195	. . . . . . 7 ⊢ (𝑔 = 𝑒 → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ 𝑒)))
8	7	fveq1d 6193	. . . . . 6 ⊢ (𝑔 = 𝑒 → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁))
9	8	eqeq1d 2624	. . . . 5 ⊢ (𝑔 = 𝑒 → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))
10	9	imbi2d 330	. . . 4 ⊢ (𝑔 = 𝑒 → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁))))
11		oveq2 6658	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝐹 ++ 𝑔) = (𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))
12	11	fveq2d 6195	. . . . . . 7 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩))))
13	12	fveq1d 6193	. . . . . 6 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁))
14	13	eqeq1d 2624	. . . . 5 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))
15	14	imbi2d 330	. . . 4 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘𝐹)‘𝑁))))
16		oveq2 6658	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (𝐹 ++ 𝑔) = (𝐹 ++ 𝐺))
17	16	fveq2d 6195	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ 𝐺)))
18	17	fveq1d 6193	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ 𝐺))‘𝑁))
19	18	eqeq1d 2624	. . . . 5 ⊢ (𝑔 = 𝐺 → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))
20	19	imbi2d 330	. . . 4 ⊢ (𝑔 = 𝐺 → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁))))
21		ccatrid 13370	. . . . . . 7 ⊢ (𝐹 ∈ Word ℝ → (𝐹 ++ ∅) = 𝐹)
22	21	fveq2d 6195	. . . . . 6 ⊢ (𝐹 ∈ Word ℝ → (𝑇‘(𝐹 ++ ∅)) = (𝑇‘𝐹))
23	22	fveq1d 6193	. . . . 5 ⊢ (𝐹 ∈ Word ℝ → ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁))
24	23	adantr 481	. . . 4 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁))
25		simprl 794	. . . . . . . . . . . 12 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → 𝐹 ∈ Word ℝ)
26		simpll 790	. . . . . . . . . . . 12 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → 𝑒 ∈ Word ℝ)
27		simplr 792	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → 𝑘 ∈ ℝ)
28	27	s1cld 13383	. . . . . . . . . . . 12 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → ⟨“𝑘”⟩ ∈ Word ℝ)
29		ccatass 13371	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ∧ ⟨“𝑘”⟩ ∈ Word ℝ) → ((𝐹 ++ 𝑒) ++ ⟨“𝑘”⟩) = (𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))
30	25, 26, 28, 29	syl3anc 1326	. . . . . . . . . . 11 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → ((𝐹 ++ 𝑒) ++ ⟨“𝑘”⟩) = (𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))
31	30	fveq2d 6195	. . . . . . . . . 10 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (𝑇‘((𝐹 ++ 𝑒) ++ ⟨“𝑘”⟩)) = (𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩))))
32	31	fveq1d 6193	. . . . . . . . 9 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → ((𝑇‘((𝐹 ++ 𝑒) ++ ⟨“𝑘”⟩))‘𝑁) = ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁))
33		ccatcl 13359	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ) → (𝐹 ++ 𝑒) ∈ Word ℝ)
34	25, 26, 33	syl2anc 693	. . . . . . . . . 10 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (𝐹 ++ 𝑒) ∈ Word ℝ)
35		lencl 13324	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Word ℝ → (#‘𝐹) ∈ ℕ₀)
36	25, 35	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘𝐹) ∈ ℕ₀)
37	36	nn0zd 11480	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘𝐹) ∈ ℤ)
38		lencl 13324	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ++ 𝑒) ∈ Word ℝ → (#‘(𝐹 ++ 𝑒)) ∈ ℕ₀)
39	34, 38	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘(𝐹 ++ 𝑒)) ∈ ℕ₀)
40	39	nn0zd 11480	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘(𝐹 ++ 𝑒)) ∈ ℤ)
41	36	nn0red 11352	. . . . . . . . . . . . . . 15 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘𝐹) ∈ ℝ)
42		lencl 13324	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ Word ℝ → (#‘𝑒) ∈ ℕ₀)
43	26, 42	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘𝑒) ∈ ℕ₀)
44		nn0addge1 11339	. . . . . . . . . . . . . . 15 ⊢ (((#‘𝐹) ∈ ℝ ∧ (#‘𝑒) ∈ ℕ₀) → (#‘𝐹) ≤ ((#‘𝐹) + (#‘𝑒)))
45	41, 43, 44	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘𝐹) ≤ ((#‘𝐹) + (#‘𝑒)))
46		ccatlen 13360	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ) → (#‘(𝐹 ++ 𝑒)) = ((#‘𝐹) + (#‘𝑒)))
47	25, 26, 46	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘(𝐹 ++ 𝑒)) = ((#‘𝐹) + (#‘𝑒)))
48	45, 47	breqtrrd 4681	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘𝐹) ≤ (#‘(𝐹 ++ 𝑒)))
49		eluz2 11693	. . . . . . . . . . . . 13 ⊢ ((#‘(𝐹 ++ 𝑒)) ∈ (ℤ_≥‘(#‘𝐹)) ↔ ((#‘𝐹) ∈ ℤ ∧ (#‘(𝐹 ++ 𝑒)) ∈ ℤ ∧ (#‘𝐹) ≤ (#‘(𝐹 ++ 𝑒))))
50	37, 40, 48, 49	syl3anbrc 1246	. . . . . . . . . . . 12 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (#‘(𝐹 ++ 𝑒)) ∈ (ℤ_≥‘(#‘𝐹)))
51		fzoss2 12496	. . . . . . . . . . . 12 ⊢ ((#‘(𝐹 ++ 𝑒)) ∈ (ℤ_≥‘(#‘𝐹)) → (0..^(#‘𝐹)) ⊆ (0..^(#‘(𝐹 ++ 𝑒))))
52	50, 51	syl 17	. . . . . . . . . . 11 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → (0..^(#‘𝐹)) ⊆ (0..^(#‘(𝐹 ++ 𝑒))))
53		simprr 796	. . . . . . . . . . 11 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → 𝑁 ∈ (0..^(#‘𝐹)))
54	52, 53	sseldd 3604	. . . . . . . . . 10 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → 𝑁 ∈ (0..^(#‘(𝐹 ++ 𝑒))))
55		signsv.p	. . . . . . . . . . 11 ⊢ ⨣ = (𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦ if(𝑏 = 0, 𝑎, 𝑏))
56		signsv.w	. . . . . . . . . . 11 ⊢ 𝑊 = {⟨(Base‘ndx), {-1, 0, 1}⟩, ⟨(+_g‘ndx), ⨣ ⟩}
57		signsv.t	. . . . . . . . . . 11 ⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(#‘𝑓)) ↦ (𝑊 Σ_g (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖))))))
58		signsv.v	. . . . . . . . . . 11 ⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(#‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0))
59	55, 56, 57, 58	signstfvp 30648	. . . . . . . . . 10 ⊢ (((𝐹 ++ 𝑒) ∈ Word ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑁 ∈ (0..^(#‘(𝐹 ++ 𝑒)))) → ((𝑇‘((𝐹 ++ 𝑒) ++ ⟨“𝑘”⟩))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁))
60	34, 27, 54, 59	syl3anc 1326	. . . . . . . . 9 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → ((𝑇‘((𝐹 ++ 𝑒) ++ ⟨“𝑘”⟩))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁))
61	32, 60	eqtr3d 2658	. . . . . . . 8 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) → ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁))
62	61	adantr 481	. . . . . . 7 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) ∧ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁))
63		simpr 477	. . . . . . 7 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) ∧ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁))
64	62, 63	eqtrd 2656	. . . . . 6 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹)))) ∧ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘𝐹)‘𝑁))
65	64	exp31 630	. . . . 5 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → (((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁) → ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘𝐹)‘𝑁))))
66	65	a2d 29	. . . 4 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘𝐹)‘𝑁))))
67	5, 10, 15, 20, 24, 66	wrdind 13476	. . 3 ⊢ (𝐺 ∈ Word ℝ → ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))
68	67	3impib 1262	. 2 ⊢ ((𝐺 ∈ Word ℝ ∧ 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁))
69	68	3com12 1269	1 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐺 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ⊆ wss 3574 ∅c0 3915 ifcif 4086 {cpr 4179 {ctp 4181 ⟨cop 4183 class class class wbr 4653 ↦ cmpt 4729 ‘cfv 5888 (class class class)co 6650 ↦ cmpt2 6652 ℝcr 9935 0cc0 9936 1c1 9937 + caddc 9939 ≤ cle 10075 − cmin 10266 -cneg 10267 ℕ₀cn0 11292 ℤcz 11377 ℤ_≥cuz 11687 ...cfz 12326 ..^cfzo 12465 #chash 13117 Word cword 13291 ++ cconcat 13293 ⟨“cs1 13294 sgncsgn 13826 Σcsu 14416 ndxcnx 15854 Basecbs 15857 +_gcplusg 15941 Σ_g cgsu 16101

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466 df-hash 13118 df-word 13299 df-lsw 13300 df-concat 13301 df-s1 13302 df-substr 13303

This theorem is referenced by: signstres 30652

W3C validator