Metamath Proof Explorer


Theorem splfv2a

Description: Symbols within the replacement region of a splice, expressed using the coordinates of the replacement region. (Contributed by Stefan O'Rear, 23-Aug-2015) (Proof shortened by AV, 15-Oct-2022)

Ref Expression
Hypotheses spllen.s ( 𝜑𝑆 ∈ Word 𝐴 )
spllen.f ( 𝜑𝐹 ∈ ( 0 ... 𝑇 ) )
spllen.t ( 𝜑𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
spllen.r ( 𝜑𝑅 ∈ Word 𝐴 )
splfv2a.x ( 𝜑𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝑅 ) ) )
Assertion splfv2a ( 𝜑 → ( ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ‘ ( 𝐹 + 𝑋 ) ) = ( 𝑅𝑋 ) )

Proof

Step Hyp Ref Expression
1 spllen.s ( 𝜑𝑆 ∈ Word 𝐴 )
2 spllen.f ( 𝜑𝐹 ∈ ( 0 ... 𝑇 ) )
3 spllen.t ( 𝜑𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
4 spllen.r ( 𝜑𝑅 ∈ Word 𝐴 )
5 splfv2a.x ( 𝜑𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝑅 ) ) )
6 splval ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝐹 ∈ ( 0 ... 𝑇 ) ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑅 ∈ Word 𝐴 ) ) → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
7 1 2 3 4 6 syl13anc ( 𝜑 → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
8 elfznn0 ( 𝐹 ∈ ( 0 ... 𝑇 ) → 𝐹 ∈ ℕ0 )
9 2 8 syl ( 𝜑𝐹 ∈ ℕ0 )
10 9 nn0cnd ( 𝜑𝐹 ∈ ℂ )
11 elfzonn0 ( 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝑅 ) ) → 𝑋 ∈ ℕ0 )
12 5 11 syl ( 𝜑𝑋 ∈ ℕ0 )
13 12 nn0cnd ( 𝜑𝑋 ∈ ℂ )
14 10 13 addcomd ( 𝜑 → ( 𝐹 + 𝑋 ) = ( 𝑋 + 𝐹 ) )
15 nn0uz 0 = ( ℤ ‘ 0 )
16 9 15 eleqtrdi ( 𝜑𝐹 ∈ ( ℤ ‘ 0 ) )
17 elfzuz3 ( 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ𝑇 ) )
18 3 17 syl ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ( ℤ𝑇 ) )
19 elfzuz3 ( 𝐹 ∈ ( 0 ... 𝑇 ) → 𝑇 ∈ ( ℤ𝐹 ) )
20 2 19 syl ( 𝜑𝑇 ∈ ( ℤ𝐹 ) )
21 uztrn ( ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ𝑇 ) ∧ 𝑇 ∈ ( ℤ𝐹 ) ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ𝐹 ) )
22 18 20 21 syl2anc ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ( ℤ𝐹 ) )
23 elfzuzb ( 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ↔ ( 𝐹 ∈ ( ℤ ‘ 0 ) ∧ ( ♯ ‘ 𝑆 ) ∈ ( ℤ𝐹 ) ) )
24 16 22 23 sylanbrc ( 𝜑𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
25 pfxlen ( ( 𝑆 ∈ Word 𝐴𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = 𝐹 )
26 1 24 25 syl2anc ( 𝜑 → ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = 𝐹 )
27 26 oveq2d ( 𝜑 → ( 𝑋 + ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) = ( 𝑋 + 𝐹 ) )
28 14 27 eqtr4d ( 𝜑 → ( 𝐹 + 𝑋 ) = ( 𝑋 + ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) )
29 7 28 fveq12d ( 𝜑 → ( ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ‘ ( 𝐹 + 𝑋 ) ) = ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ‘ ( 𝑋 + ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) ) )
30 pfxcl ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 )
31 1 30 syl ( 𝜑 → ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 )
32 ccatcl ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴𝑅 ∈ Word 𝐴 ) → ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ∈ Word 𝐴 )
33 31 4 32 syl2anc ( 𝜑 → ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ∈ Word 𝐴 )
34 swrdcl ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 )
35 1 34 syl ( 𝜑 → ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 )
36 0nn0 0 ∈ ℕ0
37 nn0addcl ( ( 0 ∈ ℕ0𝐹 ∈ ℕ0 ) → ( 0 + 𝐹 ) ∈ ℕ0 )
38 36 9 37 sylancr ( 𝜑 → ( 0 + 𝐹 ) ∈ ℕ0 )
39 fzoss1 ( ( 0 + 𝐹 ) ∈ ( ℤ ‘ 0 ) → ( ( 0 + 𝐹 ) ..^ ( ( ♯ ‘ 𝑅 ) + 𝐹 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑅 ) + 𝐹 ) ) )
40 39 15 eleq2s ( ( 0 + 𝐹 ) ∈ ℕ0 → ( ( 0 + 𝐹 ) ..^ ( ( ♯ ‘ 𝑅 ) + 𝐹 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑅 ) + 𝐹 ) ) )
41 38 40 syl ( 𝜑 → ( ( 0 + 𝐹 ) ..^ ( ( ♯ ‘ 𝑅 ) + 𝐹 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑅 ) + 𝐹 ) ) )
42 ccatlen ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴𝑅 ∈ Word 𝐴 ) → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) )
43 31 4 42 syl2anc ( 𝜑 → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) )
44 26 oveq1d ( 𝜑 → ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) = ( 𝐹 + ( ♯ ‘ 𝑅 ) ) )
45 lencl ( 𝑅 ∈ Word 𝐴 → ( ♯ ‘ 𝑅 ) ∈ ℕ0 )
46 4 45 syl ( 𝜑 → ( ♯ ‘ 𝑅 ) ∈ ℕ0 )
47 46 nn0cnd ( 𝜑 → ( ♯ ‘ 𝑅 ) ∈ ℂ )
48 10 47 addcomd ( 𝜑 → ( 𝐹 + ( ♯ ‘ 𝑅 ) ) = ( ( ♯ ‘ 𝑅 ) + 𝐹 ) )
49 43 44 48 3eqtrd ( 𝜑 → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( ( ♯ ‘ 𝑅 ) + 𝐹 ) )
50 49 oveq2d ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑅 ) + 𝐹 ) ) )
51 41 50 sseqtrrd ( 𝜑 → ( ( 0 + 𝐹 ) ..^ ( ( ♯ ‘ 𝑅 ) + 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) )
52 9 nn0zd ( 𝜑𝐹 ∈ ℤ )
53 fzoaddel ( ( 𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝑅 ) ) ∧ 𝐹 ∈ ℤ ) → ( 𝑋 + 𝐹 ) ∈ ( ( 0 + 𝐹 ) ..^ ( ( ♯ ‘ 𝑅 ) + 𝐹 ) ) )
54 5 52 53 syl2anc ( 𝜑 → ( 𝑋 + 𝐹 ) ∈ ( ( 0 + 𝐹 ) ..^ ( ( ♯ ‘ 𝑅 ) + 𝐹 ) ) )
55 51 54 sseldd ( 𝜑 → ( 𝑋 + 𝐹 ) ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) )
56 27 55 eqeltrd ( 𝜑 → ( 𝑋 + ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) )
57 ccatval1 ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 ∧ ( 𝑋 + ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) ∈ ( 0 ..^ ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) ) ) → ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ‘ ( 𝑋 + ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ ( 𝑋 + ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) ) )
58 33 35 56 57 syl3anc ( 𝜑 → ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ‘ ( 𝑋 + ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ ( 𝑋 + ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) ) )
59 ccatval3 ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴𝑅 ∈ Word 𝐴𝑋 ∈ ( 0 ..^ ( ♯ ‘ 𝑅 ) ) ) → ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ ( 𝑋 + ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) ) = ( 𝑅𝑋 ) )
60 31 4 5 59 syl3anc ( 𝜑 → ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ‘ ( 𝑋 + ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) ) ) = ( 𝑅𝑋 ) )
61 29 58 60 3eqtrd ( 𝜑 → ( ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ‘ ( 𝐹 + 𝑋 ) ) = ( 𝑅𝑋 ) )