Metamath Proof Explorer

Theorem spllen

Description: The length of a splice. (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 𝐴 )
Assertion spllen ( 𝜑 → ( ♯ ‘ ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) = ( ( ♯ ‘ 𝑆 ) + ( ( ♯ ‘ 𝑅 ) − ( 𝑇 − 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 spllen.s ⊢ ( 𝜑 → 𝑆 ∈ Word 𝐴 )
2 spllen.f ⊢ ( 𝜑 → 𝐹 ∈ ( 0 ... 𝑇 ) )
3 spllen.t ⊢ ( 𝜑 → 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
4 spllen.r ⊢ ( 𝜑 → 𝑅 ∈ Word 𝐴 )
5 splval ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ ( 𝐹 ∈ ( 0 ... 𝑇 ) ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ 𝑅 ∈ Word 𝐴 ) ) → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
6 1 2 3 4 5 syl13anc ⊢ ( 𝜑 → ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) = ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) )
7 6 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) = ( ♯ ‘ ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
8 pfxcl ⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 )
9 1 8 syl ⊢ ( 𝜑 → ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 )
10 ccatcl ⊢ ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ∈ Word 𝐴 )
11 9 4 10 syl2anc ⊢ ( 𝜑 → ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ∈ Word 𝐴 )
12 swrdcl ⊢ ( 𝑆 ∈ Word 𝐴 → ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 )
13 1 12 syl ⊢ ( 𝜑 → ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 )
14 ccatlen ⊢ ( ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ∈ Word 𝐴 ∧ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ∈ Word 𝐴 ) → ( ♯ ‘ ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) = ( ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
15 11 13 14 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ++ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) = ( ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) )
16 lencl ⊢ ( 𝑅 ∈ Word 𝐴 → ( ♯ ‘ 𝑅 ) ∈ ℕ0 )
17 16 nn0cnd ⊢ ( 𝑅 ∈ Word 𝐴 → ( ♯ ‘ 𝑅 ) ∈ ℂ )
18 4 17 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) ∈ ℂ )
19 elfzelz ⊢ ( 𝐹 ∈ ( 0 ... 𝑇 ) → 𝐹 ∈ ℤ )
20 19 zcnd ⊢ ( 𝐹 ∈ ( 0 ... 𝑇 ) → 𝐹 ∈ ℂ )
21 2 20 syl ⊢ ( 𝜑 → 𝐹 ∈ ℂ )
22 18 21 addcld ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑅 ) + 𝐹 ) ∈ ℂ )
23 elfzel2 ⊢ ( 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑆 ) ∈ ℤ )
24 23 zcnd ⊢ ( 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑆 ) ∈ ℂ )
25 3 24 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ℂ )
26 elfzelz ⊢ ( 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → 𝑇 ∈ ℤ )
27 26 zcnd ⊢ ( 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → 𝑇 ∈ ℂ )
28 3 27 syl ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
29 22 25 28 addsub12d ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝑅 ) + 𝐹 ) + ( ( ♯ ‘ 𝑆 ) − 𝑇 ) ) = ( ( ♯ ‘ 𝑆 ) + ( ( ( ♯ ‘ 𝑅 ) + 𝐹 ) − 𝑇 ) ) )
30 ccatlen ⊢ ( ( ( 𝑆 prefix 𝐹 ) ∈ Word 𝐴 ∧ 𝑅 ∈ Word 𝐴 ) → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) )
31 9 4 30 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) )
32 elfzuz ⊢ ( 𝐹 ∈ ( 0 ... 𝑇 ) → 𝐹 ∈ ( ℤ≥ ‘ 0 ) )
33 2 32 syl ⊢ ( 𝜑 → 𝐹 ∈ ( ℤ≥ ‘ 0 ) )
34 elfzuz3 ⊢ ( 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝑇 ) )
35 3 34 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝑇 ) )
36 elfzuz3 ⊢ ( 𝐹 ∈ ( 0 ... 𝑇 ) → 𝑇 ∈ ( ℤ≥ ‘ 𝐹 ) )
37 2 36 syl ⊢ ( 𝜑 → 𝑇 ∈ ( ℤ≥ ‘ 𝐹 ) )
38 uztrn ⊢ ( ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝑇 ) ∧ 𝑇 ∈ ( ℤ≥ ‘ 𝐹 ) ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝐹 ) )
39 35 37 38 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝐹 ) )
40 elfzuzb ⊢ ( 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ↔ ( 𝐹 ∈ ( ℤ≥ ‘ 0 ) ∧ ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 𝐹 ) ) )
41 33 39 40 sylanbrc ⊢ ( 𝜑 → 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
42 pfxlen ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = 𝐹 )
43 1 41 42 syl2anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) = 𝐹 )
44 43 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝑆 prefix 𝐹 ) ) + ( ♯ ‘ 𝑅 ) ) = ( 𝐹 + ( ♯ ‘ 𝑅 ) ) )
45 21 18 addcomd ⊢ ( 𝜑 → ( 𝐹 + ( ♯ ‘ 𝑅 ) ) = ( ( ♯ ‘ 𝑅 ) + 𝐹 ) )
46 31 44 45 3eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) = ( ( ♯ ‘ 𝑅 ) + 𝐹 ) )
47 elfzuz2 ⊢ ( 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 0 ) )
48 eluzfz2 ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
49 3 47 48 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
50 swrdlen ⊢ ( ( 𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ∧ ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) ) → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = ( ( ♯ ‘ 𝑆 ) − 𝑇 ) )
51 1 3 49 50 syl3anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) = ( ( ♯ ‘ 𝑆 ) − 𝑇 ) )
52 46 51 oveq12d ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) = ( ( ( ♯ ‘ 𝑅 ) + 𝐹 ) + ( ( ♯ ‘ 𝑆 ) − 𝑇 ) ) )
53 18 28 21 subsub3d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑅 ) − ( 𝑇 − 𝐹 ) ) = ( ( ( ♯ ‘ 𝑅 ) + 𝐹 ) − 𝑇 ) )
54 53 oveq2d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑆 ) + ( ( ♯ ‘ 𝑅 ) − ( 𝑇 − 𝐹 ) ) ) = ( ( ♯ ‘ 𝑆 ) + ( ( ( ♯ ‘ 𝑅 ) + 𝐹 ) − 𝑇 ) ) )
55 29 52 54 3eqtr4d ⊢ ( 𝜑 → ( ( ♯ ‘ ( ( 𝑆 prefix 𝐹 ) ++ 𝑅 ) ) + ( ♯ ‘ ( 𝑆 substr ⟨ 𝑇 , ( ♯ ‘ 𝑆 ) ⟩ ) ) ) = ( ( ♯ ‘ 𝑆 ) + ( ( ♯ ‘ 𝑅 ) − ( 𝑇 − 𝐹 ) ) ) )
56 7 15 55 3eqtrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑆 splice ⟨ 𝐹 , 𝑇 , 𝑅 ⟩ ) ) = ( ( ♯ ‘ 𝑆 ) + ( ( ♯ ‘ 𝑅 ) − ( 𝑇 − 𝐹 ) ) ) )