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 ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( 𝐴 ++ 𝑅 ) ++ 𝐶 ) )