Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . 3
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
2 | | efgval.r |
. . 3
⊢ ∼ = (
~FG ‘𝐼) |
3 | | efgval2.m |
. . 3
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
4 | | efgval2.t |
. . 3
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
5 | 1, 2, 3, 4 | efgval2 18137 |
. 2
⊢ ∼ =
∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} |
6 | | efgcpbllem.1 |
. . . . . . 7
⊢ 𝐿 = {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ∼ ((𝐴 ++ 𝑗) ++ 𝐵))} |
7 | 6 | relopabi 5245 |
. . . . . 6
⊢ Rel 𝐿 |
8 | 7 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → Rel 𝐿) |
9 | | efgred.d |
. . . . . . . . 9
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) |
10 | | efgred.s |
. . . . . . . . 9
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) |
11 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 18167 |
. . . . . . . 8
⊢ (𝑓𝐿𝑔 ↔ (𝑓 ∈ 𝑊 ∧ 𝑔 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))) |
12 | 11 | simp2bi 1077 |
. . . . . . 7
⊢ (𝑓𝐿𝑔 → 𝑔 ∈ 𝑊) |
13 | 12 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑔 ∈ 𝑊) |
14 | 11 | simp1bi 1076 |
. . . . . . 7
⊢ (𝑓𝐿𝑔 → 𝑓 ∈ 𝑊) |
15 | 14 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑓 ∈ 𝑊) |
16 | 1, 2 | efger 18131 |
. . . . . . . 8
⊢ ∼ Er
𝑊 |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ∼ Er 𝑊) |
18 | 11 | simp3bi 1078 |
. . . . . . . 8
⊢ (𝑓𝐿𝑔 → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵)) |
19 | 18 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵)) |
20 | 17, 19 | ersym 7754 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) |
21 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 18167 |
. . . . . 6
⊢ (𝑔𝐿𝑓 ↔ (𝑔 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))) |
22 | 13, 15, 20, 21 | syl3anbrc 1246 |
. . . . 5
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑔𝐿𝑓) |
23 | 14 | ad2antrl 764 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓 ∈ 𝑊) |
24 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 18167 |
. . . . . . . 8
⊢ (𝑔𝐿ℎ ↔ (𝑔 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))) |
25 | 24 | simp2bi 1077 |
. . . . . . 7
⊢ (𝑔𝐿ℎ → ℎ ∈ 𝑊) |
26 | 25 | ad2antll 765 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ℎ ∈ 𝑊) |
27 | 16 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ∼ Er 𝑊) |
28 | 18 | ad2antrl 764 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵)) |
29 | 24 | simp3bi 1078 |
. . . . . . . 8
⊢ (𝑔𝐿ℎ → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)) |
30 | 29 | ad2antll 765 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)) |
31 | 27, 28, 30 | ertrd 7758 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)) |
32 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 18167 |
. . . . . 6
⊢ (𝑓𝐿ℎ ↔ (𝑓 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))) |
33 | 23, 26, 31, 32 | syl3anbrc 1246 |
. . . . 5
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓𝐿ℎ) |
34 | 16 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ∼ Er 𝑊) |
35 | | fviss 6256 |
. . . . . . . . . . . . . 14
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ⊆ Word (𝐼 ×
2𝑜) |
36 | 1, 35 | eqsstri 3635 |
. . . . . . . . . . . . 13
⊢ 𝑊 ⊆ Word (𝐼 ×
2𝑜) |
37 | | simpll 790 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐴 ∈ 𝑊) |
38 | 36, 37 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐴 ∈ Word (𝐼 ×
2𝑜)) |
39 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑓 ∈ 𝑊) |
40 | 36, 39 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑓 ∈ Word (𝐼 ×
2𝑜)) |
41 | | ccatcl 13359 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧ 𝑓 ∈ Word (𝐼 × 2𝑜)) →
(𝐴 ++ 𝑓) ∈ Word (𝐼 ×
2𝑜)) |
42 | 38, 40, 41 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝐴 ++ 𝑓) ∈ Word (𝐼 ×
2𝑜)) |
43 | | simplr 792 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐵 ∈ 𝑊) |
44 | 36, 43 | sseldi 3601 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐵 ∈ Word (𝐼 ×
2𝑜)) |
45 | | ccatcl 13359 |
. . . . . . . . . . 11
⊢ (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2𝑜) ∧ 𝐵 ∈ Word (𝐼 × 2𝑜)) →
((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 ×
2𝑜)) |
46 | 42, 44, 45 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 ×
2𝑜)) |
47 | 1 | efgrcl 18128 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 ×
2𝑜))) |
48 | 47 | simprd 479 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑊 → 𝑊 = Word (𝐼 ×
2𝑜)) |
49 | 48 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑊 = Word (𝐼 ×
2𝑜)) |
50 | 46, 49 | eleqtrrd 2704 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊) |
51 | 34, 50 | erref 7762 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) |
52 | 51 | ex 450 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))) |
53 | 52 | pm4.71d 666 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))) |
54 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 18167 |
. . . . . . 7
⊢ (𝑓𝐿𝑓 ↔ (𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))) |
55 | | df-3an 1039 |
. . . . . . 7
⊢ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))) |
56 | | anidm 676 |
. . . . . . . 8
⊢ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ↔ 𝑓 ∈ 𝑊) |
57 | 56 | anbi1i 731 |
. . . . . . 7
⊢ (((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))) |
58 | 54, 55, 57 | 3bitri 286 |
. . . . . 6
⊢ (𝑓𝐿𝑓 ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))) |
59 | 53, 58 | syl6bbr 278 |
. . . . 5
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 ↔ 𝑓𝐿𝑓)) |
60 | 8, 22, 33, 59 | iserd 7768 |
. . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 Er 𝑊) |
61 | 1, 2, 3, 4 | efgtf 18135 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝑊 → ((𝑇‘𝑓) = (𝑎 ∈ (0...(#‘𝑓)), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(𝑓 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∧ (𝑇‘𝑓):((0...(#‘𝑓)) × (𝐼 ×
2𝑜))⟶𝑊)) |
62 | 61 | simprd 479 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝑊 → (𝑇‘𝑓):((0...(#‘𝑓)) × (𝐼 ×
2𝑜))⟶𝑊) |
63 | 62 | adantl 482 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑇‘𝑓):((0...(#‘𝑓)) × (𝐼 ×
2𝑜))⟶𝑊) |
64 | | ffn 6045 |
. . . . . . . 8
⊢ ((𝑇‘𝑓):((0...(#‘𝑓)) × (𝐼 ×
2𝑜))⟶𝑊 → (𝑇‘𝑓) Fn ((0...(#‘𝑓)) × (𝐼 ×
2𝑜))) |
65 | | ovelrn 6810 |
. . . . . . . 8
⊢ ((𝑇‘𝑓) Fn ((0...(#‘𝑓)) × (𝐼 × 2𝑜)) →
(𝑎 ∈ ran (𝑇‘𝑓) ↔ ∃𝑐 ∈ (0...(#‘𝑓))∃𝑢 ∈ (𝐼 × 2𝑜)𝑎 = (𝑐(𝑇‘𝑓)𝑢))) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑎 ∈ ran (𝑇‘𝑓) ↔ ∃𝑐 ∈ (0...(#‘𝑓))∃𝑢 ∈ (𝐼 × 2𝑜)𝑎 = (𝑐(𝑇‘𝑓)𝑢))) |
67 | | simplr 792 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
𝑓 ∈ 𝑊) |
68 | 62 | ad2antlr 763 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝑇‘𝑓):((0...(#‘𝑓)) × (𝐼 ×
2𝑜))⟶𝑊) |
69 | | simprl 794 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
𝑐 ∈
(0...(#‘𝑓))) |
70 | | simprr 796 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
𝑢 ∈ (𝐼 ×
2𝑜)) |
71 | 68, 69, 70 | fovrnd 6806 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝑐(𝑇‘𝑓)𝑢) ∈ 𝑊) |
72 | 50 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊) |
73 | 37 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
𝐴 ∈ 𝑊) |
74 | 36, 73 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
𝐴 ∈ Word (𝐼 ×
2𝑜)) |
75 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
𝑓 ∈ Word (𝐼 ×
2𝑜)) |
76 | | swrdcl 13419 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ Word (𝐼 × 2𝑜) →
(𝑓 substr 〈0, 𝑐〉) ∈ Word (𝐼 ×
2𝑜)) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝑓 substr 〈0, 𝑐〉) ∈ Word (𝐼 ×
2𝑜)) |
78 | | ccatcl 13359 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧ (𝑓 substr 〈0, 𝑐〉) ∈ Word (𝐼 × 2𝑜))
→ (𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ∈ Word (𝐼 ×
2𝑜)) |
79 | 74, 77, 78 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ∈ Word (𝐼 ×
2𝑜)) |
80 | 3 | efgmf 18126 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑀:(𝐼 ×
2𝑜)⟶(𝐼 ×
2𝑜) |
81 | 80 | ffvelrni 6358 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ (𝐼 × 2𝑜) →
(𝑀‘𝑢) ∈ (𝐼 ×
2𝑜)) |
82 | 81 | ad2antll 765 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝑀‘𝑢) ∈ (𝐼 ×
2𝑜)) |
83 | 70, 82 | s2cld 13616 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
〈“𝑢(𝑀‘𝑢)”〉 ∈ Word (𝐼 ×
2𝑜)) |
84 | | ccatcl 13359 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ∈ Word (𝐼 × 2𝑜) ∧
〈“𝑢(𝑀‘𝑢)”〉 ∈ Word (𝐼 × 2𝑜)) →
((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ∈ Word (𝐼 ×
2𝑜)) |
85 | 79, 83, 84 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ∈ Word (𝐼 ×
2𝑜)) |
86 | | swrdcl 13419 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ Word (𝐼 × 2𝑜) →
(𝑓 substr 〈𝑐, (#‘𝑓)〉) ∈ Word (𝐼 ×
2𝑜)) |
87 | 75, 86 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝑓 substr 〈𝑐, (#‘𝑓)〉) ∈ Word (𝐼 ×
2𝑜)) |
88 | 44 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
𝐵 ∈ Word (𝐼 ×
2𝑜)) |
89 | | ccatass 13371 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ∈ Word (𝐼 × 2𝑜)
∧ (𝑓 substr 〈𝑐, (#‘𝑓)〉) ∈ Word (𝐼 × 2𝑜) ∧ 𝐵 ∈ Word (𝐼 × 2𝑜)) →
((((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) ++ 𝐵) = (((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ ((𝑓 substr 〈𝑐, (#‘𝑓)〉) ++ 𝐵))) |
90 | 85, 87, 88, 89 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) ++ 𝐵) = (((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ ((𝑓 substr 〈𝑐, (#‘𝑓)〉) ++ 𝐵))) |
91 | | ccatcl 13359 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 substr 〈0, 𝑐〉) ∈ Word (𝐼 × 2𝑜)
∧ 〈“𝑢(𝑀‘𝑢)”〉 ∈ Word (𝐼 × 2𝑜)) →
((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉) ∈ Word (𝐼 ×
2𝑜)) |
92 | 77, 83, 91 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉) ∈ Word (𝐼 ×
2𝑜)) |
93 | | ccatass 13371 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧
((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉) ∈ Word (𝐼 × 2𝑜)
∧ (𝑓 substr 〈𝑐, (#‘𝑓)〉) ∈ Word (𝐼 × 2𝑜)) →
((𝐴 ++ ((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉)) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) = (𝐴 ++ (((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)))) |
94 | 74, 92, 87, 93 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝐴 ++ ((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉)) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) = (𝐴 ++ (((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)))) |
95 | | ccatass 13371 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧ (𝑓 substr 〈0, 𝑐〉) ∈ Word (𝐼 × 2𝑜)
∧ 〈“𝑢(𝑀‘𝑢)”〉 ∈ Word (𝐼 × 2𝑜)) →
((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) = (𝐴 ++ ((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉))) |
96 | 74, 77, 83, 95 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) = (𝐴 ++ ((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉))) |
97 | 96 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) = ((𝐴 ++ ((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉)) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉))) |
98 | 1, 2, 3, 4 | efgtval 18136 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ 𝑊 ∧ 𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜)) →
(𝑐(𝑇‘𝑓)𝑢) = (𝑓 splice 〈𝑐, 𝑐, 〈“𝑢(𝑀‘𝑢)”〉〉)) |
99 | 67, 69, 70, 98 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝑐(𝑇‘𝑓)𝑢) = (𝑓 splice 〈𝑐, 𝑐, 〈“𝑢(𝑀‘𝑢)”〉〉)) |
100 | | splval 13502 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ 𝑊 ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑐 ∈ (0...(#‘𝑓)) ∧ 〈“𝑢(𝑀‘𝑢)”〉 ∈ Word (𝐼 × 2𝑜))) →
(𝑓 splice 〈𝑐, 𝑐, 〈“𝑢(𝑀‘𝑢)”〉〉) = (((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉))) |
101 | 67, 69, 69, 83, 100 | syl13anc 1328 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝑓 splice 〈𝑐, 𝑐, 〈“𝑢(𝑀‘𝑢)”〉〉) = (((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉))) |
102 | 99, 101 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝑐(𝑇‘𝑓)𝑢) = (((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉))) |
103 | 102 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) = (𝐴 ++ (((𝑓 substr 〈0, 𝑐〉) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)))) |
104 | 94, 97, 103 | 3eqtr4rd 2667 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) = (((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉))) |
105 | 104 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) = ((((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) ++ 𝐵)) |
106 | | lencl 13324 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ Word (𝐼 × 2𝑜) →
(#‘𝐴) ∈
ℕ0) |
107 | 74, 106 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘𝐴) ∈
ℕ0) |
108 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . 18
⊢
ℕ0 = (ℤ≥‘0) |
109 | 107, 108 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘𝐴) ∈
(ℤ≥‘0)) |
110 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ∈ (0...(#‘𝑓)) → 𝑐 ∈ ℕ0) |
111 | 110 | ad2antrl 764 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
𝑐 ∈
ℕ0) |
112 | | uzaddcl 11744 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝐴) ∈
(ℤ≥‘0) ∧ 𝑐 ∈ ℕ0) →
((#‘𝐴) + 𝑐) ∈
(ℤ≥‘0)) |
113 | 109, 111,
112 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((#‘𝐴) + 𝑐) ∈
(ℤ≥‘0)) |
114 | 42 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝐴 ++ 𝑓) ∈ Word (𝐼 ×
2𝑜)) |
115 | | ccatlen 13360 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2𝑜) ∧ 𝐵 ∈ Word (𝐼 × 2𝑜)) →
(#‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((#‘(𝐴 ++ 𝑓)) + (#‘𝐵))) |
116 | 114, 88, 115 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((#‘(𝐴 ++ 𝑓)) + (#‘𝐵))) |
117 | | ccatlen 13360 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧ 𝑓 ∈ Word (𝐼 × 2𝑜)) →
(#‘(𝐴 ++ 𝑓)) = ((#‘𝐴) + (#‘𝑓))) |
118 | 74, 75, 117 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘(𝐴 ++ 𝑓)) = ((#‘𝐴) + (#‘𝑓))) |
119 | | elfzuz3 12339 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 ∈ (0...(#‘𝑓)) → (#‘𝑓) ∈
(ℤ≥‘𝑐)) |
120 | 119 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘𝑓) ∈
(ℤ≥‘𝑐)) |
121 | 107 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘𝐴) ∈
ℤ) |
122 | | eluzadd 11716 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((#‘𝑓) ∈
(ℤ≥‘𝑐) ∧ (#‘𝐴) ∈ ℤ) → ((#‘𝑓) + (#‘𝐴)) ∈
(ℤ≥‘(𝑐 + (#‘𝐴)))) |
123 | 120, 121,
122 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((#‘𝑓) +
(#‘𝐴)) ∈
(ℤ≥‘(𝑐 + (#‘𝐴)))) |
124 | | lencl 13324 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ Word (𝐼 × 2𝑜) →
(#‘𝑓) ∈
ℕ0) |
125 | 75, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘𝑓) ∈
ℕ0) |
126 | 125 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘𝑓) ∈
ℂ) |
127 | 107 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘𝐴) ∈
ℂ) |
128 | 126, 127 | addcomd 10238 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((#‘𝑓) +
(#‘𝐴)) =
((#‘𝐴) +
(#‘𝑓))) |
129 | 111 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
𝑐 ∈
ℂ) |
130 | 129, 127 | addcomd 10238 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝑐 + (#‘𝐴)) = ((#‘𝐴) + 𝑐)) |
131 | 130 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(ℤ≥‘(𝑐 + (#‘𝐴))) =
(ℤ≥‘((#‘𝐴) + 𝑐))) |
132 | 123, 128,
131 | 3eltr3d 2715 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((#‘𝐴) +
(#‘𝑓)) ∈
(ℤ≥‘((#‘𝐴) + 𝑐))) |
133 | 118, 132 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘(𝐴 ++ 𝑓)) ∈
(ℤ≥‘((#‘𝐴) + 𝑐))) |
134 | | lencl 13324 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ Word (𝐼 × 2𝑜) →
(#‘𝐵) ∈
ℕ0) |
135 | 88, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘𝐵) ∈
ℕ0) |
136 | | uzaddcl 11744 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘(𝐴 ++
𝑓)) ∈
(ℤ≥‘((#‘𝐴) + 𝑐)) ∧ (#‘𝐵) ∈ ℕ0) →
((#‘(𝐴 ++ 𝑓)) + (#‘𝐵)) ∈
(ℤ≥‘((#‘𝐴) + 𝑐))) |
137 | 133, 135,
136 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((#‘(𝐴 ++ 𝑓)) + (#‘𝐵)) ∈
(ℤ≥‘((#‘𝐴) + 𝑐))) |
138 | 116, 137 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈
(ℤ≥‘((#‘𝐴) + 𝑐))) |
139 | | elfzuzb 12336 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐴) +
𝑐) ∈
(0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) ↔ (((#‘𝐴) + 𝑐) ∈ (ℤ≥‘0)
∧ (#‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈
(ℤ≥‘((#‘𝐴) + 𝑐)))) |
140 | 113, 138,
139 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((#‘𝐴) + 𝑐) ∈ (0...(#‘((𝐴 ++ 𝑓) ++ 𝐵)))) |
141 | 1, 2, 3, 4 | efgtval 18136 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((#‘𝐴) + 𝑐) ∈ (0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2𝑜)) →
(((#‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice 〈((#‘𝐴) + 𝑐), ((#‘𝐴) + 𝑐), 〈“𝑢(𝑀‘𝑢)”〉〉)) |
142 | 72, 140, 70, 141 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(((#‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice 〈((#‘𝐴) + 𝑐), ((#‘𝐴) + 𝑐), 〈“𝑢(𝑀‘𝑢)”〉〉)) |
143 | | wrd0 13330 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ Word (𝐼 ×
2𝑜) |
144 | 143 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
∅ ∈ Word (𝐼
× 2𝑜)) |
145 | | ccatcl 13359 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 substr 〈𝑐, (#‘𝑓)〉) ∈ Word (𝐼 × 2𝑜) ∧ 𝐵 ∈ Word (𝐼 × 2𝑜)) →
((𝑓 substr 〈𝑐, (#‘𝑓)〉) ++ 𝐵) ∈ Word (𝐼 ×
2𝑜)) |
146 | 87, 88, 145 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝑓 substr 〈𝑐, (#‘𝑓)〉) ++ 𝐵) ∈ Word (𝐼 ×
2𝑜)) |
147 | | ccatrid 13370 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ∈ Word (𝐼 × 2𝑜) →
((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ ∅) = (𝐴 ++ (𝑓 substr 〈0, 𝑐〉))) |
148 | 79, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ ∅) = (𝐴 ++ (𝑓 substr 〈0, 𝑐〉))) |
149 | 148 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ ∅) ++ ((𝑓 substr 〈𝑐, (#‘𝑓)〉) ++ 𝐵)) = ((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ ((𝑓 substr 〈𝑐, (#‘𝑓)〉) ++ 𝐵))) |
150 | | ccatass 13371 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ∈ Word (𝐼 × 2𝑜) ∧ (𝑓 substr 〈𝑐, (#‘𝑓)〉) ∈ Word (𝐼 × 2𝑜) ∧ 𝐵 ∈ Word (𝐼 × 2𝑜)) →
(((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) ++ 𝐵) = ((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ ((𝑓 substr 〈𝑐, (#‘𝑓)〉) ++ 𝐵))) |
151 | 79, 87, 88, 150 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) ++ 𝐵) = ((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ ((𝑓 substr 〈𝑐, (#‘𝑓)〉) ++ 𝐵))) |
152 | | ccatass 13371 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧ (𝑓 substr 〈0, 𝑐〉) ∈ Word (𝐼 × 2𝑜)
∧ (𝑓 substr 〈𝑐, (#‘𝑓)〉) ∈ Word (𝐼 × 2𝑜)) →
((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) = (𝐴 ++ ((𝑓 substr 〈0, 𝑐〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)))) |
153 | 74, 77, 87, 152 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) = (𝐴 ++ ((𝑓 substr 〈0, 𝑐〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)))) |
154 | 111, 108 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
𝑐 ∈
(ℤ≥‘0)) |
155 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑐)) |
156 | 154, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) → 0
∈ (0...𝑐)) |
157 | 125, 108 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘𝑓) ∈
(ℤ≥‘0)) |
158 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑓) ∈
(ℤ≥‘0) → (#‘𝑓) ∈ (0...(#‘𝑓))) |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘𝑓) ∈
(0...(#‘𝑓))) |
160 | | ccatswrd 13456 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∈ Word (𝐼 × 2𝑜) ∧ (0
∈ (0...𝑐) ∧ 𝑐 ∈ (0...(#‘𝑓)) ∧ (#‘𝑓) ∈ (0...(#‘𝑓)))) → ((𝑓 substr 〈0, 𝑐〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) = (𝑓 substr 〈0, (#‘𝑓)〉)) |
161 | 75, 156, 69, 159, 160 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝑓 substr 〈0, 𝑐〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) = (𝑓 substr 〈0, (#‘𝑓)〉)) |
162 | | swrdid 13428 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ Word (𝐼 × 2𝑜) →
(𝑓 substr 〈0,
(#‘𝑓)〉) = 𝑓) |
163 | 75, 162 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝑓 substr 〈0,
(#‘𝑓)〉) = 𝑓) |
164 | 161, 163 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝑓 substr 〈0, 𝑐〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) = 𝑓) |
165 | 164 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝐴 ++ ((𝑓 substr 〈0, 𝑐〉) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉))) = (𝐴 ++ 𝑓)) |
166 | 153, 165 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) = (𝐴 ++ 𝑓)) |
167 | 166 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ (𝑓 substr 〈𝑐, (#‘𝑓)〉)) ++ 𝐵) = ((𝐴 ++ 𝑓) ++ 𝐵)) |
168 | 149, 151,
167 | 3eqtr2rd 2663 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝐴 ++ 𝑓) ++ 𝐵) = (((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ ∅) ++ ((𝑓 substr 〈𝑐, (#‘𝑓)〉) ++ 𝐵))) |
169 | | ccatlen 13360 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word (𝐼 × 2𝑜) ∧ (𝑓 substr 〈0, 𝑐〉) ∈ Word (𝐼 × 2𝑜))
→ (#‘(𝐴 ++
(𝑓 substr 〈0, 𝑐〉))) = ((#‘𝐴) + (#‘(𝑓 substr 〈0, 𝑐〉)))) |
170 | 74, 77, 169 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘(𝐴 ++ (𝑓 substr 〈0, 𝑐〉))) = ((#‘𝐴) + (#‘(𝑓 substr 〈0, 𝑐〉)))) |
171 | | swrd0len 13422 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ Word (𝐼 × 2𝑜) ∧ 𝑐 ∈ (0...(#‘𝑓))) → (#‘(𝑓 substr 〈0, 𝑐〉)) = 𝑐) |
172 | 75, 69, 171 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(#‘(𝑓 substr 〈0,
𝑐〉)) = 𝑐) |
173 | 172 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((#‘𝐴) +
(#‘(𝑓 substr 〈0,
𝑐〉))) =
((#‘𝐴) + 𝑐)) |
174 | 170, 173 | eqtr2d 2657 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((#‘𝐴) + 𝑐) = (#‘(𝐴 ++ (𝑓 substr 〈0, 𝑐〉)))) |
175 | | hash0 13158 |
. . . . . . . . . . . . . . . . 17
⊢
(#‘∅) = 0 |
176 | 175 | oveq2i 6661 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐴) +
𝑐) + (#‘∅)) =
(((#‘𝐴) + 𝑐) + 0) |
177 | 107, 111 | nn0addcld 11355 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((#‘𝐴) + 𝑐) ∈
ℕ0) |
178 | 177 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((#‘𝐴) + 𝑐) ∈
ℂ) |
179 | 178 | addid1d 10236 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(((#‘𝐴) + 𝑐) + 0) = ((#‘𝐴) + 𝑐)) |
180 | 176, 179 | syl5req 2669 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((#‘𝐴) + 𝑐) = (((#‘𝐴) + 𝑐) + (#‘∅))) |
181 | 79, 144, 146, 83, 168, 174, 180 | splval2 13508 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(((𝐴 ++ 𝑓) ++ 𝐵) splice 〈((#‘𝐴) + 𝑐), ((#‘𝐴) + 𝑐), 〈“𝑢(𝑀‘𝑢)”〉〉) = (((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ ((𝑓 substr 〈𝑐, (#‘𝑓)〉) ++ 𝐵))) |
182 | 142, 181 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(((#‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ (𝑓 substr 〈0, 𝑐〉)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ ((𝑓 substr 〈𝑐, (#‘𝑓)〉) ++ 𝐵))) |
183 | 90, 105, 182 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) = (((#‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢)) |
184 | 1, 2, 3, 4 | efgtf 18135 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) = (𝑎 ∈ (0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))), 𝑏 ∈ (𝐼 × 2𝑜) ↦
(((𝐴 ++ 𝑓) ++ 𝐵) splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∧ (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 ×
2𝑜))⟶𝑊)) |
185 | 184 | simprd 479 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 ×
2𝑜))⟶𝑊) |
186 | | ffn 6045 |
. . . . . . . . . . . . . 14
⊢ ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 ×
2𝑜))⟶𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 ×
2𝑜))) |
187 | 72, 185, 186 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 ×
2𝑜))) |
188 | | fnovrn 6809 |
. . . . . . . . . . . . 13
⊢ (((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2𝑜)) ∧
((#‘𝐴) + 𝑐) ∈ (0...(#‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2𝑜)) →
(((#‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) |
189 | 187, 140,
70, 188 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(((#‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) |
190 | 183, 189 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) |
191 | 1, 2, 3, 4 | efgi2 18138 |
. . . . . . . . . . 11
⊢ ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵)) |
192 | 72, 190, 191 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵)) |
193 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 18167 |
. . . . . . . . . 10
⊢ (𝑓𝐿(𝑐(𝑇‘𝑓)𝑢) ↔ (𝑓 ∈ 𝑊 ∧ (𝑐(𝑇‘𝑓)𝑢) ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵))) |
194 | 67, 71, 192, 193 | syl3anbrc 1246 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
𝑓𝐿(𝑐(𝑇‘𝑓)𝑢)) |
195 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
196 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑓 ∈ V |
197 | 195, 196 | elec 7786 |
. . . . . . . . . 10
⊢ (𝑎 ∈ [𝑓]𝐿 ↔ 𝑓𝐿𝑎) |
198 | | breq2 4657 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → (𝑓𝐿𝑎 ↔ 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢))) |
199 | 197, 198 | syl5bb 272 |
. . . . . . . . 9
⊢ (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → (𝑎 ∈ [𝑓]𝐿 ↔ 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢))) |
200 | 194, 199 | syl5ibrcom 237 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(#‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2𝑜))) →
(𝑎 = (𝑐(𝑇‘𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿)) |
201 | 200 | rexlimdvva 3038 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (∃𝑐 ∈ (0...(#‘𝑓))∃𝑢 ∈ (𝐼 × 2𝑜)𝑎 = (𝑐(𝑇‘𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿)) |
202 | 66, 201 | sylbid 230 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑎 ∈ ran (𝑇‘𝑓) → 𝑎 ∈ [𝑓]𝐿)) |
203 | 202 | ssrdv 3609 |
. . . . 5
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ran (𝑇‘𝑓) ⊆ [𝑓]𝐿) |
204 | 203 | ralrimiva 2966 |
. . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿) |
205 | | fvex 6201 |
. . . . . . 7
⊢ ( I
‘Word (𝐼 ×
2𝑜)) ∈ V |
206 | 1, 205 | eqeltri 2697 |
. . . . . 6
⊢ 𝑊 ∈ V |
207 | | erex 7766 |
. . . . . 6
⊢ (𝐿 Er 𝑊 → (𝑊 ∈ V → 𝐿 ∈ V)) |
208 | 60, 206, 207 | mpisyl 21 |
. . . . 5
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 ∈ V) |
209 | | ereq1 7749 |
. . . . . . 7
⊢ (𝑟 = 𝐿 → (𝑟 Er 𝑊 ↔ 𝐿 Er 𝑊)) |
210 | | eceq2 7784 |
. . . . . . . . 9
⊢ (𝑟 = 𝐿 → [𝑓]𝑟 = [𝑓]𝐿) |
211 | 210 | sseq2d 3633 |
. . . . . . . 8
⊢ (𝑟 = 𝐿 → (ran (𝑇‘𝑓) ⊆ [𝑓]𝑟 ↔ ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)) |
212 | 211 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑟 = 𝐿 → (∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟 ↔ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)) |
213 | 209, 212 | anbi12d 747 |
. . . . . 6
⊢ (𝑟 = 𝐿 → ((𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟) ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))) |
214 | 213 | elabg 3351 |
. . . . 5
⊢ (𝐿 ∈ V → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))) |
215 | 208, 214 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))) |
216 | 60, 204, 215 | mpbir2and 957 |
. . 3
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)}) |
217 | | intss1 4492 |
. . 3
⊢ (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿) |
218 | 216, 217 | syl 17 |
. 2
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿) |
219 | 5, 218 | syl5eqss 3649 |
1
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∼ ⊆ 𝐿) |