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

Proof

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