Metamath Proof Explorer

Theorem pfxccatpfx2

Description: A prefix of a concatenation of two words being the first word concatenated with a prefix of the second word. (Contributed by AV, 10-May-2020)

Ref Expression
Hypotheses swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
pfxccatpfx2.m ⊢ 𝑀 = ( ♯ ‘ 𝐵 )
Assertion pfxccatpfx2 ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
2 pfxccatpfx2.m ⊢ 𝑀 = ( ♯ ‘ 𝐵 )
3 ccatcl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 )
4 3 3adant3 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 )
5 lencl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
6 1 5 eqeltrid ⊢ ( 𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℕ0 )
7 elfzuz ⊢ ( 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝐿 + 1 ) ) )
8 peano2nn0 ⊢ ( 𝐿 ∈ ℕ0 → ( 𝐿 + 1 ) ∈ ℕ0 )
9 8 anim1i ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐿 + 1 ) ) ) → ( ( 𝐿 + 1 ) ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐿 + 1 ) ) ) )
10 6 7 9 syl2an ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → ( ( 𝐿 + 1 ) ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐿 + 1 ) ) ) )
11 10 3adant2 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → ( ( 𝐿 + 1 ) ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐿 + 1 ) ) ) )
12 eluznn0 ⊢ ( ( ( 𝐿 + 1 ) ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝐿 + 1 ) ) ) → 𝑁 ∈ ℕ0 )
13 11 12 syl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → 𝑁 ∈ ℕ0 )
14 pfxval ⊢ ( ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( ( 𝐴 ++ 𝐵 ) substr ⟨ 0 , 𝑁 ⟩ ) )
15 4 13 14 syl2anc ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( ( 𝐴 ++ 𝐵 ) substr ⟨ 0 , 𝑁 ⟩ ) )
16 3simpa ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
17 6 3ad2ant1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → 𝐿 ∈ ℕ0 )
18 0elfz ⊢ ( 𝐿 ∈ ℕ0 → 0 ∈ ( 0 ... 𝐿 ) )
19 17 18 syl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → 0 ∈ ( 0 ... 𝐿 ) )
20 5 nn0zd ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℤ )
21 1 20 eqeltrid ⊢ ( 𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℤ )
22 21 adantr ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → 𝐿 ∈ ℤ )
23 uzid ⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ( ℤ≥ ‘ 𝐿 ) )
24 peano2uz ⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 𝐿 ) → ( 𝐿 + 1 ) ∈ ( ℤ≥ ‘ 𝐿 ) )
25 fzss1 ⊢ ( ( 𝐿 + 1 ) ∈ ( ℤ≥ ‘ 𝐿 ) → ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ⊆ ( 𝐿 ... ( 𝐿 + 𝑀 ) ) )
26 22 23 24 25 4syl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ⊆ ( 𝐿 ... ( 𝐿 + 𝑀 ) ) )
27 2 eqcomi ⊢ ( ♯ ‘ 𝐵 ) = 𝑀
28 27 oveq2i ⊢ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) = ( 𝐿 + 𝑀 )
29 28 oveq2i ⊢ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) = ( 𝐿 ... ( 𝐿 + 𝑀 ) )
30 26 29 sseqtrrdi ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ⊆ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
31 30 sseld ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
32 31 3impia ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
33 19 32 jca ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → ( 0 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
34 1 pfxccatin12 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 0 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 0 , 𝑁 ⟩ ) = ( ( 𝐴 substr ⟨ 0 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) )
35 16 33 34 sylc ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 0 , 𝑁 ⟩ ) = ( ( 𝐴 substr ⟨ 0 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) )
36 1 opeq2i ⊢ ⟨ 0 , 𝐿 ⟩ = ⟨ 0 , ( ♯ ‘ 𝐴 ) ⟩
37 36 oveq2i ⊢ ( 𝐴 substr ⟨ 0 , 𝐿 ⟩ ) = ( 𝐴 substr ⟨ 0 , ( ♯ ‘ 𝐴 ) ⟩ )
38 pfxval ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) → ( 𝐴 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐴 substr ⟨ 0 , ( ♯ ‘ 𝐴 ) ⟩ ) )
39 5 38 mpdan ⊢ ( 𝐴 ∈ Word 𝑉 → ( 𝐴 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐴 substr ⟨ 0 , ( ♯ ‘ 𝐴 ) ⟩ ) )
40 pfxid ⊢ ( 𝐴 ∈ Word 𝑉 → ( 𝐴 prefix ( ♯ ‘ 𝐴 ) ) = 𝐴 )
41 39 40 eqtr3d ⊢ ( 𝐴 ∈ Word 𝑉 → ( 𝐴 substr ⟨ 0 , ( ♯ ‘ 𝐴 ) ⟩ ) = 𝐴 )
42 37 41 eqtrid ⊢ ( 𝐴 ∈ Word 𝑉 → ( 𝐴 substr ⟨ 0 , 𝐿 ⟩ ) = 𝐴 )
43 42 3ad2ant1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → ( 𝐴 substr ⟨ 0 , 𝐿 ⟩ ) = 𝐴 )
44 43 oveq1d ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → ( ( 𝐴 substr ⟨ 0 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) = ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) )
45 15 35 44 3eqtrd ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( ( 𝐿 + 1 ) ... ( 𝐿 + 𝑀 ) ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( 𝐴 ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) )