# Metamath Proof Explorer

## Theorem swrdccatfn

Description: The subword of a concatenation as function. (Contributed by Alexander van der Vekens, 27-May-2018)

Ref Expression
Assertion swrdccatfn ( ( ( 𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁𝑀 ) ) )

### Proof

Step Hyp Ref Expression
1 ccatcl ( ( 𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ) → ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 )
2 1 adantr ( ( ( 𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 )
3 simprl ( ( ( 𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ) → 𝑀 ∈ ( 0 ... 𝑁 ) )
4 ccatlen ( ( 𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ) → ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) = ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) )
5 4 eqcomd ( ( 𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ) → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) = ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) )
6 5 oveq2d ( ( 𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ) → ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) = ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) )
7 6 eleq2d ( ( 𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ) → ( 𝑁 ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↔ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) ) )
8 7 biimpcd ( 𝑁 ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) ) )
9 8 adantl ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) ) )
10 9 impcom ( ( ( 𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ) → 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) )
11 swrdvalfn ( ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁𝑀 ) ) )
12 2 3 10 11 syl3anc ( ( ( 𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) Fn ( 0 ..^ ( 𝑁𝑀 ) ) )