Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . 3
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) |
2 | | efgval.r |
. . 3
⊢ ∼ = (
~FG ‘𝐼) |
3 | | efgval2.m |
. . 3
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) |
4 | | efgval2.t |
. . 3
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
5 | 1, 2, 3, 4 | efgval2 19114 |
. 2
⊢ ∼ =
∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} |
6 | | efgcpbllem.1 |
. . . . . . 7
⊢ 𝐿 = {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑊 ∧ ((𝐴 ++ 𝑖) ++ 𝐵) ∼ ((𝐴 ++ 𝑗) ++ 𝐵))} |
7 | 6 | relopabiv 5690 |
. . . . . 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 19144 |
. . . . . . . 8
⊢ (𝑓𝐿𝑔 ↔ (𝑓 ∈ 𝑊 ∧ 𝑔 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵))) |
12 | 11 | simp2bi 1148 |
. . . . . . 7
⊢ (𝑓𝐿𝑔 → 𝑔 ∈ 𝑊) |
13 | 12 | adantl 485 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑔 ∈ 𝑊) |
14 | 11 | simp1bi 1147 |
. . . . . . 7
⊢ (𝑓𝐿𝑔 → 𝑓 ∈ 𝑊) |
15 | 14 | adantl 485 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑓 ∈ 𝑊) |
16 | 1, 2 | efger 19108 |
. . . . . . . 8
⊢ ∼ Er
𝑊 |
17 | 16 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ∼ Er 𝑊) |
18 | 11 | simp3bi 1149 |
. . . . . . . 8
⊢ (𝑓𝐿𝑔 → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵)) |
19 | 18 | adantl 485 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵)) |
20 | 17, 19 | ersym 8403 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) |
21 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 19144 |
. . . . . 6
⊢ (𝑔𝐿𝑓 ↔ (𝑔 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))) |
22 | 13, 15, 20, 21 | syl3anbrc 1345 |
. . . . 5
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓𝐿𝑔) → 𝑔𝐿𝑓) |
23 | 14 | ad2antrl 728 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓 ∈ 𝑊) |
24 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 19144 |
. . . . . . . 8
⊢ (𝑔𝐿ℎ ↔ (𝑔 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))) |
25 | 24 | simp2bi 1148 |
. . . . . . 7
⊢ (𝑔𝐿ℎ → ℎ ∈ 𝑊) |
26 | 25 | ad2antll 729 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ℎ ∈ 𝑊) |
27 | 16 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ∼ Er 𝑊) |
28 | 18 | ad2antrl 728 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑔) ++ 𝐵)) |
29 | 24 | simp3bi 1149 |
. . . . . . . 8
⊢ (𝑔𝐿ℎ → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)) |
30 | 29 | ad2antll 729 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑔) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)) |
31 | 27, 28, 30 | ertrd 8407 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵)) |
32 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 19144 |
. . . . . 6
⊢ (𝑓𝐿ℎ ↔ (𝑓 ∈ 𝑊 ∧ ℎ ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ ℎ) ++ 𝐵))) |
33 | 23, 26, 31, 32 | syl3anbrc 1345 |
. . . . 5
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ (𝑓𝐿𝑔 ∧ 𝑔𝐿ℎ)) → 𝑓𝐿ℎ) |
34 | 16 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ∼ Er 𝑊) |
35 | | fviss 6788 |
. . . . . . . . . . . . . 14
⊢ ( I
‘Word (𝐼 ×
2o)) ⊆ Word (𝐼 × 2o) |
36 | 1, 35 | eqsstri 3935 |
. . . . . . . . . . . . 13
⊢ 𝑊 ⊆ Word (𝐼 × 2o) |
37 | | simpll 767 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐴 ∈ 𝑊) |
38 | 36, 37 | sseldi 3899 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐴 ∈ Word (𝐼 × 2o)) |
39 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑓 ∈ 𝑊) |
40 | 36, 39 | sseldi 3899 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑓 ∈ Word (𝐼 × 2o)) |
41 | | ccatcl 14129 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ 𝑓 ∈ Word (𝐼 × 2o)) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o)) |
42 | 38, 40, 41 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o)) |
43 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐵 ∈ 𝑊) |
44 | 36, 43 | sseldi 3899 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝐵 ∈ Word (𝐼 × 2o)) |
45 | | ccatcl 14129 |
. . . . . . . . . . 11
⊢ (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2o)) |
46 | 42, 44, 45 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ Word (𝐼 × 2o)) |
47 | 1 | efgrcl 19105 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑊 → (𝐼 ∈ V ∧ 𝑊 = Word (𝐼 × 2o))) |
48 | 47 | simprd 499 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑊 → 𝑊 = Word (𝐼 × 2o)) |
49 | 48 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → 𝑊 = Word (𝐼 × 2o)) |
50 | 46, 49 | eleqtrrd 2841 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊) |
51 | 34, 50 | erref 8411 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) |
52 | 51 | ex 416 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))) |
53 | 52 | pm4.71d 565 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)))) |
54 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 19144 |
. . . . . . 7
⊢ (𝑓𝐿𝑓 ↔ (𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))) |
55 | | df-3an 1091 |
. . . . . . 7
⊢ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))) |
56 | | anidm 568 |
. . . . . . . 8
⊢ ((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ↔ 𝑓 ∈ 𝑊) |
57 | 56 | anbi1i 627 |
. . . . . . 7
⊢ (((𝑓 ∈ 𝑊 ∧ 𝑓 ∈ 𝑊) ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵)) ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))) |
58 | 54, 55, 57 | 3bitri 300 |
. . . . . 6
⊢ (𝑓𝐿𝑓 ↔ (𝑓 ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ 𝑓) ++ 𝐵))) |
59 | 53, 58 | bitr4di 292 |
. . . . 5
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝑓 ∈ 𝑊 ↔ 𝑓𝐿𝑓)) |
60 | 8, 22, 33, 59 | iserd 8417 |
. . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 Er 𝑊) |
61 | 1, 2, 3, 4 | efgtf 19112 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝑊 → ((𝑇‘𝑓) = (𝑎 ∈ (0...(♯‘𝑓)), 𝑏 ∈ (𝐼 × 2o) ↦ (𝑓 splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∧ (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊)) |
62 | 61 | simprd 499 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝑊 → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊) |
63 | 62 | adantl 485 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊) |
64 | | ffn 6545 |
. . . . . . . 8
⊢ ((𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊 → (𝑇‘𝑓) Fn ((0...(♯‘𝑓)) × (𝐼 × 2o))) |
65 | | ovelrn 7384 |
. . . . . . . 8
⊢ ((𝑇‘𝑓) Fn ((0...(♯‘𝑓)) × (𝐼 × 2o)) → (𝑎 ∈ ran (𝑇‘𝑓) ↔ ∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢))) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑎 ∈ ran (𝑇‘𝑓) ↔ ∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢))) |
67 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓 ∈ 𝑊) |
68 | 62 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑇‘𝑓):((0...(♯‘𝑓)) × (𝐼 × 2o))⟶𝑊) |
69 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈
(0...(♯‘𝑓))) |
70 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑢 ∈ (𝐼 × 2o)) |
71 | 68, 69, 70 | fovrnd 7380 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) ∈ 𝑊) |
72 | 50 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊) |
73 | 37 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐴 ∈ 𝑊) |
74 | 36, 73 | sseldi 3899 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐴 ∈ Word (𝐼 × 2o)) |
75 | 40 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓 ∈ Word (𝐼 × 2o)) |
76 | | pfxcl 14242 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) |
78 | | ccatcl 14129 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) → (𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o)) |
79 | 74, 77, 78 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o)) |
80 | 3 | efgmf 19103 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑀:(𝐼 × 2o)⟶(𝐼 ×
2o) |
81 | 80 | ffvelrni 6903 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ (𝐼 × 2o) → (𝑀‘𝑢) ∈ (𝐼 × 2o)) |
82 | 81 | ad2antll 729 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑀‘𝑢) ∈ (𝐼 × 2o)) |
83 | 70, 82 | s2cld 14436 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
〈“𝑢(𝑀‘𝑢)”〉 ∈ Word (𝐼 × 2o)) |
84 | | ccatcl 14129 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) ∧
〈“𝑢(𝑀‘𝑢)”〉 ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ∈ Word (𝐼 ×
2o)) |
85 | 79, 83, 84 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ∈ Word (𝐼 ×
2o)) |
86 | | swrdcl 14210 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 substr 〈𝑐, (♯‘𝑓)〉) ∈ Word (𝐼 × 2o)) |
87 | 75, 86 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 substr 〈𝑐, (♯‘𝑓)〉) ∈ Word (𝐼 × 2o)) |
88 | 44 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝐵 ∈ Word (𝐼 × 2o)) |
89 | | ccatass 14145 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ∈ Word (𝐼 × 2o) ∧
(𝑓 substr 〈𝑐, (♯‘𝑓)〉) ∈ Word (𝐼 × 2o) ∧
𝐵 ∈ Word (𝐼 × 2o)) →
((((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ ((𝑓 substr 〈𝑐, (♯‘𝑓)〉) ++ 𝐵))) |
90 | 85, 87, 88, 89 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ ((𝑓 substr 〈𝑐, (♯‘𝑓)〉) ++ 𝐵))) |
91 | | ccatcl 14129 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧
〈“𝑢(𝑀‘𝑢)”〉 ∈ Word (𝐼 × 2o)) → ((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉) ∈ Word (𝐼 ×
2o)) |
92 | 77, 83, 91 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉) ∈ Word (𝐼 ×
2o)) |
93 | | ccatass 14145 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ ((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉) ∈ Word (𝐼 × 2o) ∧
(𝑓 substr 〈𝑐, (♯‘𝑓)〉) ∈ Word (𝐼 × 2o)) →
((𝐴 ++ ((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉)) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)))) |
94 | 74, 92, 87, 93 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ ((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉)) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)))) |
95 | | ccatass 14145 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧
〈“𝑢(𝑀‘𝑢)”〉 ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉))) |
96 | 74, 77, 83, 95 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉))) |
97 | 96 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) = ((𝐴 ++ ((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉)) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉))) |
98 | 1, 2, 3, 4 | efgtval 19113 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ 𝑊 ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o)) → (𝑐(𝑇‘𝑓)𝑢) = (𝑓 splice 〈𝑐, 𝑐, 〈“𝑢(𝑀‘𝑢)”〉〉)) |
99 | 67, 69, 70, 98 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) = (𝑓 splice 〈𝑐, 𝑐, 〈“𝑢(𝑀‘𝑢)”〉〉)) |
100 | | splval 14316 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ 𝑊 ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑐 ∈ (0...(♯‘𝑓)) ∧ 〈“𝑢(𝑀‘𝑢)”〉 ∈ Word (𝐼 × 2o))) → (𝑓 splice 〈𝑐, 𝑐, 〈“𝑢(𝑀‘𝑢)”〉〉) = (((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉))) |
101 | 67, 69, 69, 83, 100 | syl13anc 1374 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 splice 〈𝑐, 𝑐, 〈“𝑢(𝑀‘𝑢)”〉〉) = (((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉))) |
102 | 99, 101 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐(𝑇‘𝑓)𝑢) = (((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉))) |
103 | 102 | oveq2d 7229 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) = (𝐴 ++ (((𝑓 prefix 𝑐) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)))) |
104 | 94, 97, 103 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉))) |
105 | 104 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) = ((((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) ++ 𝐵)) |
106 | | lencl 14088 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈ Word (𝐼 × 2o) →
(♯‘𝐴) ∈
ℕ0) |
107 | 74, 106 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘𝐴) ∈
ℕ0) |
108 | | nn0uz 12476 |
. . . . . . . . . . . . . . . . . 18
⊢
ℕ0 = (ℤ≥‘0) |
109 | 107, 108 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘𝐴) ∈
(ℤ≥‘0)) |
110 | | elfznn0 13205 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ∈
(0...(♯‘𝑓))
→ 𝑐 ∈
ℕ0) |
111 | 110 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈
ℕ0) |
112 | | uzaddcl 12500 |
. . . . . . . . . . . . . . . . 17
⊢
(((♯‘𝐴)
∈ (ℤ≥‘0) ∧ 𝑐 ∈ ℕ0) →
((♯‘𝐴) + 𝑐) ∈
(ℤ≥‘0)) |
113 | 109, 111,
112 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
((♯‘𝐴) + 𝑐) ∈
(ℤ≥‘0)) |
114 | 42 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o)) |
115 | | ccatlen 14130 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ++ 𝑓) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) →
(♯‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵))) |
116 | 114, 88, 115 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘((𝐴 ++ 𝑓) ++ 𝐵)) = ((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵))) |
117 | | ccatlen 14130 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ 𝑓 ∈ Word (𝐼 × 2o)) →
(♯‘(𝐴 ++ 𝑓)) = ((♯‘𝐴) + (♯‘𝑓))) |
118 | 74, 75, 117 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘(𝐴 ++ 𝑓)) = ((♯‘𝐴) + (♯‘𝑓))) |
119 | | elfzuz3 13109 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 ∈
(0...(♯‘𝑓))
→ (♯‘𝑓)
∈ (ℤ≥‘𝑐)) |
120 | 119 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘𝑓) ∈
(ℤ≥‘𝑐)) |
121 | 107 | nn0zd 12280 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘𝐴) ∈
ℤ) |
122 | | eluzadd 12469 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((♯‘𝑓)
∈ (ℤ≥‘𝑐) ∧ (♯‘𝐴) ∈ ℤ) →
((♯‘𝑓) +
(♯‘𝐴)) ∈
(ℤ≥‘(𝑐 + (♯‘𝐴)))) |
123 | 120, 121,
122 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
((♯‘𝑓) +
(♯‘𝐴)) ∈
(ℤ≥‘(𝑐 + (♯‘𝐴)))) |
124 | | lencl 14088 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ Word (𝐼 × 2o) →
(♯‘𝑓) ∈
ℕ0) |
125 | 75, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘𝑓) ∈
ℕ0) |
126 | 125 | nn0cnd 12152 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘𝑓) ∈
ℂ) |
127 | 107 | nn0cnd 12152 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘𝐴) ∈
ℂ) |
128 | 126, 127 | addcomd 11034 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
((♯‘𝑓) +
(♯‘𝐴)) =
((♯‘𝐴) +
(♯‘𝑓))) |
129 | 111 | nn0cnd 12152 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑐 ∈
ℂ) |
130 | 129, 127 | addcomd 11034 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑐 + (♯‘𝐴)) = ((♯‘𝐴) + 𝑐)) |
131 | 130 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(ℤ≥‘(𝑐 + (♯‘𝐴))) =
(ℤ≥‘((♯‘𝐴) + 𝑐))) |
132 | 123, 128,
131 | 3eltr3d 2852 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
((♯‘𝐴) +
(♯‘𝑓)) ∈
(ℤ≥‘((♯‘𝐴) + 𝑐))) |
133 | 118, 132 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘(𝐴 ++ 𝑓)) ∈
(ℤ≥‘((♯‘𝐴) + 𝑐))) |
134 | | lencl 14088 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ Word (𝐼 × 2o) →
(♯‘𝐵) ∈
ℕ0) |
135 | 88, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘𝐵) ∈
ℕ0) |
136 | | uzaddcl 12500 |
. . . . . . . . . . . . . . . . . 18
⊢
(((♯‘(𝐴
++ 𝑓)) ∈
(ℤ≥‘((♯‘𝐴) + 𝑐)) ∧ (♯‘𝐵) ∈ ℕ0) →
((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)) ∈
(ℤ≥‘((♯‘𝐴) + 𝑐))) |
137 | 133, 135,
136 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
((♯‘(𝐴 ++ 𝑓)) + (♯‘𝐵)) ∈
(ℤ≥‘((♯‘𝐴) + 𝑐))) |
138 | 116, 137 | eqeltrd 2838 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘((𝐴 ++ 𝑓) ++ 𝐵)) ∈
(ℤ≥‘((♯‘𝐴) + 𝑐))) |
139 | | elfzuzb 13106 |
. . . . . . . . . . . . . . . 16
⊢
(((♯‘𝐴)
+ 𝑐) ∈
(0...(♯‘((𝐴 ++
𝑓) ++ 𝐵))) ↔ (((♯‘𝐴) + 𝑐) ∈ (ℤ≥‘0)
∧ (♯‘((𝐴 ++
𝑓) ++ 𝐵)) ∈
(ℤ≥‘((♯‘𝐴) + 𝑐)))) |
140 | 113, 138,
139 | sylanbrc 586 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
((♯‘𝐴) + 𝑐) ∈
(0...(♯‘((𝐴 ++
𝑓) ++ 𝐵)))) |
141 | 1, 2, 3, 4 | efgtval 19113 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((♯‘𝐴) + 𝑐) ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2o)) →
(((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice 〈((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), 〈“𝑢(𝑀‘𝑢)”〉〉)) |
142 | 72, 140, 70, 141 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ 𝑓) ++ 𝐵) splice 〈((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), 〈“𝑢(𝑀‘𝑢)”〉〉)) |
143 | | wrd0 14094 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ Word (𝐼 ×
2o) |
144 | 143 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ∅
∈ Word (𝐼 ×
2o)) |
145 | | ccatcl 14129 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓 substr 〈𝑐, (♯‘𝑓)〉) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → ((𝑓 substr 〈𝑐, (♯‘𝑓)〉) ++ 𝐵) ∈ Word (𝐼 × 2o)) |
146 | 87, 88, 145 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 substr 〈𝑐, (♯‘𝑓)〉) ++ 𝐵) ∈ Word (𝐼 × 2o)) |
147 | | ccatrid 14144 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) = (𝐴 ++ (𝑓 prefix 𝑐))) |
148 | 79, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) = (𝐴 ++ (𝑓 prefix 𝑐))) |
149 | 148 | oveq1d 7228 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) ++ ((𝑓 substr 〈𝑐, (♯‘𝑓)〉) ++ 𝐵)) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr 〈𝑐, (♯‘𝑓)〉) ++ 𝐵))) |
150 | | ccatass 14145 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ++ (𝑓 prefix 𝑐)) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr 〈𝑐, (♯‘𝑓)〉) ∈ Word (𝐼 × 2o) ∧ 𝐵 ∈ Word (𝐼 × 2o)) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) ++ 𝐵) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr 〈𝑐, (♯‘𝑓)〉) ++ 𝐵))) |
151 | 79, 87, 88, 150 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) ++ 𝐵) = ((𝐴 ++ (𝑓 prefix 𝑐)) ++ ((𝑓 substr 〈𝑐, (♯‘𝑓)〉) ++ 𝐵))) |
152 | | ccatass 14145 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o) ∧ (𝑓 substr 〈𝑐, (♯‘𝑓)〉) ∈ Word (𝐼 × 2o)) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)))) |
153 | 74, 77, 87, 152 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) = (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)))) |
154 | 125, 108 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘𝑓) ∈
(ℤ≥‘0)) |
155 | | eluzfz2 13120 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((♯‘𝑓)
∈ (ℤ≥‘0) → (♯‘𝑓) ∈
(0...(♯‘𝑓))) |
156 | 154, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘𝑓) ∈
(0...(♯‘𝑓))) |
157 | | ccatpfx 14266 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑓 ∈ Word (𝐼 × 2o) ∧ 𝑐 ∈
(0...(♯‘𝑓))
∧ (♯‘𝑓)
∈ (0...(♯‘𝑓))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) = (𝑓 prefix (♯‘𝑓))) |
158 | 75, 69, 156, 157 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) = (𝑓 prefix (♯‘𝑓))) |
159 | | pfxid 14249 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ Word (𝐼 × 2o) → (𝑓 prefix (♯‘𝑓)) = 𝑓) |
160 | 75, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑓 prefix (♯‘𝑓)) = 𝑓) |
161 | 158, 160 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝑓 prefix 𝑐) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) = 𝑓) |
162 | 161 | oveq2d 7229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝐴 ++ ((𝑓 prefix 𝑐) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉))) = (𝐴 ++ 𝑓)) |
163 | 153, 162 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) = (𝐴 ++ 𝑓)) |
164 | 163 | oveq1d 7228 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ (𝑓 prefix 𝑐)) ++ (𝑓 substr 〈𝑐, (♯‘𝑓)〉)) ++ 𝐵) = ((𝐴 ++ 𝑓) ++ 𝐵)) |
165 | 149, 151,
164 | 3eqtr2rd 2784 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ ∅) ++ ((𝑓 substr 〈𝑐, (♯‘𝑓)〉) ++ 𝐵))) |
166 | | ccatlen 14130 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Word (𝐼 × 2o) ∧ (𝑓 prefix 𝑐) ∈ Word (𝐼 × 2o)) →
(♯‘(𝐴 ++ (𝑓 prefix 𝑐))) = ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐)))) |
167 | 74, 77, 166 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘(𝐴 ++ (𝑓 prefix 𝑐))) = ((♯‘𝐴) + (♯‘(𝑓 prefix 𝑐)))) |
168 | | pfxlen 14248 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ Word (𝐼 × 2o) ∧ 𝑐 ∈
(0...(♯‘𝑓)))
→ (♯‘(𝑓
prefix 𝑐)) = 𝑐) |
169 | 75, 69, 168 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(♯‘(𝑓 prefix
𝑐)) = 𝑐) |
170 | 169 | oveq2d 7229 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
((♯‘𝐴) +
(♯‘(𝑓 prefix
𝑐))) =
((♯‘𝐴) + 𝑐)) |
171 | 167, 170 | eqtr2d 2778 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
((♯‘𝐴) + 𝑐) = (♯‘(𝐴 ++ (𝑓 prefix 𝑐)))) |
172 | | hash0 13934 |
. . . . . . . . . . . . . . . . 17
⊢
(♯‘∅) = 0 |
173 | 172 | oveq2i 7224 |
. . . . . . . . . . . . . . . 16
⊢
(((♯‘𝐴)
+ 𝑐) +
(♯‘∅)) = (((♯‘𝐴) + 𝑐) + 0) |
174 | 107, 111 | nn0addcld 12154 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
((♯‘𝐴) + 𝑐) ∈
ℕ0) |
175 | 174 | nn0cnd 12152 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
((♯‘𝐴) + 𝑐) ∈
ℂ) |
176 | 175 | addid1d 11032 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(((♯‘𝐴) + 𝑐) + 0) = ((♯‘𝐴) + 𝑐)) |
177 | 173, 176 | eqtr2id 2791 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
((♯‘𝐴) + 𝑐) = (((♯‘𝐴) + 𝑐) +
(♯‘∅))) |
178 | 79, 144, 146, 83, 165, 171, 177 | splval2 14322 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (((𝐴 ++ 𝑓) ++ 𝐵) splice 〈((♯‘𝐴) + 𝑐), ((♯‘𝐴) + 𝑐), 〈“𝑢(𝑀‘𝑢)”〉〉) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ ((𝑓 substr 〈𝑐, (♯‘𝑓)〉) ++ 𝐵))) |
179 | 142, 178 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) = (((𝐴 ++ (𝑓 prefix 𝑐)) ++ 〈“𝑢(𝑀‘𝑢)”〉) ++ ((𝑓 substr 〈𝑐, (♯‘𝑓)〉) ++ 𝐵))) |
180 | 90, 105, 179 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) = (((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢)) |
181 | 1, 2, 3, 4 | efgtf 19112 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) = (𝑎 ∈ (0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))), 𝑏 ∈ (𝐼 × 2o) ↦ (((𝐴 ++ 𝑓) ++ 𝐵) splice 〈𝑎, 𝑎, 〈“𝑏(𝑀‘𝑏)”〉〉)) ∧ (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊)) |
182 | 181 | simprd 499 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊) |
183 | | ffn 6545 |
. . . . . . . . . . . . . 14
⊢ ((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)):((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))⟶𝑊 → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))) |
184 | 72, 182, 183 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o))) |
185 | | fnovrn 7383 |
. . . . . . . . . . . . 13
⊢ (((𝑇‘((𝐴 ++ 𝑓) ++ 𝐵)) Fn ((0...(♯‘((𝐴 ++ 𝑓) ++ 𝐵))) × (𝐼 × 2o)) ∧
((♯‘𝐴) + 𝑐) ∈
(0...(♯‘((𝐴 ++
𝑓) ++ 𝐵))) ∧ 𝑢 ∈ (𝐼 × 2o)) →
(((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) |
186 | 184, 140,
70, 185 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) →
(((♯‘𝐴) + 𝑐)(𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))𝑢) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) |
187 | 180, 186 | eqeltrd 2838 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) |
188 | 1, 2, 3, 4 | efgi2 19115 |
. . . . . . . . . . 11
⊢ ((((𝐴 ++ 𝑓) ++ 𝐵) ∈ 𝑊 ∧ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵) ∈ ran (𝑇‘((𝐴 ++ 𝑓) ++ 𝐵))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵)) |
189 | 72, 187, 188 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵)) |
190 | 1, 2, 3, 4, 9, 10,
6 | efgcpbllema 19144 |
. . . . . . . . . 10
⊢ (𝑓𝐿(𝑐(𝑇‘𝑓)𝑢) ↔ (𝑓 ∈ 𝑊 ∧ (𝑐(𝑇‘𝑓)𝑢) ∈ 𝑊 ∧ ((𝐴 ++ 𝑓) ++ 𝐵) ∼ ((𝐴 ++ (𝑐(𝑇‘𝑓)𝑢)) ++ 𝐵))) |
191 | 67, 71, 189, 190 | syl3anbrc 1345 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢)) |
192 | | vex 3412 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
193 | | vex 3412 |
. . . . . . . . . . 11
⊢ 𝑓 ∈ V |
194 | 192, 193 | elec 8435 |
. . . . . . . . . 10
⊢ (𝑎 ∈ [𝑓]𝐿 ↔ 𝑓𝐿𝑎) |
195 | | breq2 5057 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → (𝑓𝐿𝑎 ↔ 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢))) |
196 | 194, 195 | syl5bb 286 |
. . . . . . . . 9
⊢ (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → (𝑎 ∈ [𝑓]𝐿 ↔ 𝑓𝐿(𝑐(𝑇‘𝑓)𝑢))) |
197 | 191, 196 | syl5ibrcom 250 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) ∧ (𝑐 ∈ (0...(♯‘𝑓)) ∧ 𝑢 ∈ (𝐼 × 2o))) → (𝑎 = (𝑐(𝑇‘𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿)) |
198 | 197 | rexlimdvva 3213 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (∃𝑐 ∈ (0...(♯‘𝑓))∃𝑢 ∈ (𝐼 × 2o)𝑎 = (𝑐(𝑇‘𝑓)𝑢) → 𝑎 ∈ [𝑓]𝐿)) |
199 | 66, 198 | sylbid 243 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → (𝑎 ∈ ran (𝑇‘𝑓) → 𝑎 ∈ [𝑓]𝐿)) |
200 | 199 | ssrdv 3907 |
. . . . 5
⊢ (((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) ∧ 𝑓 ∈ 𝑊) → ran (𝑇‘𝑓) ⊆ [𝑓]𝐿) |
201 | 200 | ralrimiva 3105 |
. . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿) |
202 | 1 | fvexi 6731 |
. . . . . 6
⊢ 𝑊 ∈ V |
203 | | erex 8415 |
. . . . . 6
⊢ (𝐿 Er 𝑊 → (𝑊 ∈ V → 𝐿 ∈ V)) |
204 | 60, 202, 203 | mpisyl 21 |
. . . . 5
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 ∈ V) |
205 | | ereq1 8398 |
. . . . . . 7
⊢ (𝑟 = 𝐿 → (𝑟 Er 𝑊 ↔ 𝐿 Er 𝑊)) |
206 | | eceq2 8431 |
. . . . . . . . 9
⊢ (𝑟 = 𝐿 → [𝑓]𝑟 = [𝑓]𝐿) |
207 | 206 | sseq2d 3933 |
. . . . . . . 8
⊢ (𝑟 = 𝐿 → (ran (𝑇‘𝑓) ⊆ [𝑓]𝑟 ↔ ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)) |
208 | 207 | ralbidv 3118 |
. . . . . . 7
⊢ (𝑟 = 𝐿 → (∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟 ↔ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿)) |
209 | 205, 208 | anbi12d 634 |
. . . . . 6
⊢ (𝑟 = 𝐿 → ((𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟) ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))) |
210 | 209 | elabg 3585 |
. . . . 5
⊢ (𝐿 ∈ V → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))) |
211 | 204, 210 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ↔ (𝐿 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝐿))) |
212 | 60, 201, 211 | mpbir2and 713 |
. . 3
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → 𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)}) |
213 | | intss1 4874 |
. . 3
⊢ (𝐿 ∈ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿) |
214 | 212, 213 | syl 17 |
. 2
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∩ {𝑟 ∣ (𝑟 Er 𝑊 ∧ ∀𝑓 ∈ 𝑊 ran (𝑇‘𝑓) ⊆ [𝑓]𝑟)} ⊆ 𝐿) |
215 | 5, 214 | eqsstrid 3949 |
1
⊢ ((𝐴 ∈ 𝑊 ∧ 𝐵 ∈ 𝑊) → ∼ ⊆ 𝐿) |