Metamath Proof Explorer

Theorem pfxccatpfx1

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

Ref Expression
Hypothesis swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
Assertion pfxccatpfx1 ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( 𝐴 prefix 𝑁 ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
2 3simpa ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
3 elfznn0 ⊢ ( 𝑁 ∈ ( 0 ... 𝐿 ) → 𝑁 ∈ ℕ0 )
4 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
5 3 4 syl ⊢ ( 𝑁 ∈ ( 0 ... 𝐿 ) → 0 ∈ ( 0 ... 𝑁 ) )
6 1 oveq2i ⊢ ( 0 ... 𝐿 ) = ( 0 ... ( ♯ ‘ 𝐴 ) )
7 6 eleq2i ⊢ ( 𝑁 ∈ ( 0 ... 𝐿 ) ↔ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
8 7 biimpi ⊢ ( 𝑁 ∈ ( 0 ... 𝐿 ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
9 5 8 jca ⊢ ( 𝑁 ∈ ( 0 ... 𝐿 ) → ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) )
10 9 3ad2ant3 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) → ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) )
11 swrdccatin1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 0 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 0 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 0 , 𝑁 ⟩ ) ) )
12 2 10 11 sylc ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 0 , 𝑁 ⟩ ) = ( 𝐴 substr ⟨ 0 , 𝑁 ⟩ ) )
13 ccatcl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 )
14 13 3adant3 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) → ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 )
15 3 3ad2ant3 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) → 𝑁 ∈ ℕ0 )
16 14 15 jca ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) → ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) )
17 pfxval ⊢ ( ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( ( 𝐴 ++ 𝐵 ) substr ⟨ 0 , 𝑁 ⟩ ) )
18 16 17 syl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( ( 𝐴 ++ 𝐵 ) substr ⟨ 0 , 𝑁 ⟩ ) )
19 pfxval ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 prefix 𝑁 ) = ( 𝐴 substr ⟨ 0 , 𝑁 ⟩ ) )
20 3 19 sylan2 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) → ( 𝐴 prefix 𝑁 ) = ( 𝐴 substr ⟨ 0 , 𝑁 ⟩ ) )
21 20 3adant2 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) → ( 𝐴 prefix 𝑁 ) = ( 𝐴 substr ⟨ 0 , 𝑁 ⟩ ) )
22 12 18 21 3eqtr4d ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... 𝐿 ) ) → ( ( 𝐴 ++ 𝐵 ) prefix 𝑁 ) = ( 𝐴 prefix 𝑁 ) )