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 ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( 𝑆 ++ 𝑇 ) prefix ( ♯ ‘ 𝑆 ) ) = 𝑆 )

Proof

Step Hyp Ref Expression
1 ccatcl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 𝑆 ++ 𝑇 ) ∈ Word 𝐵 )
2 lencl ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
3 lencl ⊢ ( 𝑇 ∈ Word 𝐵 → ( ♯ ‘ 𝑇 ) ∈ ℕ0 )
4 2 3 anim12i ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑇 ) ∈ ℕ0 ) )
5 nn0fz0 ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
6 2 5 sylib ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
7 6 adantr ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) )
8 elfz0add ⊢ ( ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑇 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ 𝑆 ) ) → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) ) )
9 4 7 8 sylc ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
10 ccatlen ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) )
11 10 oveq2d ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 0 ... ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) = ( 0 ... ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
12 9 11 eleqtrrd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) )
13 pfxres ⊢ ( ( ( 𝑆 ++ 𝑇 ) ∈ Word 𝐵 ∧ ( ♯ ‘ 𝑆 ) ∈ ( 0 ... ( ♯ ‘ ( 𝑆 ++ 𝑇 ) ) ) ) → ( ( 𝑆 ++ 𝑇 ) prefix ( ♯ ‘ 𝑆 ) ) = ( ( 𝑆 ++ 𝑇 ) ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
14 1 12 13 syl2anc ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( 𝑆 ++ 𝑇 ) prefix ( ♯ ‘ 𝑆 ) ) = ( ( 𝑆 ++ 𝑇 ) ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
15 ccatvalfn ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 𝑆 ++ 𝑇 ) Fn ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
16 2 nn0zd ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ℤ )
17 16 uzidd ⊢ ( 𝑆 ∈ Word 𝐵 → ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) )
18 uzaddcl ⊢ ( ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) ∧ ( ♯ ‘ 𝑇 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) )
19 17 3 18 syl2an ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) )
20 fzoss2 ⊢ ( ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ∈ ( ℤ≥ ‘ ( ♯ ‘ 𝑆 ) ) → ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
21 19 20 syl ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ⊆ ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ 𝑇 ) ) ) )
22 15 21 fnssresd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( 𝑆 ++ 𝑇 ) ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
23 wrdfn ⊢ ( 𝑆 ∈ Word 𝐵 → 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
24 23 adantr ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
25 fvres ⊢ ( 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) → ( ( ( 𝑆 ++ 𝑇 ) ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 ++ 𝑇 ) ‘ 𝑘 ) )
26 25 adantl ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 ++ 𝑇 ) ‘ 𝑘 ) )
27 ccatval1 ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑘 ) = ( 𝑆 ‘ 𝑘 ) )
28 27 3expa ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ++ 𝑇 ) ‘ 𝑘 ) = ( 𝑆 ‘ 𝑘 ) )
29 26 28 eqtrd ⊢ ( ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) ∧ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( ( 𝑆 ++ 𝑇 ) ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ‘ 𝑘 ) = ( 𝑆 ‘ 𝑘 ) )
30 22 24 29 eqfnfvd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( 𝑆 ++ 𝑇 ) ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) = 𝑆 )
31 14 30 eqtrd ⊢ ( ( 𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ) → ( ( 𝑆 ++ 𝑇 ) prefix ( ♯ ‘ 𝑆 ) ) = 𝑆 )