| Step | Hyp | Ref
| Expression |
| 1 | | gsumwrd2dccatlem.f |
. . . 4
⊢ 𝐹 = (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ 〈((1st
‘𝑎) ++
(2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉) |
| 2 | | sneq 4636 |
. . . . . . . . 9
⊢ (𝑤 = ((1st ‘𝑎) ++ (2nd
‘𝑎)) → {𝑤} = {((1st
‘𝑎) ++
(2nd ‘𝑎))}) |
| 3 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑤 = ((1st ‘𝑎) ++ (2nd
‘𝑎)) →
(♯‘𝑤) =
(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎)))) |
| 4 | 3 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑤 = ((1st ‘𝑎) ++ (2nd
‘𝑎)) →
(0...(♯‘𝑤)) =
(0...(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎))))) |
| 5 | 2, 4 | xpeq12d 5716 |
. . . . . . . 8
⊢ (𝑤 = ((1st ‘𝑎) ++ (2nd
‘𝑎)) → ({𝑤} ×
(0...(♯‘𝑤))) =
({((1st ‘𝑎) ++ (2nd ‘𝑎))} ×
(0...(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎)))))) |
| 6 | 5 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑤 = ((1st ‘𝑎) ++ (2nd
‘𝑎)) →
(〈((1st ‘𝑎) ++ (2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉 ∈ ({𝑤} × (0...(♯‘𝑤))) ↔
〈((1st ‘𝑎) ++ (2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉 ∈ ({((1st
‘𝑎) ++
(2nd ‘𝑎))}
× (0...(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎))))))) |
| 7 | | xp1st 8046 |
. . . . . . . . 9
⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (1st ‘𝑎) ∈ Word 𝐴) |
| 8 | 7 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (1st ‘𝑎) ∈ Word 𝐴) |
| 9 | | xp2nd 8047 |
. . . . . . . . 9
⊢ (𝑎 ∈ (Word 𝐴 × Word 𝐴) → (2nd ‘𝑎) ∈ Word 𝐴) |
| 10 | 9 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (2nd ‘𝑎) ∈ Word 𝐴) |
| 11 | | ccatcl 14612 |
. . . . . . . 8
⊢
(((1st ‘𝑎) ∈ Word 𝐴 ∧ (2nd ‘𝑎) ∈ Word 𝐴) → ((1st ‘𝑎) ++ (2nd
‘𝑎)) ∈ Word
𝐴) |
| 12 | 8, 10, 11 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((1st ‘𝑎) ++ (2nd
‘𝑎)) ∈ Word
𝐴) |
| 13 | | ovex 7464 |
. . . . . . . . . 10
⊢
((1st ‘𝑎) ++ (2nd ‘𝑎)) ∈ V |
| 14 | 13 | snid 4662 |
. . . . . . . . 9
⊢
((1st ‘𝑎) ++ (2nd ‘𝑎)) ∈ {((1st
‘𝑎) ++
(2nd ‘𝑎))} |
| 15 | 14 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ((1st ‘𝑎) ++ (2nd
‘𝑎)) ∈
{((1st ‘𝑎)
++ (2nd ‘𝑎))}) |
| 16 | | 0zd 12625 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ∈ ℤ) |
| 17 | | lencl 14571 |
. . . . . . . . . . 11
⊢
(((1st ‘𝑎) ++ (2nd ‘𝑎)) ∈ Word 𝐴 → (♯‘((1st
‘𝑎) ++
(2nd ‘𝑎)))
∈ ℕ0) |
| 18 | 12, 17 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1st
‘𝑎) ++
(2nd ‘𝑎)))
∈ ℕ0) |
| 19 | 18 | nn0zd 12639 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘((1st
‘𝑎) ++
(2nd ‘𝑎)))
∈ ℤ) |
| 20 | | lencl 14571 |
. . . . . . . . . . 11
⊢
((1st ‘𝑎) ∈ Word 𝐴 → (♯‘(1st
‘𝑎)) ∈
ℕ0) |
| 21 | 8, 20 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1st
‘𝑎)) ∈
ℕ0) |
| 22 | 21 | nn0zd 12639 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1st
‘𝑎)) ∈
ℤ) |
| 23 | 21 | nn0ge0d 12590 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ≤
(♯‘(1st ‘𝑎))) |
| 24 | | lencl 14571 |
. . . . . . . . . . . . 13
⊢
((2nd ‘𝑎) ∈ Word 𝐴 → (♯‘(2nd
‘𝑎)) ∈
ℕ0) |
| 25 | 10, 24 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(2nd
‘𝑎)) ∈
ℕ0) |
| 26 | 25 | nn0ge0d 12590 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 0 ≤
(♯‘(2nd ‘𝑎))) |
| 27 | 21 | nn0red 12588 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1st
‘𝑎)) ∈
ℝ) |
| 28 | 25 | nn0red 12588 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(2nd
‘𝑎)) ∈
ℝ) |
| 29 | 27, 28 | addge01d 11851 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (0 ≤
(♯‘(2nd ‘𝑎)) ↔ (♯‘(1st
‘𝑎)) ≤
((♯‘(1st ‘𝑎)) + (♯‘(2nd
‘𝑎))))) |
| 30 | 26, 29 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1st
‘𝑎)) ≤
((♯‘(1st ‘𝑎)) + (♯‘(2nd
‘𝑎)))) |
| 31 | | ccatlen 14613 |
. . . . . . . . . . 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 5171 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1st
‘𝑎)) ≤
(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎)))) |
| 34 | 16, 19, 22, 23, 33 | elfzd 13555 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (♯‘(1st
‘𝑎)) ∈
(0...(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎))))) |
| 35 | 15, 34 | opelxpd 5724 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 〈((1st
‘𝑎) ++
(2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉 ∈ ({((1st
‘𝑎) ++
(2nd ‘𝑎))}
× (0...(♯‘((1st ‘𝑎) ++ (2nd ‘𝑎)))))) |
| 36 | 6, 12, 35 | rspcedvdw 3625 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤 ∈ Word 𝐴〈((1st ‘𝑎) ++ (2nd
‘𝑎)),
(♯‘(1st ‘𝑎))〉 ∈ ({𝑤} × (0...(♯‘𝑤)))) |
| 37 | 36 | eliund 4998 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 〈((1st
‘𝑎) ++
(2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))) |
| 38 | | gsumwrd2dccatlem.u |
. . . . 5
⊢ 𝑈 = ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) |
| 39 | 37, 38 | eleqtrrdi 2852 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 〈((1st
‘𝑎) ++
(2nd ‘𝑎)),
(♯‘(1st ‘𝑎))〉 ∈ 𝑈) |
| 40 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) |
| 41 | | xp1st 8046 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) → (1st
‘𝑏) ∈ {𝑢}) |
| 42 | | elsni 4643 |
. . . . . . . . . 10
⊢
((1st ‘𝑏) ∈ {𝑢} → (1st ‘𝑏) = 𝑢) |
| 43 | 40, 41, 42 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1st
‘𝑏) = 𝑢) |
| 44 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → 𝑢 ∈ Word 𝐴) |
| 45 | 43, 44 | eqeltrd 2841 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1st
‘𝑏) ∈ Word 𝐴) |
| 46 | 45 | adantllr 719 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) → (1st
‘𝑏) ∈ Word 𝐴) |
| 47 | 38 | eleq2i 2833 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪
𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))) |
| 48 | 47 | biimpi 216 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝑈 → 𝑏 ∈ ∪
𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))) |
| 49 | 48 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 𝑏 ∈ ∪
𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))) |
| 50 | | eliun 4995 |
. . . . . . . . 9
⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤)))) |
| 51 | 49, 50 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤)))) |
| 52 | | sneq 4636 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → {𝑢} = {𝑤}) |
| 53 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → (♯‘𝑢) = (♯‘𝑤)) |
| 54 | 53 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → (0...(♯‘𝑢)) = (0...(♯‘𝑤))) |
| 55 | 52, 54 | xpeq12d 5716 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑤 → ({𝑢} × (0...(♯‘𝑢))) = ({𝑤} × (0...(♯‘𝑤)))) |
| 56 | 55 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑢 = 𝑤 → (𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) ↔ 𝑏 ∈ ({𝑤} × (0...(♯‘𝑤))))) |
| 57 | 56 | cbvrexvw 3238 |
. . . . . . . 8
⊢
(∃𝑢 ∈
Word 𝐴𝑏 ∈ ({𝑢} × (0...(♯‘𝑢))) ↔ ∃𝑤 ∈ Word 𝐴𝑏 ∈ ({𝑤} × (0...(♯‘𝑤)))) |
| 58 | 51, 57 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ∃𝑢 ∈ Word 𝐴𝑏 ∈ ({𝑢} × (0...(♯‘𝑢)))) |
| 59 | 46, 58 | r19.29a 3162 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → (1st ‘𝑏) ∈ Word 𝐴) |
| 60 | | pfxcl 14715 |
. . . . . 6
⊢
((1st ‘𝑏) ∈ Word 𝐴 → ((1st ‘𝑏) prefix (2nd
‘𝑏)) ∈ Word
𝐴) |
| 61 | 59, 60 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ((1st ‘𝑏) prefix (2nd
‘𝑏)) ∈ Word
𝐴) |
| 62 | | swrdcl 14683 |
. . . . . 6
⊢
((1st ‘𝑏) ∈ Word 𝐴 → ((1st ‘𝑏) substr 〈(2nd
‘𝑏),
(♯‘(1st ‘𝑏))〉) ∈ Word 𝐴) |
| 63 | 59, 62 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → ((1st ‘𝑏) substr 〈(2nd
‘𝑏),
(♯‘(1st ‘𝑏))〉) ∈ Word 𝐴) |
| 64 | 61, 63 | opelxpd 5724 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ 𝑈) → 〈((1st ‘𝑏) prefix (2nd
‘𝑏)),
((1st ‘𝑏)
substr 〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)〉
∈ (Word 𝐴 × Word
𝐴)) |
| 65 | 49 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑏 ∈ ∪
𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤)))) |
| 66 | | eliunxp 5848 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ↔ ∃𝑤∃𝑛(𝑏 = 〈𝑤, 𝑛〉 ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤))))) |
| 67 | 65, 66 | sylib 218 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∃𝑤∃𝑛(𝑏 = 〈𝑤, 𝑛〉 ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤))))) |
| 68 | | opeq1 4873 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑤 → 〈𝑢, 𝑛〉 = 〈𝑤, 𝑛〉) |
| 69 | 68 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → (𝑏 = 〈𝑢, 𝑛〉 ↔ 𝑏 = 〈𝑤, 𝑛〉)) |
| 70 | | eleq1w 2824 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑤 → (𝑢 ∈ Word 𝐴 ↔ 𝑤 ∈ Word 𝐴)) |
| 71 | 54 | eleq2d 2827 |
. . . . . . . . . . . . 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 1921 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑤 → (∃𝑛(𝑏 = 〈𝑢, 𝑛〉 ∧ (𝑢 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑢)))) ↔ ∃𝑛(𝑏 = 〈𝑤, 𝑛〉 ∧ (𝑤 ∈ Word 𝐴 ∧ 𝑛 ∈ (0...(♯‘𝑤)))))) |
| 75 | 74 | cbvexvw 2036 |
. . . . . . . . 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 7449 |
. . . . . . . . . . . . . . . . 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 3484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑢 ∈ V |
| 81 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑛 ∈ V |
| 82 | 80, 81 | op1std 8024 |
. . . . . . . . . . . . . . . . . . . 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 2841 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(1st ‘𝑏)
∈ Word 𝐴) |
| 86 | 80, 81 | op2ndd 8025 |
. . . . . . . . . . . . . . . . . . . 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 2743 |
. . . . . . . . . . . . . . . . . . . . . 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 7447 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(0...(♯‘𝑢)) =
(0...(♯‘(1st ‘𝑏)))) |
| 92 | 88, 91 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
𝑛 ∈
(0...(♯‘(1st ‘𝑏)))) |
| 93 | 87, 92 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑎) =
((1st ‘𝑏)
prefix (2nd ‘𝑏))) ∧ (2nd ‘𝑎) = ((1st
‘𝑏) substr
〈(2nd ‘𝑏), (♯‘(1st
‘𝑏))〉)) →
(2nd ‘𝑏)
∈ (0...(♯‘(1st ‘𝑏)))) |
| 94 | | pfxcctswrd 14748 |
. . . . . . . . . . . . . . . . . 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 2778 |
. . . . . . . . . . . . . . . 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 14721 |
. . . . . . . . . . . . . . . . . 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 2778 |
. . . . . . . . . . . . . . . 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 7449 |
. . . . . . . . . . . . . . . . 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 14740 |
. . . . . . . . . . . . . . . . . 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 2778 |
. . . . . . . . . . . . . . . 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 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → (♯‘(1st
‘𝑏)) =
((♯‘(1st ‘𝑎)) + (♯‘(2nd
‘𝑎)))) |
| 114 | 104, 113 | opeq12d 4881 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → 〈(2nd ‘𝑏),
(♯‘(1st ‘𝑏))〉 =
〈(♯‘(1st ‘𝑎)), ((♯‘(1st
‘𝑎)) +
(♯‘(2nd ‘𝑎)))〉) |
| 115 | 103, 114 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑏 = 〈𝑢, 𝑛〉) ∧ 𝑢 ∈ Word 𝐴) ∧ 𝑛 ∈ (0...(♯‘𝑢))) ∧ (1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎))) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))) → ((1st ‘𝑏) substr 〈(2nd
‘𝑏),
(♯‘(1st ‘𝑏))〉) = (((1st ‘𝑎) ++ (2nd
‘𝑎)) substr
〈(♯‘(1st ‘𝑎)), ((♯‘(1st
‘𝑎)) +
(♯‘(2nd ‘𝑎)))〉)) |
| 116 | | swrdccat2 14707 |
. . . . . . . . . . . . . . . . . 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 2778 |
. . . . . . . . . . . . . . . 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 1933 |
. . . . . . . . 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 1935 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → (((1st ‘𝑎) = ((1st
‘𝑏) prefix
(2nd ‘𝑏))
∧ (2nd ‘𝑎) = ((1st ‘𝑏) substr 〈(2nd
‘𝑏),
(♯‘(1st ‘𝑏))〉)) ↔ ((1st
‘𝑏) =
((1st ‘𝑎)
++ (2nd ‘𝑎)) ∧ (2nd ‘𝑏) =
(♯‘(1st ‘𝑎))))) |
| 128 | | eqop 8056 |
. . . . . . . 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 4808 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ Word 𝐴 → {𝑤} ⊆ Word 𝐴) |
| 131 | 130 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → {𝑤} ⊆ Word 𝐴) |
| 132 | | fz0ssnn0 13662 |
. . . . . . . . . . . 12
⊢
(0...(♯‘𝑤)) ⊆
ℕ0 |
| 133 | | xpss12 5700 |
. . . . . . . . . . . 12
⊢ (({𝑤} ⊆ Word 𝐴 ∧ (0...(♯‘𝑤)) ⊆ ℕ0)
→ ({𝑤} ×
(0...(♯‘𝑤)))
⊆ (Word 𝐴 ×
ℕ0)) |
| 134 | 131, 132,
133 | sylancl 586 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) ∧ 𝑤 ∈ Word 𝐴) → ({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 ×
ℕ0)) |
| 135 | 134 | iunssd 5050 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 ×
ℕ0)) |
| 136 | 135 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) ⊆ (Word 𝐴 ×
ℕ0)) |
| 137 | 136, 65 | sseldd 3984 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ∈ (Word 𝐴 × Word 𝐴)) → 𝑏 ∈ (Word 𝐴 ×
ℕ0)) |
| 138 | | eqop 8056 |
. . . . . . . 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 7686 |
. . 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 2795 |
. 2
⊢ (𝜑 → ◡𝐹 = 𝐺) |
| 148 | 144, 147 | jca 511 |
1
⊢ (𝜑 → (𝐹:(Word 𝐴 × Word 𝐴)–1-1-onto→𝑈 ∧ ◡𝐹 = 𝐺)) |