Metamath Proof Explorer


Theorem splval2

Description: Value of a splice, assuming the input word S has already been decomposed into its pieces. (Contributed by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 15-Oct-2022)

Ref Expression
Hypotheses splval2.a ( 𝜑𝐴 ∈ Word 𝑋 )
splval2.b ( 𝜑𝐵 ∈ Word 𝑋 )
splval2.c ( 𝜑𝐶 ∈ Word 𝑋 )
splval2.r ( 𝜑𝑅 ∈ Word 𝑋 )
splval2.s ( 𝜑𝑆 = ( ( 𝐴 ++ 𝐵 ) ++ 𝐶 ) )
splval2.f ( 𝜑𝐹 = ( ♯ ‘ 𝐴 ) )
splval2.t ( 𝜑𝑇 = ( 𝐹 + ( ♯ ‘ 𝐵 ) ) )
Assertion splval2 ( 𝜑 → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( 𝐴 ++ 𝑅 ) ++ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 splval2.a ( 𝜑𝐴 ∈ Word 𝑋 )
2 splval2.b ( 𝜑𝐵 ∈ Word 𝑋 )
3 splval2.c ( 𝜑𝐶 ∈ Word 𝑋 )
4 splval2.r ( 𝜑𝑅 ∈ Word 𝑋 )
5 splval2.s ( 𝜑𝑆 = ( ( 𝐴 ++ 𝐵 ) ++ 𝐶 ) )
6 splval2.f ( 𝜑𝐹 = ( ♯ ‘ 𝐴 ) )
7 splval2.t ( 𝜑𝑇 = ( 𝐹 + ( ♯ ‘ 𝐵 ) ) )
8 ccatcl ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) → ( 𝐴 ++ 𝐵 ) ∈ Word 𝑋 )
9 1 2 8 syl2anc ( 𝜑 → ( 𝐴 ++ 𝐵 ) ∈ Word 𝑋 )
10 ccatcl ( ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑋𝐶 ∈ Word 𝑋 ) → ( ( 𝐴 ++ 𝐵 ) ++ 𝐶 ) ∈ Word 𝑋 )
11 9 3 10 syl2anc ( 𝜑 → ( ( 𝐴 ++ 𝐵 ) ++ 𝐶 ) ∈ Word 𝑋 )
12 5 11 eqeltrd ( 𝜑𝑆 ∈ Word 𝑋 )
13 lencl ( 𝐴 ∈ Word 𝑋 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
14 1 13 syl ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
15 6 14 eqeltrd ( 𝜑𝐹 ∈ ℕ0 )
16 lencl ( 𝐵 ∈ Word 𝑋 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
17 2 16 syl ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
18 15 17 nn0addcld ( 𝜑 → ( 𝐹 + ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 )
19 7 18 eqeltrd ( 𝜑𝑇 ∈ ℕ0 )
20 splval ( ( 𝑆 ∈ Word 𝑋 ∧ ( 𝐹 ∈ ℕ0𝑇 ∈ ℕ0𝑅 ∈ Word 𝑋 ) ) → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
21 12 15 19 4 20 syl13anc ( 𝜑 → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
22 nn0uz 0 = ( ℤ ‘ 0 )
23 15 22 eleqtrdi ( 𝜑𝐹 ∈ ( ℤ ‘ 0 ) )
24 15 nn0zd ( 𝜑𝐹 ∈ ℤ )
25 24 uzidd ( 𝜑𝐹 ∈ ( ℤ𝐹 ) )
26 uzaddcl ( ( 𝐹 ∈ ( ℤ𝐹 ) ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( 𝐹 + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ𝐹 ) )
27 25 17 26 syl2anc ( 𝜑 → ( 𝐹 + ( ♯ ‘ 𝐵 ) ) ∈ ( ℤ𝐹 ) )
28 7 27 eqeltrd ( 𝜑𝑇 ∈ ( ℤ𝐹 ) )
29 elfzuzb ( 𝐹 ∈ ( 0 ... 𝑇 ) ↔ ( 𝐹 ∈ ( ℤ ‘ 0 ) ∧ 𝑇 ∈ ( ℤ𝐹 ) ) )
30 23 28 29 sylanbrc ( 𝜑𝐹 ∈ ( 0 ... 𝑇 ) )
31 19 22 eleqtrdi ( 𝜑𝑇 ∈ ( ℤ ‘ 0 ) )
32 ccatlen ( ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑋𝐶 ∈ Word 𝑋 ) → ( ♯ ‘ ( ( 𝐴 ++ 𝐵 ) ++ 𝐶 ) ) = ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) + ( ♯ ‘ 𝐶 ) ) )
33 9 3 32 syl2anc ( 𝜑 → ( ♯ ‘ ( ( 𝐴 ++ 𝐵 ) ++ 𝐶 ) ) = ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) + ( ♯ ‘ 𝐶 ) ) )
34 5 fveq2d ( 𝜑 → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ ( ( 𝐴 ++ 𝐵 ) ++ 𝐶 ) ) )
35 6 oveq1d ( 𝜑 → ( 𝐹 + ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
36 ccatlen ( ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
37 1 2 36 syl2anc ( 𝜑 → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
38 35 7 37 3eqtr4d ( 𝜑𝑇 = ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) )
39 38 oveq1d ( 𝜑 → ( 𝑇 + ( ♯ ‘ 𝐶 ) ) = ( ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) + ( ♯ ‘ 𝐶 ) ) )
40 33 34 39 3eqtr4d ( 𝜑 → ( ♯ ‘ 𝑆 ) = ( 𝑇 + ( ♯ ‘ 𝐶 ) ) )
41 19 nn0zd ( 𝜑𝑇 ∈ ℤ )
42 41 uzidd ( 𝜑𝑇 ∈ ( ℤ𝑇 ) )
43 lencl ( 𝐶 ∈ Word 𝑋 → ( ♯ ‘ 𝐶 ) ∈ ℕ0 )
44 3 43 syl ( 𝜑 → ( ♯ ‘ 𝐶 ) ∈ ℕ0 )
45 uzaddcl ( ( 𝑇 ∈ ( ℤ𝑇 ) ∧ ( ♯ ‘ 𝐶 ) ∈ ℕ0 ) → ( 𝑇 + ( ♯ ‘ 𝐶 ) ) ∈ ( ℤ𝑇 ) )
46 42 44 45 syl2anc ( 𝜑 → ( 𝑇 + ( ♯ ‘ 𝐶 ) ) ∈ ( ℤ𝑇 ) )
47 40 46 eqeltrd ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ( ℤ𝑇 ) )
48 elfzuzb ( 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ↔ ( 𝑇 ∈ ( ℤ ‘ 0 ) ∧ ( ♯ ‘ 𝑆 ) ∈ ( ℤ𝑇 ) ) )
49 31 47 48 sylanbrc ( 𝜑𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
50 ccatpfx ( ( 𝑆 ∈ Word 𝑋𝐹 ∈ ( 0 ... 𝑇 ) ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 prefix 𝐹 ) ++ ( 𝑆 substr ⟨ 𝐹 , 𝑇 ⟩ ) ) = ( 𝑆 prefix 𝑇 ) )
51 12 30 49 50 syl3anc ( 𝜑 → ( ( 𝑆 prefix 𝐹 ) ++ ( 𝑆 substr ⟨ 𝐹 , 𝑇 ⟩ ) ) = ( 𝑆 prefix 𝑇 ) )
52 lencl ( 𝑆 ∈ Word 𝑋 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
53 12 52 syl ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
54 53 22 eleqtrdi ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ( ℤ ‘ 0 ) )
55 eluzfz2 ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ ‘ 0 ) → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
56 54 55 syl ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
57 ccatpfx ( ( 𝑆 ∈ Word 𝑋𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 prefix 𝑇 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) )
58 12 49 56 57 syl3anc ( 𝜑 → ( ( 𝑆 prefix 𝑇 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) )
59 pfxid ( 𝑆 ∈ Word 𝑋 → ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) = 𝑆 )
60 12 59 syl ( 𝜑 → ( 𝑆 prefix ( ♯ ‘ 𝑆 ) ) = 𝑆 )
61 58 60 5 3eqtrd ( 𝜑 → ( ( 𝑆 prefix 𝑇 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = ( ( 𝐴 ++ 𝐵 ) ++ 𝐶 ) )
62 pfxcl ( 𝑆 ∈ Word 𝑋 → ( 𝑆 prefix 𝑇 ) ∈ Word 𝑋 )
63 12 62 syl ( 𝜑 → ( 𝑆 prefix 𝑇 ) ∈ Word 𝑋 )
64 swrdcl ( 𝑆 ∈ Word 𝑋 → ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝑋 )
65 12 64 syl ( 𝜑 → ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝑋 )
66 pfxlen ( ( 𝑆 ∈ Word 𝑋𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝑇 ) ) = 𝑇 )
67 12 49 66 syl2anc ( 𝜑 → ( ♯ ‘ ( 𝑆 prefix 𝑇 ) ) = 𝑇 )
68 67 38 eqtrd ( 𝜑 → ( ♯ ‘ ( 𝑆 prefix 𝑇 ) ) = ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) )
69 ccatopth ( ( ( ( 𝑆 prefix 𝑇 ) ∈ Word 𝑋 ∧ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝑋 ) ∧ ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑋𝐶 ∈ Word 𝑋 ) ∧ ( ♯ ‘ ( 𝑆 prefix 𝑇 ) ) = ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) → ( ( ( 𝑆 prefix 𝑇 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = ( ( 𝐴 ++ 𝐵 ) ++ 𝐶 ) ↔ ( ( 𝑆 prefix 𝑇 ) = ( 𝐴 ++ 𝐵 ) ∧ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) = 𝐶 ) ) )
70 63 65 9 3 68 69 syl221anc ( 𝜑 → ( ( ( 𝑆 prefix 𝑇 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = ( ( 𝐴 ++ 𝐵 ) ++ 𝐶 ) ↔ ( ( 𝑆 prefix 𝑇 ) = ( 𝐴 ++ 𝐵 ) ∧ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) = 𝐶 ) ) )
71 61 70 mpbid ( 𝜑 → ( ( 𝑆 prefix 𝑇 ) = ( 𝐴 ++ 𝐵 ) ∧ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) = 𝐶 ) )
72 71 simpld ( 𝜑 → ( 𝑆 prefix 𝑇 ) = ( 𝐴 ++ 𝐵 ) )
73 51 72 eqtrd ( 𝜑 → ( ( 𝑆 prefix 𝐹 ) ++ ( 𝑆 substr ⟨ 𝐹 , 𝑇 ⟩ ) ) = ( 𝐴 ++ 𝐵 ) )
74 pfxcl ( 𝑆 ∈ Word 𝑋 → ( 𝑆 prefix 𝐹 ) ∈ Word 𝑋 )
75 12 74 syl ( 𝜑 → ( 𝑆 prefix 𝐹 ) ∈ Word 𝑋 )
76 swrdcl ( 𝑆 ∈ Word 𝑋 → ( 𝑆 substr ⟨ 𝐹 , 𝑇 ⟩ ) ∈ Word 𝑋 )
77 12 76 syl ( 𝜑 → ( 𝑆 substr ⟨ 𝐹 , 𝑇 ⟩ ) ∈ Word 𝑋 )
78 uztrn ( ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ𝑇 ) ∧ 𝑇 ∈ ( ℤ𝐹 ) ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ𝐹 ) )
79 47 28 78 syl2anc ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ( ℤ𝐹 ) )
80 elfzuzb ( 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ↔ ( 𝐹 ∈ ( ℤ ‘ 0 ) ∧ ( ♯ ‘ 𝑆 ) ∈ ( ℤ𝐹 ) ) )
81 23 79 80 sylanbrc ( 𝜑𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
82 pfxlen ( ( 𝑆 ∈ Word 𝑋𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = 𝐹 )
83 12 81 82 syl2anc ( 𝜑 → ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = 𝐹 )
84 83 6 eqtrd ( 𝜑 → ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = ( ♯ ‘ 𝐴 ) )
85 ccatopth ( ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝑋 ∧ ( 𝑆 substr ⟨ 𝐹 , 𝑇 ⟩ ) ∈ Word 𝑋 ) ∧ ( 𝐴 ∈ Word 𝑋𝐵 ∈ Word 𝑋 ) ∧ ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = ( ♯ ‘ 𝐴 ) ) → ( ( ( 𝑆 prefix 𝐹 ) ++ ( 𝑆 substr ⟨ 𝐹 , 𝑇 ⟩ ) ) = ( 𝐴 ++ 𝐵 ) ↔ ( ( 𝑆 prefix 𝐹 ) = 𝐴 ∧ ( 𝑆 substr ⟨ 𝐹 , 𝑇 ⟩ ) = 𝐵 ) ) )
86 75 77 1 2 84 85 syl221anc ( 𝜑 → ( ( ( 𝑆 prefix 𝐹 ) ++ ( 𝑆 substr ⟨ 𝐹 , 𝑇 ⟩ ) ) = ( 𝐴 ++ 𝐵 ) ↔ ( ( 𝑆 prefix 𝐹 ) = 𝐴 ∧ ( 𝑆 substr ⟨ 𝐹 , 𝑇 ⟩ ) = 𝐵 ) ) )
87 73 86 mpbid ( 𝜑 → ( ( 𝑆 prefix 𝐹 ) = 𝐴 ∧ ( 𝑆 substr ⟨ 𝐹 , 𝑇 ⟩ ) = 𝐵 ) )
88 87 simpld ( 𝜑 → ( 𝑆 prefix 𝐹 ) = 𝐴 )
89 88 oveq1d ( 𝜑 → ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) = ( 𝐴 ++ 𝑅 ) )
90 71 simprd ( 𝜑 → ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) = 𝐶 )
91 89 90 oveq12d ( 𝜑 → ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = ( ( 𝐴 ++ 𝑅 ) ++ 𝐶 ) )
92 21 91 eqtrd ( 𝜑 → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( 𝐴 ++ 𝑅 ) ++ 𝐶 ) )