Metamath Proof Explorer

Theorem swrdccat2

Description: Recover the right half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Assertion swrdccat2 ⊢ S ∈ Word B ∧ T ∈ Word B → S ++ T substr S S + T = T

Proof

Step Hyp Ref Expression
1 ccatcl ⊢ S ∈ Word B ∧ T ∈ Word B → S ++ T ∈ Word B
2 swrdcl ⊢ S ++ T ∈ Word B → S ++ T substr S S + T ∈ Word B
3 wrdfn ⊢ S ++ T substr S S + T ∈ Word B → S ++ T substr S S + T Fn 0 ..^ S ++ T substr S S + T
4 1 2 3 3syl ⊢ S ∈ Word B ∧ T ∈ Word B → S ++ T substr S S + T Fn 0 ..^ S ++ T substr S S + T
5 lencl ⊢ S ∈ Word B → S ∈ ℕ 0
6 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
7 5 6 eleqtrdi ⊢ S ∈ Word B → S ∈ ℤ ≥ 0
8 7 adantr ⊢ S ∈ Word B ∧ T ∈ Word B → S ∈ ℤ ≥ 0
9 5 nn0zd ⊢ S ∈ Word B → S ∈ ℤ
10 9 uzidd ⊢ S ∈ Word B → S ∈ ℤ ≥ S
11 lencl ⊢ T ∈ Word B → T ∈ ℕ 0
12 uzaddcl ⊢ S ∈ ℤ ≥ S ∧ T ∈ ℕ 0 → S + T ∈ ℤ ≥ S
13 10 11 12 syl2an ⊢ S ∈ Word B ∧ T ∈ Word B → S + T ∈ ℤ ≥ S
14 elfzuzb ⊢ S ∈ 0 … S + T ↔ S ∈ ℤ ≥ 0 ∧ S + T ∈ ℤ ≥ S
15 8 13 14 sylanbrc ⊢ S ∈ Word B ∧ T ∈ Word B → S ∈ 0 … S + T
16 nn0addcl ⊢ S ∈ ℕ 0 ∧ T ∈ ℕ 0 → S + T ∈ ℕ 0
17 5 11 16 syl2an ⊢ S ∈ Word B ∧ T ∈ Word B → S + T ∈ ℕ 0
18 17 6 eleqtrdi ⊢ S ∈ Word B ∧ T ∈ Word B → S + T ∈ ℤ ≥ 0
19 17 nn0zd ⊢ S ∈ Word B ∧ T ∈ Word B → S + T ∈ ℤ
20 19 uzidd ⊢ S ∈ Word B ∧ T ∈ Word B → S + T ∈ ℤ ≥ S + T
21 elfzuzb ⊢ S + T ∈ 0 … S + T ↔ S + T ∈ ℤ ≥ 0 ∧ S + T ∈ ℤ ≥ S + T
22 18 20 21 sylanbrc ⊢ S ∈ Word B ∧ T ∈ Word B → S + T ∈ 0 … S + T
23 ccatlen ⊢ S ∈ Word B ∧ T ∈ Word B → S ++ T = S + T
24 23 oveq2d ⊢ S ∈ Word B ∧ T ∈ Word B → 0 … S ++ T = 0 … S + T
25 22 24 eleqtrrd ⊢ S ∈ Word B ∧ T ∈ Word B → S + T ∈ 0 … S ++ T
26 swrdlen ⊢ S ++ T ∈ Word B ∧ S ∈ 0 … S + T ∧ S + T ∈ 0 … S ++ T → S ++ T substr S S + T = S + T - S
27 1 15 25 26 syl3anc ⊢ S ∈ Word B ∧ T ∈ Word B → S ++ T substr S S + T = S + T - S
28 5 nn0cnd ⊢ S ∈ Word B → S ∈ ℂ
29 11 nn0cnd ⊢ T ∈ Word B → T ∈ ℂ
30 pncan2 ⊢ S ∈ ℂ ∧ T ∈ ℂ → S + T - S = T
31 28 29 30 syl2an ⊢ S ∈ Word B ∧ T ∈ Word B → S + T - S = T
32 27 31 eqtrd ⊢ S ∈ Word B ∧ T ∈ Word B → S ++ T substr S S + T = T
33 32 oveq2d ⊢ S ∈ Word B ∧ T ∈ Word B → 0 ..^ S ++ T substr S S + T = 0 ..^ T
34 33 fneq2d ⊢ S ∈ Word B ∧ T ∈ Word B → S ++ T substr S S + T Fn 0 ..^ S ++ T substr S S + T ↔ S ++ T substr S S + T Fn 0 ..^ T
35 4 34 mpbid ⊢ S ∈ Word B ∧ T ∈ Word B → S ++ T substr S S + T Fn 0 ..^ T
36 wrdfn ⊢ T ∈ Word B → T Fn 0 ..^ T
37 36 adantl ⊢ S ∈ Word B ∧ T ∈ Word B → T Fn 0 ..^ T
38 1 15 25 3jca ⊢ S ∈ Word B ∧ T ∈ Word B → S ++ T ∈ Word B ∧ S ∈ 0 … S + T ∧ S + T ∈ 0 … S ++ T
39 31 oveq2d ⊢ S ∈ Word B ∧ T ∈ Word B → 0 ..^ S + T - S = 0 ..^ T
40 39 eleq2d ⊢ S ∈ Word B ∧ T ∈ Word B → k ∈ 0 ..^ S + T - S ↔ k ∈ 0 ..^ T
41 40 biimpar ⊢ S ∈ Word B ∧ T ∈ Word B ∧ k ∈ 0 ..^ T → k ∈ 0 ..^ S + T - S
42 swrdfv ⊢ S ++ T ∈ Word B ∧ S ∈ 0 … S + T ∧ S + T ∈ 0 … S ++ T ∧ k ∈ 0 ..^ S + T - S → S ++ T substr S S + T ⁡ k = S ++ T ⁡ k + S
43 38 41 42 syl2an2r ⊢ S ∈ Word B ∧ T ∈ Word B ∧ k ∈ 0 ..^ T → S ++ T substr S S + T ⁡ k = S ++ T ⁡ k + S
44 ccatval3 ⊢ S ∈ Word B ∧ T ∈ Word B ∧ k ∈ 0 ..^ T → S ++ T ⁡ k + S = T ⁡ k
45 44 3expa ⊢ S ∈ Word B ∧ T ∈ Word B ∧ k ∈ 0 ..^ T → S ++ T ⁡ k + S = T ⁡ k
46 43 45 eqtrd ⊢ S ∈ Word B ∧ T ∈ Word B ∧ k ∈ 0 ..^ T → S ++ T substr S S + T ⁡ k = T ⁡ k
47 35 37 46 eqfnfvd ⊢ S ∈ Word B ∧ T ∈ Word B → S ++ T substr S S + T = T