Step | Hyp | Ref
| Expression |
1 | | oveq2 6800 |
. . . . . . . 8
⊢ (𝑔 = ∅ → (𝐹 ++ 𝑔) = (𝐹 ++ ∅)) |
2 | 1 | fveq2d 6336 |
. . . . . . 7
⊢ (𝑔 = ∅ → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ ∅))) |
3 | 2 | fveq1d 6334 |
. . . . . 6
⊢ (𝑔 = ∅ → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ ∅))‘𝑁)) |
4 | 3 | eqeq1d 2772 |
. . . . 5
⊢ (𝑔 = ∅ → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁))) |
5 | 4 | imbi2d 329 |
. . . 4
⊢ (𝑔 = ∅ → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))) |
6 | | oveq2 6800 |
. . . . . . . 8
⊢ (𝑔 = 𝑒 → (𝐹 ++ 𝑔) = (𝐹 ++ 𝑒)) |
7 | 6 | fveq2d 6336 |
. . . . . . 7
⊢ (𝑔 = 𝑒 → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ 𝑒))) |
8 | 7 | fveq1d 6334 |
. . . . . 6
⊢ (𝑔 = 𝑒 → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁)) |
9 | 8 | eqeq1d 2772 |
. . . . 5
⊢ (𝑔 = 𝑒 → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁))) |
10 | 9 | imbi2d 329 |
. . . 4
⊢ (𝑔 = 𝑒 → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))) |
11 | | oveq2 6800 |
. . . . . . . 8
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (𝐹 ++ 𝑔) = (𝐹 ++ (𝑒 ++ 〈“𝑘”〉))) |
12 | 11 | fveq2d 6336 |
. . . . . . 7
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))) |
13 | 12 | fveq1d 6334 |
. . . . . 6
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁)) |
14 | 13 | eqeq1d 2772 |
. . . . 5
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘𝐹)‘𝑁))) |
15 | 14 | imbi2d 329 |
. . . 4
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))) |
16 | | oveq2 6800 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (𝐹 ++ 𝑔) = (𝐹 ++ 𝐺)) |
17 | 16 | fveq2d 6336 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (𝑇‘(𝐹 ++ 𝑔)) = (𝑇‘(𝐹 ++ 𝐺))) |
18 | 17 | fveq1d 6334 |
. . . . . 6
⊢ (𝑔 = 𝐺 → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘(𝐹 ++ 𝐺))‘𝑁)) |
19 | 18 | eqeq1d 2772 |
. . . . 5
⊢ (𝑔 = 𝐺 → (((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁) ↔ ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁))) |
20 | 19 | imbi2d 329 |
. . . 4
⊢ (𝑔 = 𝐺 → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝑔))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) ↔ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))) |
21 | | ccatrid 13568 |
. . . . . . 7
⊢ (𝐹 ∈ Word ℝ →
(𝐹 ++ ∅) = 𝐹) |
22 | 21 | fveq2d 6336 |
. . . . . 6
⊢ (𝐹 ∈ Word ℝ →
(𝑇‘(𝐹 ++ ∅)) = (𝑇‘𝐹)) |
23 | 22 | fveq1d 6334 |
. . . . 5
⊢ (𝐹 ∈ Word ℝ →
((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |
24 | 23 | adantr 466 |
. . . 4
⊢ ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ ∅))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |
25 | | simprl 746 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ 𝐹 ∈ Word
ℝ) |
26 | | simpll 742 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ 𝑒 ∈ Word
ℝ) |
27 | | simplr 744 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ 𝑘 ∈
ℝ) |
28 | 27 | s1cld 13582 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ 〈“𝑘”〉 ∈ Word
ℝ) |
29 | | ccatass 13569 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ ∧
〈“𝑘”〉
∈ Word ℝ) → ((𝐹 ++ 𝑒) ++ 〈“𝑘”〉) = (𝐹 ++ (𝑒 ++ 〈“𝑘”〉))) |
30 | 25, 26, 28, 29 | syl3anc 1475 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ ((𝐹 ++ 𝑒) ++ 〈“𝑘”〉) = (𝐹 ++ (𝑒 ++ 〈“𝑘”〉))) |
31 | 30 | fveq2d 6336 |
. . . . . . . . . 10
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ (𝑇‘((𝐹 ++ 𝑒) ++ 〈“𝑘”〉)) = (𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))) |
32 | 31 | fveq1d 6334 |
. . . . . . . . 9
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ ((𝑇‘((𝐹 ++ 𝑒) ++ 〈“𝑘”〉))‘𝑁) = ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁)) |
33 | | ccatcl 13555 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ) →
(𝐹 ++ 𝑒) ∈ Word ℝ) |
34 | 25, 26, 33 | syl2anc 565 |
. . . . . . . . . 10
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ (𝐹 ++ 𝑒) ∈ Word
ℝ) |
35 | | lencl 13519 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ Word ℝ →
(♯‘𝐹) ∈
ℕ0) |
36 | 25, 35 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ (♯‘𝐹)
∈ ℕ0) |
37 | 36 | nn0zd 11681 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ (♯‘𝐹)
∈ ℤ) |
38 | | lencl 13519 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ++ 𝑒) ∈ Word ℝ →
(♯‘(𝐹 ++ 𝑒)) ∈
ℕ0) |
39 | 34, 38 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ (♯‘(𝐹 ++
𝑒)) ∈
ℕ0) |
40 | 39 | nn0zd 11681 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ (♯‘(𝐹 ++
𝑒)) ∈
ℤ) |
41 | 36 | nn0red 11553 |
. . . . . . . . . . . . . . 15
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ (♯‘𝐹)
∈ ℝ) |
42 | | lencl 13519 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 ∈ Word ℝ →
(♯‘𝑒) ∈
ℕ0) |
43 | 26, 42 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ (♯‘𝑒)
∈ ℕ0) |
44 | | nn0addge1 11540 |
. . . . . . . . . . . . . . 15
⊢
(((♯‘𝐹)
∈ ℝ ∧ (♯‘𝑒) ∈ ℕ0) →
(♯‘𝐹) ≤
((♯‘𝐹) +
(♯‘𝑒))) |
45 | 41, 43, 44 | syl2anc 565 |
. . . . . . . . . . . . . 14
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ (♯‘𝐹)
≤ ((♯‘𝐹) +
(♯‘𝑒))) |
46 | | ccatlen 13556 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ∈ Word ℝ ∧ 𝑒 ∈ Word ℝ) →
(♯‘(𝐹 ++ 𝑒)) = ((♯‘𝐹) + (♯‘𝑒))) |
47 | 25, 26, 46 | syl2anc 565 |
. . . . . . . . . . . . . 14
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ (♯‘(𝐹 ++
𝑒)) = ((♯‘𝐹) + (♯‘𝑒))) |
48 | 45, 47 | breqtrrd 4812 |
. . . . . . . . . . . . 13
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ (♯‘𝐹)
≤ (♯‘(𝐹 ++
𝑒))) |
49 | | eluz2 11893 |
. . . . . . . . . . . . 13
⊢
((♯‘(𝐹
++ 𝑒)) ∈
(ℤ≥‘(♯‘𝐹)) ↔ ((♯‘𝐹) ∈ ℤ ∧ (♯‘(𝐹 ++ 𝑒)) ∈ ℤ ∧ (♯‘𝐹) ≤ (♯‘(𝐹 ++ 𝑒)))) |
50 | 37, 40, 48, 49 | syl3anbrc 1427 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ (♯‘(𝐹 ++
𝑒)) ∈
(ℤ≥‘(♯‘𝐹))) |
51 | | fzoss2 12703 |
. . . . . . . . . . . 12
⊢
((♯‘(𝐹
++ 𝑒)) ∈
(ℤ≥‘(♯‘𝐹)) → (0..^(♯‘𝐹)) ⊆
(0..^(♯‘(𝐹 ++
𝑒)))) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ (0..^(♯‘𝐹)) ⊆ (0..^(♯‘(𝐹 ++ 𝑒)))) |
53 | | simprr 748 |
. . . . . . . . . . 11
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ 𝑁 ∈
(0..^(♯‘𝐹))) |
54 | 52, 53 | sseldd 3751 |
. . . . . . . . . 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 30982 |
. . . . . . . . . 10
⊢ (((𝐹 ++ 𝑒) ∈ Word ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑁 ∈
(0..^(♯‘(𝐹 ++
𝑒)))) → ((𝑇‘((𝐹 ++ 𝑒) ++ 〈“𝑘”〉))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁)) |
60 | 34, 27, 54, 59 | syl3anc 1475 |
. . . . . . . . 9
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ ((𝑇‘((𝐹 ++ 𝑒) ++ 〈“𝑘”〉))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁)) |
61 | 32, 60 | eqtr3d 2806 |
. . . . . . . 8
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
→ ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁)) |
62 | 61 | adantr 466 |
. . . . . . 7
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
∧ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘(𝐹 ++ 𝑒))‘𝑁)) |
63 | | simpr 471 |
. . . . . . 7
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
∧ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |
64 | 62, 63 | eqtrd 2804 |
. . . . . 6
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹))))
∧ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |
65 | 64 | exp31 406 |
. . . . 5
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ (((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁) → ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))) |
66 | 65 | a2d 29 |
. . . 4
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (((𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ 𝑒))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) → ((𝐹 ∈ Word ℝ ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘(𝐹 ++ (𝑒 ++ 〈“𝑘”〉)))‘𝑁) = ((𝑇‘𝐹)‘𝑁)))) |
67 | 5, 10, 15, 20, 24, 66 | wrdind 13684 |
. . 3
⊢ (𝐺 ∈ Word ℝ →
((𝐹 ∈ Word ℝ
∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁))) |
68 | 67 | 3impib 1107 |
. 2
⊢ ((𝐺 ∈ Word ℝ ∧ 𝐹 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |
69 | 68 | 3com12 1116 |
1
⊢ ((𝐹 ∈ Word ℝ ∧ 𝐺 ∈ Word ℝ ∧ 𝑁 ∈
(0..^(♯‘𝐹)))
→ ((𝑇‘(𝐹 ++ 𝐺))‘𝑁) = ((𝑇‘𝐹)‘𝑁)) |