Metamath Proof Explorer

Theorem pfxccat1

Description: Recover the left half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by AV, 6-May-2020)

Ref Expression
Assertion pfxccat1 ⊢S∈WordB∧T∈WordB→S++TprefixS=S

Proof

Step Hyp Ref Expression
1 ccatcl ⊢S∈WordB∧T∈WordB→S++T∈WordB
2 lencl ⊢S∈WordB→S∈ℕ0
3 lencl ⊢T∈WordB→T∈ℕ0
4 2 3 anim12i ⊢S∈WordB∧T∈WordB→S∈ℕ0∧T∈ℕ0
5 nn0fz0 ⊢S∈ℕ0↔S∈0…S
6 2 5 sylib ⊢S∈WordB→S∈0…S
7 6 adantr ⊢S∈WordB∧T∈WordB→S∈0…S
8 elfz0add ⊢S∈ℕ0∧T∈ℕ0→S∈0…S→S∈0…S+T
9 4 7 8 sylc ⊢S∈WordB∧T∈WordB→S∈0…S+T
10 ccatlen ⊢S∈WordB∧T∈WordB→S++T=S+T
11 10 oveq2d ⊢S∈WordB∧T∈WordB→0…S++T=0…S+T
12 9 11 eleqtrrd ⊢S∈WordB∧T∈WordB→S∈0…S++T
13 pfxres ⊢S++T∈WordB∧S∈0…S++T→S++TprefixS=S++T↾0..^S
14 1 12 13 syl2anc ⊢S∈WordB∧T∈WordB→S++TprefixS=S++T↾0..^S
15 ccatvalfn ⊢S∈WordB∧T∈WordB→S++TFn0..^S+T
16 2 nn0zd ⊢S∈WordB→S∈ℤ
17 16 uzidd ⊢S∈WordB→S∈ℤ≥S
18 uzaddcl ⊢S∈ℤ≥S∧T∈ℕ0→S+T∈ℤ≥S
19 17 3 18 syl2an ⊢S∈WordB∧T∈WordB→S+T∈ℤ≥S
20 fzoss2 ⊢S+T∈ℤ≥S→0..^S⊆0..^S+T
21 19 20 syl ⊢S∈WordB∧T∈WordB→0..^S⊆0..^S+T
22 15 21 fnssresd ⊢S∈WordB∧T∈WordB→S++T↾0..^SFn0..^S
23 wrdfn ⊢S∈WordB→SFn0..^S
24 23 adantr ⊢S∈WordB∧T∈WordB→SFn0..^S
25 fvres ⊢k∈0..^S→S++T↾0..^S⁡k=S++T⁡k
26 25 adantl ⊢S∈WordB∧T∈WordB∧k∈0..^S→S++T↾0..^S⁡k=S++T⁡k
27 ccatval1 ⊢S∈WordB∧T∈WordB∧k∈0..^S→S++T⁡k=S⁡k
28 27 3expa ⊢S∈WordB∧T∈WordB∧k∈0..^S→S++T⁡k=S⁡k
29 26 28 eqtrd ⊢S∈WordB∧T∈WordB∧k∈0..^S→S++T↾0..^S⁡k=S⁡k
30 22 24 29 eqfnfvd ⊢S∈WordB∧T∈WordB→S++T↾0..^S=S
31 14 30 eqtrd ⊢S∈WordB∧T∈WordB→S++TprefixS=S