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 30972

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 6878	. . . . . . . 8 ⊢ (𝑔 = ∅ → (𝐹 ++ 𝑔) = (𝐹 ++ ∅))
2	1	fveq2d 6408	. . . . . . 7 ⊢ (𝑔 = ∅ → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ ∅)))
3	2	fveq1d 6406	. . . . . 6 ⊢ (𝑔 = ∅ → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ ∅))‘𝑁))
4	3	eqeq1d 2808	. . . . 5 ⊢ (𝑔 = ∅ → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))
5	4	imbi2d 331	. . . 4 ⊢ (𝑔 = ∅ → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁))))
6		oveq2 6878	. . . . . . . 8 ⊢ (𝑔 = 𝑒 → (𝐹 ++ 𝑔) = (𝐹 ++ 𝑒))
7	6	fveq2d 6408	. . . . . . 7 ⊢ (𝑔 = 𝑒 → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ 𝑒)))
8	7	fveq1d 6406	. . . . . 6 ⊢ (𝑔 = 𝑒 → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁))
9	8	eqeq1d 2808	. . . . 5 ⊢ (𝑔 = 𝑒 → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))
10	9	imbi2d 331	. . . 4 ⊢ (𝑔 = 𝑒 → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁))))
11		oveq2 6878	. . . . . . . 8 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝐹 ++ 𝑔) = (𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))
12	11	fveq2d 6408	. . . . . . 7 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩))))
13	12	fveq1d 6406	. . . . . 6 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁))
14	13	eqeq1d 2808	. . . . 5 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))
15	14	imbi2d 331	. . . 4 ⊢ (𝑔 = (𝑒 ++ ⟨“𝑘”⟩) → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘𝐹)‘𝑁))))
16		oveq2 6878	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → (𝐹 ++ 𝑔) = (𝐹 ++ 𝐺))
17	16	fveq2d 6408	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ 𝐺)))
18	17	fveq1d 6406	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ 𝐺))‘𝑁))
19	18	eqeq1d 2808	. . . . 5 ⊢ (𝑔 = 𝐺 → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))
20	19	imbi2d 331	. . . 4 ⊢ (𝑔 = 𝐺 → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁))))
21		ccatrid 13580	. . . . . . 7 ⊢ (𝐹 ∈ Word ℝ → (𝐹 ++ ∅) = 𝐹)
22	21	fveq2d 6408	. . . . . 6 ⊢ (𝐹 ∈ Word ℝ → (𝑇‘(𝐹 ++ ∅)) = (𝑇‘𝐹))
23	22	fveq1d 6406	. . . . 5 ⊢ (𝐹 ∈ Word ℝ → ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁))
24	23	adantr 468	. . . 4 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁))
25		simprl 778	. . . . . . . . . . . 12 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → 𝐹 ∈ Word ℝ)
26		simpll 774	. . . . . . . . . . . 12 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → 𝑒 ∈ Word ℝ)
27		simplr 776	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → 𝑘 ∈ ℝ)
28	27	s1cld 13594	. . . . . . . . . . . 12 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → ⟨“𝑘”⟩ ∈ Word ℝ)
29		ccatass 13581	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ∧ ⟨“𝑘”⟩ ∈ Word ℝ) → ((𝐹 ++ 𝑒) ++ ⟨“𝑘”⟩) = (𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))
30	25, 26, 28, 29	syl3anc 1483	. . . . . . . . . . 11 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → ((𝐹 ++ 𝑒) ++ ⟨“𝑘”⟩) = (𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))
31	30	fveq2d 6408	. . . . . . . . . 10 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → (𝑇‘((𝐹 ++ 𝑒) ++ ⟨“𝑘”⟩)) = (𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩))))
32	31	fveq1d 6406	. . . . . . . . 9 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → ((𝑇‘((𝐹 ++ 𝑒) ++ ⟨“𝑘”⟩))‘𝑁) = ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁))
33		ccatcl 13567	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ) → (𝐹 ++ 𝑒) ∈ Word ℝ)
34	25, 26, 33	syl2anc 575	. . . . . . . . . 10 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → (𝐹 ++ 𝑒) ∈ Word ℝ)
35		lencl 13531	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ∈ Word ℝ → (♯‘𝐹) ∈ ℕ₀)
36	25, 35	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → (♯‘𝐹) ∈ ℕ₀)
37	36	nn0zd 11742	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → (♯‘𝐹) ∈ ℤ)
38		lencl 13531	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ++ 𝑒) ∈ Word ℝ → (♯‘(𝐹 ++ 𝑒)) ∈ ℕ₀)
39	34, 38	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → (♯‘(𝐹 ++ 𝑒)) ∈ ℕ₀)
40	39	nn0zd 11742	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → (♯‘(𝐹 ++ 𝑒)) ∈ ℤ)
41	36	nn0red 11614	. . . . . . . . . . . . . . 15 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → (♯‘𝐹) ∈ ℝ)
42		lencl 13531	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ Word ℝ → (♯‘𝑒) ∈ ℕ₀)
43	26, 42	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → (♯‘𝑒) ∈ ℕ₀)
44		nn0addge1 11601	. . . . . . . . . . . . . . 15 ⊢ (((♯‘𝐹) ∈ ℝ ∧ (♯‘𝑒) ∈ ℕ₀) → (♯‘𝐹) ≤ ((♯‘𝐹) + (♯‘𝑒)))
45	41, 43, 44	syl2anc 575	. . . . . . . . . . . . . 14 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → (♯‘𝐹) ≤ ((♯‘𝐹) + (♯‘𝑒)))
46		ccatlen 13568	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ) → (♯‘(𝐹 ++ 𝑒)) = ((♯‘𝐹) + (♯‘𝑒)))
47	25, 26, 46	syl2anc 575	. . . . . . . . . . . . . 14 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → (♯‘(𝐹 ++ 𝑒)) = ((♯‘𝐹) + (♯‘𝑒)))
48	45, 47	breqtrrd 4872	. . . . . . . . . . . . 13 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → (♯‘𝐹) ≤ (♯‘(𝐹 ++ 𝑒)))
49		eluz2 11906	. . . . . . . . . . . . 13 ⊢ ((♯‘(𝐹 ++ 𝑒)) ∈ (ℤ_≥‘(♯‘𝐹)) ↔ ((♯‘𝐹) ∈ ℤ ∧ (♯‘(𝐹 ++ 𝑒)) ∈ ℤ ∧ (♯‘𝐹) ≤ (♯‘(𝐹 ++ 𝑒))))
50	37, 40, 48, 49	syl3anbrc 1436	. . . . . . . . . . . 12 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → (♯‘(𝐹 ++ 𝑒)) ∈ (ℤ_≥‘(♯‘𝐹)))
51		fzoss2 12716	. . . . . . . . . . . 12 ⊢ ((♯‘(𝐹 ++ 𝑒)) ∈ (ℤ_≥‘(♯‘𝐹)) → (0..^(♯‘𝐹)) ⊆ (0..^(♯‘(𝐹 ++ 𝑒))))
52	50, 51	syl 17	. . . . . . . . . . 11 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → (0..^(♯‘𝐹)) ⊆ (0..^(♯‘(𝐹 ++ 𝑒))))
53		simprr 780	. . . . . . . . . . 11 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → 𝑁 ∈ (0..^(♯‘𝐹)))
54	52, 53	sseldd 3799	. . . . . . . . . 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 30969	. . . . . . . . . 10 ⊢ (((𝐹 ++ 𝑒) ∈ Word ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑁 ∈ (0..^(♯‘(𝐹 ++ 𝑒)))) → ((𝑇‘((𝐹 ++ 𝑒) ++ ⟨“𝑘”⟩))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁))
60	34, 27, 54, 59	syl3anc 1483	. . . . . . . . 9 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → ((𝑇‘((𝐹 ++ 𝑒) ++ ⟨“𝑘”⟩))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁))
61	32, 60	eqtr3d 2842	. . . . . . . 8 ⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) → ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁))
62	61	adantr 468	. . . . . . 7 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) ∧ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁))
63		simpr 473	. . . . . . 7 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) ∧ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁))
64	62, 63	eqtrd 2840	. . . . . 6 ⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹)))) ∧ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘𝐹)‘𝑁))
65	64	exp31 408	. . . . 5 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁) → ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘𝐹)‘𝑁))))
66	65	a2d 29	. . . 4 ⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ (𝑒 ++ ⟨“𝑘”⟩)))‘𝑁) = ((𝑇‘𝐹)‘𝑁))))
67	5, 10, 15, 20, 24, 66	wrdind 13696	. . 3 ⊢ (𝐺 ∈ Word ℝ → ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))
68	67	3impib 1137	. 2 ⊢ ((𝐺 ∈ Word ℝ ∧ 𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁))
69	68	3com12 1146	1 ⊢ ((𝐹 ∈ Word ℝ ∧ 𝐺 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1100 = wceq 1637 ∈ wcel 2156 ≠ wne 2978 ⊆ wss 3769 ∅c0 4116 ifcif 4279 {cpr 4372 {ctp 4374 ⟨cop 4376 class class class wbr 4844 ↦ cmpt 4923 ‘cfv 6097 (class class class)co 6870 ↦ cmpt2 6872 ℝcr 10216 0cc0 10217 1c1 10218 + caddc 10220 ≤ cle 10356 − cmin 10547 -cneg 10548 ℕ₀cn0 11555 ℤcz 11639 ℤ_≥cuz 11900 ...cfz 12545 ..^cfzo 12685 ♯chash 13333 Word cword 13498 ++ cconcat 13500 ⟨“cs1 13501 sgncsgn 14045 Σcsu 14635 ndxcnx 16061 Basecbs 16064 +_gcplusg 16149 Σ_g cgsu 16302

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2068 ax-7 2104 ax-8 2158 ax-9 2165 ax-10 2185 ax-11 2201 ax-12 2214 ax-13 2420 ax-ext 2784 ax-rep 4964 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5096 ax-un 7175 ax-cnex 10273 ax-resscn 10274 ax-1cn 10275 ax-icn 10276 ax-addcl 10277 ax-addrcl 10278 ax-mulcl 10279 ax-mulrcl 10280 ax-mulcom 10281 ax-addass 10282 ax-mulass 10283 ax-distr 10284 ax-i2m1 10285 ax-1ne0 10286 ax-1rid 10287 ax-rnegex 10288 ax-rrecex 10289 ax-cnre 10290 ax-pre-lttri 10291 ax-pre-lttrn 10292 ax-pre-ltadd 10293 ax-pre-mulgt0 10294

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-3or 1101 df-3an 1102 df-tru 1641 df-ex 1860 df-nf 1864 df-sb 2061 df-eu 2634 df-mo 2635 df-clab 2793 df-cleq 2799 df-clel 2802 df-nfc 2937 df-ne 2979 df-nel 3082 df-ral 3101 df-rex 3102 df-reu 3103 df-rab 3105 df-v 3393 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-pss 3785 df-nul 4117 df-if 4280 df-pw 4353 df-sn 4371 df-pr 4373 df-tp 4375 df-op 4377 df-uni 4631 df-int 4670 df-iun 4714 df-br 4845 df-opab 4907 df-mpt 4924 df-tr 4947 df-id 5219 df-eprel 5224 df-po 5232 df-so 5233 df-fr 5270 df-we 5272 df-xp 5317 df-rel 5318 df-cnv 5319 df-co 5320 df-dm 5321 df-rn 5322 df-res 5323 df-ima 5324 df-pred 5893 df-ord 5939 df-on 5940 df-lim 5941 df-suc 5942 df-iota 6060 df-fun 6099 df-fn 6100 df-f 6101 df-f1 6102 df-fo 6103 df-f1o 6104 df-fv 6105 df-riota 6831 df-ov 6873 df-oprab 6874 df-mpt2 6875 df-om 7292 df-1st 7394 df-2nd 7395 df-wrecs 7638 df-recs 7700 df-rdg 7738 df-1o 7792 df-oadd 7796 df-er 7975 df-en 8189 df-dom 8190 df-sdom 8191 df-fin 8192 df-card 9044 df-pnf 10357 df-mnf 10358 df-xr 10359 df-ltxr 10360 df-le 10361 df-sub 10549 df-neg 10550 df-nn 11302 df-n0 11556 df-xnn0 11626 df-z 11640 df-uz 11901 df-fz 12546 df-fzo 12686 df-hash 13334 df-word 13506 df-lsw 13507 df-concat 13508 df-s1 13509 df-substr 13510

This theorem is referenced by: signstres 30973

W3C validator