Step | Hyp | Ref
| Expression |
1 | | elex 3466 |
. . . 4
⊢ (𝑆 ∈ Word 𝐴 → 𝑆 ∈ V) |
2 | | otex 5427 |
. . . 4
⊢
⟨𝐹, 𝑇, 𝑅⟩ ∈ V |
3 | | id 22 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → 𝑠 = 𝑆) |
4 | | 2fveq3 6852 |
. . . . . . . 8
⊢ (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (1st
‘(1st ‘𝑏)) = (1st ‘(1st
‘⟨𝐹, 𝑇, 𝑅⟩))) |
5 | 3, 4 | oveqan12d 7381 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (𝑠 prefix (1st
‘(1st ‘𝑏))) = (𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))) |
6 | | simpr 486 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) |
7 | 6 | fveq2d 6851 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd ‘𝑏) = (2nd
‘⟨𝐹, 𝑇, 𝑅⟩)) |
8 | 5, 7 | oveq12d 7380 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → ((𝑠 prefix (1st
‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) = ((𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ++ (2nd
‘⟨𝐹, 𝑇, 𝑅⟩))) |
9 | | simpl 484 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → 𝑠 = 𝑆) |
10 | 6 | fveq2d 6851 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (1st ‘𝑏) = (1st
‘⟨𝐹, 𝑇, 𝑅⟩)) |
11 | 10 | fveq2d 6851 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd
‘(1st ‘𝑏)) = (2nd ‘(1st
‘⟨𝐹, 𝑇, 𝑅⟩))) |
12 | 9 | fveq2d 6851 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (♯‘𝑠) = (♯‘𝑆)) |
13 | 11, 12 | opeq12d 4843 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → ⟨(2nd
‘(1st ‘𝑏)), (♯‘𝑠)⟩ = ⟨(2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)), (♯‘𝑆)⟩) |
14 | 9, 13 | oveq12d 7380 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (𝑠 substr ⟨(2nd
‘(1st ‘𝑏)), (♯‘𝑠)⟩) = (𝑆 substr ⟨(2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)), (♯‘𝑆)⟩)) |
15 | 8, 14 | oveq12d 7380 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (((𝑠 prefix (1st
‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd
‘(1st ‘𝑏)), (♯‘𝑠)⟩)) = (((𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ++ (2nd
‘⟨𝐹, 𝑇, 𝑅⟩)) ++ (𝑆 substr ⟨(2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)), (♯‘𝑆)⟩))) |
16 | | df-splice 14645 |
. . . . 5
⊢ splice =
(𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1st
‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd
‘(1st ‘𝑏)), (♯‘𝑠)⟩))) |
17 | | ovex 7395 |
. . . . 5
⊢ (((𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ++ (2nd
‘⟨𝐹, 𝑇, 𝑅⟩)) ++ (𝑆 substr ⟨(2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)), (♯‘𝑆)⟩)) ∈ V |
18 | 15, 16, 17 | ovmpoa 7515 |
. . . 4
⊢ ((𝑆 ∈ V ∧ ⟨𝐹, 𝑇, 𝑅⟩ ∈ V) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ++ (2nd
‘⟨𝐹, 𝑇, 𝑅⟩)) ++ (𝑆 substr ⟨(2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)), (♯‘𝑆)⟩))) |
19 | 1, 2, 18 | sylancl 587 |
. . 3
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ++ (2nd
‘⟨𝐹, 𝑇, 𝑅⟩)) ++ (𝑆 substr ⟨(2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)), (♯‘𝑆)⟩))) |
20 | 19 | adantr 482 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ++ (2nd
‘⟨𝐹, 𝑇, 𝑅⟩)) ++ (𝑆 substr ⟨(2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)), (♯‘𝑆)⟩))) |
21 | | pfxcl 14572 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ∈ Word 𝐴) |
22 | 21 | adantr 482 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ∈ Word 𝐴) |
23 | | ot3rdg 7942 |
. . . . . 6
⊢ (𝑅 ∈ Word 𝐴 → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅) |
24 | 23 | adantl 483 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅) |
25 | | simpr 486 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → 𝑅 ∈ Word 𝐴) |
26 | 24, 25 | eqeltrd 2838 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) ∈ Word 𝐴) |
27 | | ccatcl 14469 |
. . . 4
⊢ (((𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ∈ Word 𝐴 ∧ (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) ∈ Word 𝐴) → ((𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ++ (2nd
‘⟨𝐹, 𝑇, 𝑅⟩)) ∈ Word 𝐴) |
28 | 22, 26, 27 | syl2anc 585 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → ((𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ++ (2nd
‘⟨𝐹, 𝑇, 𝑅⟩)) ∈ Word 𝐴) |
29 | | swrdcl 14540 |
. . . 4
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr ⟨(2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)), (♯‘𝑆)⟩) ∈ Word 𝐴) |
30 | 29 | adantr 482 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (𝑆 substr ⟨(2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)), (♯‘𝑆)⟩) ∈ Word 𝐴) |
31 | | ccatcl 14469 |
. . 3
⊢ ((((𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ++ (2nd
‘⟨𝐹, 𝑇, 𝑅⟩)) ∈ Word 𝐴 ∧ (𝑆 substr ⟨(2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)), (♯‘𝑆)⟩) ∈ Word 𝐴) → (((𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ++ (2nd
‘⟨𝐹, 𝑇, 𝑅⟩)) ++ (𝑆 substr ⟨(2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)), (♯‘𝑆)⟩)) ∈ Word 𝐴) |
32 | 28, 30, 31 | syl2anc 585 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (((𝑆 prefix (1st
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩))) ++ (2nd
‘⟨𝐹, 𝑇, 𝑅⟩)) ++ (𝑆 substr ⟨(2nd
‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)), (♯‘𝑆)⟩)) ∈ Word 𝐴) |
33 | 20, 32 | eqeltrd 2838 |
1
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) ∈ Word 𝐴) |