Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. . . 4
⊢ (𝑆 ∈ Word 𝐴 → 𝑆 ∈ V) |
2 | | otex 4933 |
. . . 4
⊢
〈𝐹, 𝑇, 𝑅〉 ∈ V |
3 | | id 22 |
. . . . . . . 8
⊢ (𝑠 = 𝑆 → 𝑠 = 𝑆) |
4 | | fveq2 6191 |
. . . . . . . . . 10
⊢ (𝑏 = 〈𝐹, 𝑇, 𝑅〉 → (1st ‘𝑏) = (1st
‘〈𝐹, 𝑇, 𝑅〉)) |
5 | 4 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑏 = 〈𝐹, 𝑇, 𝑅〉 → (1st
‘(1st ‘𝑏)) = (1st ‘(1st
‘〈𝐹, 𝑇, 𝑅〉))) |
6 | 5 | opeq2d 4409 |
. . . . . . . 8
⊢ (𝑏 = 〈𝐹, 𝑇, 𝑅〉 → 〈0, (1st
‘(1st ‘𝑏))〉 = 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) |
7 | 3, 6 | oveqan12d 6669 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → (𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) = (𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉)) |
8 | | simpr 477 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → 𝑏 = 〈𝐹, 𝑇, 𝑅〉) |
9 | 8 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → (2nd ‘𝑏) = (2nd
‘〈𝐹, 𝑇, 𝑅〉)) |
10 | 7, 9 | oveq12d 6668 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → ((𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) ++ (2nd ‘𝑏)) = ((𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ++ (2nd
‘〈𝐹, 𝑇, 𝑅〉))) |
11 | | simpl 473 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → 𝑠 = 𝑆) |
12 | 8 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → (1st ‘𝑏) = (1st
‘〈𝐹, 𝑇, 𝑅〉)) |
13 | 12 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → (2nd
‘(1st ‘𝑏)) = (2nd ‘(1st
‘〈𝐹, 𝑇, 𝑅〉))) |
14 | 11 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → (#‘𝑠) = (#‘𝑆)) |
15 | 13, 14 | opeq12d 4410 |
. . . . . . 7
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → 〈(2nd
‘(1st ‘𝑏)), (#‘𝑠)〉 = 〈(2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)), (#‘𝑆)〉) |
16 | 11, 15 | oveq12d 6668 |
. . . . . 6
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (#‘𝑠)〉) = (𝑆 substr 〈(2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)), (#‘𝑆)〉)) |
17 | 10, 16 | oveq12d 6668 |
. . . . 5
⊢ ((𝑠 = 𝑆 ∧ 𝑏 = 〈𝐹, 𝑇, 𝑅〉) → (((𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) ++ (2nd ‘𝑏)) ++ (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (#‘𝑠)〉)) = (((𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ++ (2nd
‘〈𝐹, 𝑇, 𝑅〉)) ++ (𝑆 substr 〈(2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)), (#‘𝑆)〉))) |
18 | | df-splice 13304 |
. . . . 5
⊢ splice =
(𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr 〈0, (1st
‘(1st ‘𝑏))〉) ++ (2nd ‘𝑏)) ++ (𝑠 substr 〈(2nd
‘(1st ‘𝑏)), (#‘𝑠)〉))) |
19 | | ovex 6678 |
. . . . 5
⊢ (((𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ++ (2nd
‘〈𝐹, 𝑇, 𝑅〉)) ++ (𝑆 substr 〈(2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)), (#‘𝑆)〉)) ∈ V |
20 | 17, 18, 19 | ovmpt2a 6791 |
. . . 4
⊢ ((𝑆 ∈ V ∧ 〈𝐹, 𝑇, 𝑅〉 ∈ V) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ++ (2nd
‘〈𝐹, 𝑇, 𝑅〉)) ++ (𝑆 substr 〈(2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)), (#‘𝑆)〉))) |
21 | 1, 2, 20 | sylancl 694 |
. . 3
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ++ (2nd
‘〈𝐹, 𝑇, 𝑅〉)) ++ (𝑆 substr 〈(2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)), (#‘𝑆)〉))) |
22 | 21 | adantr 481 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) = (((𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ++ (2nd
‘〈𝐹, 𝑇, 𝑅〉)) ++ (𝑆 substr 〈(2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)), (#‘𝑆)〉))) |
23 | | swrdcl 13419 |
. . . . 5
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ∈ Word 𝐴) |
24 | 23 | adantr 481 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ∈ Word 𝐴) |
25 | | ot3rdg 7184 |
. . . . . 6
⊢ (𝑅 ∈ Word 𝐴 → (2nd ‘〈𝐹, 𝑇, 𝑅〉) = 𝑅) |
26 | 25 | adantl 482 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (2nd ‘〈𝐹, 𝑇, 𝑅〉) = 𝑅) |
27 | | simpr 477 |
. . . . 5
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → 𝑅 ∈ Word 𝐴) |
28 | 26, 27 | eqeltrd 2701 |
. . . 4
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (2nd ‘〈𝐹, 𝑇, 𝑅〉) ∈ Word 𝐴) |
29 | | ccatcl 13359 |
. . . 4
⊢ (((𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ∈ Word 𝐴 ∧ (2nd
‘〈𝐹, 𝑇, 𝑅〉) ∈ Word 𝐴) → ((𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ++ (2nd
‘〈𝐹, 𝑇, 𝑅〉)) ∈ Word 𝐴) |
30 | 24, 28, 29 | syl2anc 693 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → ((𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ++ (2nd
‘〈𝐹, 𝑇, 𝑅〉)) ∈ Word 𝐴) |
31 | | swrdcl 13419 |
. . . 4
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈(2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)), (#‘𝑆)〉) ∈ Word 𝐴) |
32 | 31 | adantr 481 |
. . 3
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (𝑆 substr 〈(2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)), (#‘𝑆)〉) ∈ Word 𝐴) |
33 | | ccatcl 13359 |
. . 3
⊢ ((((𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ++ (2nd
‘〈𝐹, 𝑇, 𝑅〉)) ∈ Word 𝐴 ∧ (𝑆 substr 〈(2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)), (#‘𝑆)〉) ∈ Word 𝐴) → (((𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ++ (2nd
‘〈𝐹, 𝑇, 𝑅〉)) ++ (𝑆 substr 〈(2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)), (#‘𝑆)〉)) ∈ Word 𝐴) |
34 | 30, 32, 33 | syl2anc 693 |
. 2
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (((𝑆 substr 〈0, (1st
‘(1st ‘〈𝐹, 𝑇, 𝑅〉))〉) ++ (2nd
‘〈𝐹, 𝑇, 𝑅〉)) ++ (𝑆 substr 〈(2nd
‘(1st ‘〈𝐹, 𝑇, 𝑅〉)), (#‘𝑆)〉)) ∈ Word 𝐴) |
35 | 22, 34 | eqeltrd 2701 |
1
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴) → (𝑆 splice 〈𝐹, 𝑇, 𝑅〉) ∈ Word 𝐴) |