Step | Hyp | Ref
| Expression |
1 | | gsumwrd2dccatlem.f |
. . . 4
⊢ 𝐹 = (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ 〈((1st
‘𝑎) ++
(2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉) |
2 | | sneq 4640 |
. . . . . . . . 9
⊢ (𝑤 = ((1st ‘𝑎) ++ (2nd
‘𝑎)) → {𝑤} = {((1st
‘𝑎) ++
(2nd ‘𝑎))}) |
3 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑤 = ((1st ‘𝑎) ++ (2nd
‘𝑎)) →
(♯‘𝑤) =
(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎)))) |
4 | 3 | oveq2d 7446 |
. . . . . . . . 9
⊢ (𝑤 = ((1st ‘𝑎) ++ (2nd
‘𝑎)) →
(0...(♯‘𝑤)) =
(0...(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎))))) |
5 | 2, 4 | xpeq12d 5719 |
. . . . . . . 8
⊢ (𝑤 = ((1st ‘𝑎) ++ (2nd
‘𝑎)) → ({𝑤} ×
(0...(♯‘𝑤))) =
({((1st ‘𝑎) ++ (2nd ‘𝑎))} ×
(0...(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎)))))) |
6 | 5 | eleq2d 2824 |
. . . . . . 7
⊢ (𝑤 = ((1st ‘𝑎) ++ (2nd
‘𝑎)) →
(〈((1st ‘𝑎) ++ (2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉 ∈ ({𝑤} × (0...(♯‘𝑤))) ↔
〈((1st ‘𝑎) ++ (2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉 ∈ ({((1st
‘𝑎) ++
(2nd ‘𝑎))}
× (0...(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎))))))) |
7 | | xp1st 8044 |
. . . . . . . . 9
⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1st ‘𝑎) ∈ Word 𝐴) |
8 | 7 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐴) |
9 | | xp2nd 8045 |
. . . . . . . . 9
⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (2nd ‘𝑎) ∈ Word 𝐴) |
10 | 9 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐴) |
11 | | ccatcl 14608 |
. . . . . . . 8
⊢
(((1st ‘𝑎) ∈ Word 𝐴 ∧ (2nd ‘𝑎) ∈ Word 𝐴) → ((1st ‘𝑎) ++ (2nd
‘𝑎)) ∈ Word
𝐴) |
12 | 8, 10, 11 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((1st ‘𝑎) ++ (2nd
‘𝑎)) ∈ Word
𝐴) |
13 | | ovex 7463 |
. . . . . . . . . 10
⊢
((1st ‘𝑎) ++ (2nd ‘𝑎)) ∈ V |
14 | 13 | snid 4666 |
. . . . . . . . 9
⊢
((1st ‘𝑎) ++ (2nd ‘𝑎)) ∈ {((1st
‘𝑎) ++
(2nd ‘𝑎))} |
15 | 14 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((1st ‘𝑎) ++ (2nd
‘𝑎)) ∈
{((1st ‘𝑎)
++ (2nd ‘𝑎))}) |
16 | | 0zd 12622 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ∈ ℤ) |
17 | | lencl 14567 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑎) ++ (2nd ‘𝑎)) ∈ Word 𝐴 → (♯‘((1st
‘𝑎) ++
(2nd ‘𝑎)))
∈ ℕ0) |
18 | 12, 17 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1st
‘𝑎) ++
(2nd ‘𝑎)))
∈ ℕ0) |
19 | 18 | nn0zd 12636 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1st
‘𝑎) ++
(2nd ‘𝑎)))
∈ ℤ) |
20 | | lencl 14567 |
. . . . . . . . . . 11
⊢
((1st ‘𝑎) ∈ Word 𝐴 → (♯‘(1st
‘𝑎)) ∈
ℕ0) |
21 | 8, 20 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1st
‘𝑎)) ∈
ℕ0) |
22 | 21 | nn0zd 12636 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1st
‘𝑎)) ∈
ℤ) |
23 | 21 | nn0ge0d 12587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ≤
(♯‘(1st ‘𝑎))) |
24 | | lencl 14567 |
. . . . . . . . . . . . 13
⊢
((2nd ‘𝑎) ∈ Word 𝐴 → (♯‘(2nd
‘𝑎)) ∈
ℕ0) |
25 | 10, 24 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(2nd
‘𝑎)) ∈
ℕ0) |
26 | 25 | nn0ge0d 12587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ≤
(♯‘(2nd ‘𝑎))) |
27 | 21 | nn0red 12585 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1st
‘𝑎)) ∈
ℝ) |
28 | 25 | nn0red 12585 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(2nd
‘𝑎)) ∈
ℝ) |
29 | 27, 28 | addge01d 11848 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (0 ≤
(♯‘(2nd ‘𝑎)) ↔ (♯‘(1st
‘𝑎)) ≤
((♯‘(1st ‘𝑎)) + (♯‘(2nd
‘𝑎))))) |
30 | 26, 29 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1st
‘𝑎)) ≤
((♯‘(1st ‘𝑎)) + (♯‘(2nd
‘𝑎)))) |
31 | | ccatlen 14609 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑎) ∈ Word 𝐴 ∧ (2nd ‘𝑎) ∈ Word 𝐴) → (♯‘((1st
‘𝑎) ++
(2nd ‘𝑎)))
= ((♯‘(1st ‘𝑎)) + (♯‘(2nd
‘𝑎)))) |
32 | 8, 10, 31 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1st
‘𝑎) ++
(2nd ‘𝑎)))
= ((♯‘(1st ‘𝑎)) + (♯‘(2nd
‘𝑎)))) |
33 | 30, 32 | breqtrrd 5175 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1st
‘𝑎)) ≤
(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎)))) |
34 | 16, 19, 22, 23, 33 | elfzd 13551 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1st
‘𝑎)) ∈
(0...(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎))))) |
35 | 15, 34 | opelxpd 5727 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 〈((1st
‘𝑎) ++
(2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉 ∈ ({((1st
‘𝑎) ++
(2nd ‘𝑎))}
× (0...(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎)))))) |
36 | 6, 12, 35 | rspcedvdw 3624 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤 ∈ Word 𝐴〈((1st ‘𝑎) ++ (2nd
‘𝑎)),
(♯‘(1st ‘𝑎))〉 ∈ ({𝑤} × (0...(♯‘𝑤)))) |
37 | 36 | eliund 5002 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 〈((1st
‘𝑎) ++
(2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))) |
38 | | gsumwrd2dccatlem.u |
. . . . 5
⊢ 𝑈 = ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) |
39 | 37, 38 | eleqtrrdi 2849 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 〈((1st
‘𝑎) ++
(2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉 ∈ 𝑈) |
40 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) |
41 | | xp1st 8044 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) → (1st
‘𝑏) ∈ {𝑢}) |
42 | | elsni 4647 |
. . . . . . . . . 10
⊢
((1st ‘𝑏) ∈ {𝑢} → (1st ‘𝑏) = 𝑢) |
43 | 40, 41, 42 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1st
‘𝑏) = 𝑢) |
44 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → 𝑢 ∈ Word 𝐴) |
45 | 43, 44 | eqeltrd 2838 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1st
‘𝑏) ∈ Word 𝐴) |
46 | 45 | adantllr 719 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1st
‘𝑏) ∈ Word 𝐴) |
47 | 38 | eleq2i 2830 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪
𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))) |
48 | 47 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝑈 → 𝑏 ∈ ∪
𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))) |
49 | 48 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ ∪
𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))) |
50 | | eliun 4999 |
. . . . . . . . 9
⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤)))) |
51 | 49, 50 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤)))) |
52 | | sneq 4640 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → {𝑢} = {𝑤}) |
53 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → (♯‘𝑢) = (♯‘𝑤)) |
54 | 53 | oveq2d 7446 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → (0...(♯‘𝑢)) = (0...(♯‘𝑤))) |
55 | 52, 54 | xpeq12d 5719 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑤 → ({𝑢} × (0...(♯‘𝑢))) = ({𝑤} × (0...(♯‘𝑤)))) |
56 | 55 | eleq2d 2824 |
. . . . . . . . 9
⊢ (𝑢 = 𝑤 → (𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) ↔ 𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))) |
57 | 56 | cbvrexvw 3235 |
. . . . . . . 8
⊢
(∃𝑢 ∈
Word 𝐴𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) ↔ ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤)))) |
58 | 51, 57 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∃𝑢 ∈ Word 𝐴𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) |
59 | 46, 58 | r19.29a 3159 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (1st ‘𝑏) ∈ Word 𝐴) |
60 | | pfxcl 14711 |
. . . . . 6
⊢
((1st ‘𝑏) ∈ Word 𝐴 → ((1st ‘𝑏) prefix (2nd
‘𝑏)) ∈ Word
𝐴) |
61 | 59, 60 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ((1st ‘𝑏) prefix (2nd
‘𝑏)) ∈ Word
𝐴) |
62 | | swrdcl 14679 |
. . . . . 6
⊢
((1st ‘𝑏) ∈ Word 𝐴 → ((1st ‘𝑏) substr 〈(2nd
‘𝑏),
(♯‘(1st ‘𝑏))〉) ∈ Word 𝐴) |
63 | 59, 62 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ((1st ‘𝑏) substr 〈(2nd
‘𝑏),
(♯‘(1st ‘𝑏))〉) ∈ Word 𝐴) |
64 | 61, 63 | opelxpd 5727 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 〈((1st ‘𝑏) prefix (2nd
‘𝑏)),
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)〉
∈ (Word 𝐴 × Word
𝐴)) |
65 | 49 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑏 ∈ ∪
𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))) |
66 | | eliunxp 5850 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤∃𝑛(𝑏 = 〈𝑤, 𝑛〉 ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤))))) |
67 | 65, 66 | sylib 218 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤∃𝑛(𝑏 = 〈𝑤, 𝑛〉 ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤))))) |
68 | | opeq1 4877 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑤 → 〈𝑢, 𝑛〉 = 〈𝑤, 𝑛〉) |
69 | 68 | eqeq2d 2745 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → (𝑏 = 〈𝑢, 𝑛〉 ↔ 𝑏 = 〈𝑤, 𝑛〉)) |
70 | | eleq1w 2821 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑤 → (𝑢 ∈ Word 𝐴 ↔ 𝑤 ∈ Word 𝐴)) |
71 | 54 | eleq2d 2824 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑤 → (𝑛 ∈ (0...(♯‘𝑢)) ↔ 𝑛 ∈ (0...(♯‘𝑤)))) |
72 | 70, 71 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → ((𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢))) ↔ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤))))) |
73 | 69, 72 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → ((𝑏 = 〈𝑢, 𝑛〉 ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ (𝑏 = 〈𝑤, 𝑛〉 ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))) |
74 | 73 | exbidv 1918 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑤 → (∃𝑛(𝑏 = 〈𝑢, 𝑛〉 ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ ∃𝑛(𝑏 = 〈𝑤, 𝑛〉 ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))) |
75 | 74 | cbvexvw 2033 |
. . . . . . . . 9
⊢
(∃𝑢∃𝑛(𝑏 = 〈𝑢, 𝑛〉 ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ ∃𝑤∃𝑛(𝑏 = 〈𝑤, 𝑛〉 ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤))))) |
76 | 67, 75 | sylibr 234 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑢∃𝑛(𝑏 = 〈𝑢, 𝑛〉 ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢))))) |
77 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(1st ‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) |
78 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(2nd ‘𝑎) =
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) |
79 | 77, 78 | oveq12d 7448 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
((1st ‘𝑎)
++ (2nd ‘𝑎)) = (((1st ‘𝑏) prefix (2nd
‘𝑏)) ++
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉))) |
80 | | vex 3481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑢 ∈ V |
81 | | vex 3481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑛 ∈ V |
82 | 80, 81 | op1std 8022 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 〈𝑢, 𝑛〉 → (1st ‘𝑏) = 𝑢) |
83 | 82 | ad5antlr 735 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(1st ‘𝑏) =
𝑢) |
84 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
𝑢 ∈ Word 𝐴) |
85 | 83, 84 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(1st ‘𝑏)
∈ Word 𝐴) |
86 | 80, 81 | op2ndd 8023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 〈𝑢, 𝑛〉 → (2nd ‘𝑏) = 𝑛) |
87 | 86 | ad5antlr 735 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(2nd ‘𝑏) =
𝑛) |
88 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
𝑛 ∈
(0...(♯‘𝑢))) |
89 | 83 | eqcomd 2740 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
𝑢 = (1st
‘𝑏)) |
90 | 89 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(♯‘𝑢) =
(♯‘(1st ‘𝑏))) |
91 | 90 | oveq2d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(0...(♯‘𝑢)) =
(0...(♯‘(1st ‘𝑏)))) |
92 | 88, 91 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
𝑛 ∈
(0...(♯‘(1st ‘𝑏)))) |
93 | 87, 92 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(2nd ‘𝑏)
∈ (0...(♯‘(1st ‘𝑏)))) |
94 | | pfxcctswrd 14744 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1st ‘𝑏) ∈ Word 𝐴 ∧ (2nd ‘𝑏) ∈
(0...(♯‘(1st ‘𝑏)))) → (((1st ‘𝑏) prefix (2nd
‘𝑏)) ++
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) =
(1st ‘𝑏)) |
95 | 85, 93, 94 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(((1st ‘𝑏)
prefix (2nd ‘𝑏)) ++ ((1st ‘𝑏) substr 〈(2nd
‘𝑏),
(♯‘(1st ‘𝑏))〉)) = (1st ‘𝑏)) |
96 | 79, 95 | eqtr2d 2775 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(1st ‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) |
97 | 77 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(♯‘(1st ‘𝑎)) = (♯‘((1st
‘𝑏) prefix
(2nd ‘𝑏)))) |
98 | | pfxlen 14717 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1st ‘𝑏) ∈ Word 𝐴 ∧ (2nd ‘𝑏) ∈
(0...(♯‘(1st ‘𝑏)))) → (♯‘((1st
‘𝑏) prefix
(2nd ‘𝑏)))
= (2nd ‘𝑏)) |
99 | 85, 93, 98 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(♯‘((1st ‘𝑏) prefix (2nd ‘𝑏))) = (2nd
‘𝑏)) |
100 | 97, 99 | eqtr2d 2775 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) |
101 | 96, 100 | jca 511 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
((1st ‘𝑏)
= ((1st ‘𝑎) ++ (2nd ‘𝑎)) ∧ (2nd
‘𝑏) =
(♯‘(1st ‘𝑎)))) |
102 | 101 | anasss 466 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ ((1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏)) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉))) →
((1st ‘𝑏)
= ((1st ‘𝑎) ++ (2nd ‘𝑎)) ∧ (2nd
‘𝑏) =
(♯‘(1st ‘𝑎)))) |
103 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → (1st ‘𝑏) = ((1st
‘𝑎) ++
(2nd ‘𝑎))) |
104 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) |
105 | 103, 104 | oveq12d 7448 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → ((1st ‘𝑏) prefix (2nd
‘𝑏)) =
(((1st ‘𝑎)
++ (2nd ‘𝑎)) prefix (♯‘(1st
‘𝑎)))) |
106 | 8 | ad5antr 734 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → (1st ‘𝑎) ∈ Word 𝐴) |
107 | 10 | ad5antr 734 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → (2nd ‘𝑎) ∈ Word 𝐴) |
108 | | pfxccat1 14736 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1st ‘𝑎) ∈ Word 𝐴 ∧ (2nd ‘𝑎) ∈ Word 𝐴) → (((1st ‘𝑎) ++ (2nd
‘𝑎)) prefix
(♯‘(1st ‘𝑎))) = (1st ‘𝑎)) |
109 | 106, 107,
108 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → (((1st ‘𝑎) ++ (2nd
‘𝑎)) prefix
(♯‘(1st ‘𝑎))) = (1st ‘𝑎)) |
110 | 105, 109 | eqtr2d 2775 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → (1st ‘𝑎) = ((1st
‘𝑏) prefix
(2nd ‘𝑏))) |
111 | 103 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → (♯‘(1st
‘𝑏)) =
(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎)))) |
112 | 106, 107,
31 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → (♯‘((1st
‘𝑎) ++
(2nd ‘𝑎)))
= ((♯‘(1st ‘𝑎)) + (♯‘(2nd
‘𝑎)))) |
113 | 111, 112 | eqtrd 2774 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → (♯‘(1st
‘𝑏)) =
((♯‘(1st ‘𝑎)) + (♯‘(2nd
‘𝑎)))) |
114 | 104, 113 | opeq12d 4885 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → 〈(2nd ‘𝑏),
(♯‘(1st ‘𝑏))〉 =
〈(♯‘(1st ‘𝑎)), ((♯‘(1st
‘𝑎)) +
(♯‘(2nd ‘𝑎)))〉) |
115 | 103, 114 | oveq12d 7448 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → ((1st ‘𝑏) substr 〈(2nd
‘𝑏),
(♯‘(1st ‘𝑏))〉) = (((1st ‘𝑎) ++ (2nd
‘𝑎)) substr
〈(♯‘(1st ‘𝑎)), ((♯‘(1st
‘𝑎)) +
(♯‘(2nd ‘𝑎)))〉)) |
116 | | swrdccat2 14703 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1st ‘𝑎) ∈ Word 𝐴 ∧ (2nd ‘𝑎) ∈ Word 𝐴) → (((1st ‘𝑎) ++ (2nd
‘𝑎)) substr
〈(♯‘(1st ‘𝑎)), ((♯‘(1st
‘𝑎)) +
(♯‘(2nd ‘𝑎)))〉) = (2nd ‘𝑎)) |
117 | 106, 107,
116 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → (((1st ‘𝑎) ++ (2nd
‘𝑎)) substr
〈(♯‘(1st ‘𝑎)), ((♯‘(1st
‘𝑎)) +
(♯‘(2nd ‘𝑎)))〉) = (2nd ‘𝑎)) |
118 | 115, 117 | eqtr2d 2775 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) |
119 | 110, 118 | jca 511 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → ((1st ‘𝑎) = ((1st
‘𝑏) prefix
(2nd ‘𝑏))
∧ (2nd ‘𝑎) = ((1st ‘𝑏) substr 〈(2nd
‘𝑏),
(♯‘(1st ‘𝑏))〉))) |
120 | 119 | anasss 466 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ ((1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎)) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎)))) → ((1st ‘𝑎) = ((1st
‘𝑏) prefix
(2nd ‘𝑏))
∧ (2nd ‘𝑎) = ((1st ‘𝑏) substr 〈(2nd
‘𝑏),
(♯‘(1st ‘𝑏))〉))) |
121 | 102, 120 | impbida 801 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) → (((1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏)) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) ↔
((1st ‘𝑏)
= ((1st ‘𝑎) ++ (2nd ‘𝑎)) ∧ (2nd
‘𝑏) =
(♯‘(1st ‘𝑎))))) |
122 | 121 | anasss 466 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) → (((1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏)) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) ↔
((1st ‘𝑏)
= ((1st ‘𝑎) ++ (2nd ‘𝑎)) ∧ (2nd
‘𝑏) =
(♯‘(1st ‘𝑎))))) |
123 | 122 | expl 457 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑏 = 〈𝑢, 𝑛〉 ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) → (((1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏)) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) ↔
((1st ‘𝑏)
= ((1st ‘𝑎) ++ (2nd ‘𝑎)) ∧ (2nd
‘𝑏) =
(♯‘(1st ‘𝑎)))))) |
124 | 123 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((𝑏 = 〈𝑢, 𝑛〉 ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) → (((1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏)) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) ↔
((1st ‘𝑏)
= ((1st ‘𝑎) ++ (2nd ‘𝑎)) ∧ (2nd
‘𝑏) =
(♯‘(1st ‘𝑎)))))) |
125 | 124 | exlimdv 1930 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (∃𝑛(𝑏 = 〈𝑢, 𝑛〉 ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) → (((1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏)) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) ↔
((1st ‘𝑏)
= ((1st ‘𝑎) ++ (2nd ‘𝑎)) ∧ (2nd
‘𝑏) =
(♯‘(1st ‘𝑎)))))) |
126 | 125 | imp 406 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ ∃𝑛(𝑏 = 〈𝑢, 𝑛〉 ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢))))) → (((1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏)) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) ↔
((1st ‘𝑏)
= ((1st ‘𝑎) ++ (2nd ‘𝑎)) ∧ (2nd
‘𝑏) =
(♯‘(1st ‘𝑎))))) |
127 | 76, 126 | exlimddv 1932 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (((1st ‘𝑎) = ((1st
‘𝑏) prefix
(2nd ‘𝑏))
∧ (2nd ‘𝑎) = ((1st ‘𝑏) substr 〈(2nd
‘𝑏),
(♯‘(1st ‘𝑏))〉)) ↔ ((1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎)) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))))) |
128 | | eqop 8054 |
. . . . . . . 8
⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (𝑎 = 〈((1st ‘𝑏) prefix (2nd
‘𝑏)),
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)〉
↔ ((1st ‘𝑎) = ((1st ‘𝑏) prefix (2nd
‘𝑏)) ∧
(2nd ‘𝑎) =
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)))) |
129 | 128 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑎 = 〈((1st ‘𝑏) prefix (2nd
‘𝑏)),
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)〉
↔ ((1st ‘𝑎) = ((1st ‘𝑏) prefix (2nd
‘𝑏)) ∧
(2nd ‘𝑎) =
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)))) |
130 | | snssi 4812 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ Word 𝐴 → {𝑤} ⊆ Word 𝐴) |
131 | 130 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → {𝑤} ⊆ Word 𝐴) |
132 | | fz0ssnn0 13658 |
. . . . . . . . . . . 12
⊢
(0...(♯‘𝑤)) ⊆
ℕ0 |
133 | | xpss12 5703 |
. . . . . . . . . . . 12
⊢ (({𝑤} ⊆ Word 𝐴 ∧ (0...(♯‘𝑤)) ⊆ ℕ0)
→ ({𝑤} ×
(0...(♯‘𝑤)))
⊆ (Word 𝐴 ×
ℕ0)) |
134 | 131, 132,
133 | sylancl 586 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → ({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 ×
ℕ0)) |
135 | 134 | iunssd 5054 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 ×
ℕ0)) |
136 | 135 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 ×
ℕ0)) |
137 | 136, 65 | sseldd 3995 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑏 ∈ (Word 𝐴 ×
ℕ0)) |
138 | | eqop 8054 |
. . . . . . . 8
⊢ (𝑏 ∈ (Word 𝐴 × ℕ0) → (𝑏 = 〈((1st
‘𝑎) ++
(2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉 ↔ ((1st ‘𝑏) = ((1st
‘𝑎) ++
(2nd ‘𝑎))
∧ (2nd ‘𝑏) = (♯‘(1st
‘𝑎))))) |
139 | 137, 138 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑏 = 〈((1st ‘𝑎) ++ (2nd
‘𝑎)),
(♯‘(1st ‘𝑎))〉 ↔ ((1st ‘𝑏) = ((1st
‘𝑎) ++
(2nd ‘𝑎))
∧ (2nd ‘𝑏) = (♯‘(1st
‘𝑎))))) |
140 | 127, 129,
139 | 3bitr4d 311 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (𝑎 = 〈((1st ‘𝑏) prefix (2nd
‘𝑏)),
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)〉
↔ 𝑏 =
〈((1st ‘𝑎) ++ (2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉)) |
141 | 140 | an32s 652 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 ∈ 𝑈) → (𝑎 = 〈((1st ‘𝑏) prefix (2nd
‘𝑏)),
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)〉
↔ 𝑏 =
〈((1st ‘𝑎) ++ (2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉)) |
142 | 141 | anasss 466 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (Word 𝐴 × Word 𝐴) ∧ 𝑏 ∈ 𝑈)) → (𝑎 = 〈((1st ‘𝑏) prefix (2nd
‘𝑏)),
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)〉
↔ 𝑏 =
〈((1st ‘𝑎) ++ (2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉)) |
143 | 1, 39, 64, 142 | f1ocnv2d 7685 |
. . 3
⊢ (𝜑 → (𝐹:(Word 𝐴 × Word 𝐴)–1-1-onto→𝑈 ∧ ◡𝐹 = (𝑏 ∈ 𝑈 ↦ 〈((1st ‘𝑏) prefix (2nd
‘𝑏)),
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)〉))) |
144 | 143 | simpld 494 |
. 2
⊢ (𝜑 → 𝐹:(Word 𝐴 × Word 𝐴)–1-1-onto→𝑈) |
145 | 143 | simprd 495 |
. . 3
⊢ (𝜑 → ◡𝐹 = (𝑏 ∈ 𝑈 ↦ 〈((1st ‘𝑏) prefix (2nd
‘𝑏)),
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)〉)) |
146 | | gsumwrd2dccatlem.g |
. . 3
⊢ 𝐺 = (𝑏 ∈ 𝑈 ↦ 〈((1st ‘𝑏) prefix (2nd
‘𝑏)),
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)〉) |
147 | 145, 146 | eqtr4di 2792 |
. 2
⊢ (𝜑 → ◡𝐹 = 𝐺) |
148 | 144, 147 | jca 511 |
1
⊢ (𝜑 → (𝐹:(Word 𝐴 × Word 𝐴)–1-1-onto→𝑈 ∧ ◡𝐹 = 𝐺)) |