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