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 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … N ∧ N ∈ 0 … A + B → A ++ B substr M N Fn 0 ..^ N − M

Proof

Step Hyp Ref Expression
1 ccatcl ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B ∈ Word V
2 1 adantr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … N ∧ N ∈ 0 … A + B → A ++ B ∈ Word V
3 simprl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … N ∧ N ∈ 0 … A + B → M ∈ 0 … N
4 ccatlen ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B = A + B
5 4 oveq2d ⊢ A ∈ Word V ∧ B ∈ Word V → 0 … A ++ B = 0 … A + B
6 5 eleq2d ⊢ A ∈ Word V ∧ B ∈ Word V → N ∈ 0 … A ++ B ↔ N ∈ 0 … A + B
7 6 biimpar ⊢ A ∈ Word V ∧ B ∈ Word V ∧ N ∈ 0 … A + B → N ∈ 0 … A ++ B
8 7 adantrl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … N ∧ N ∈ 0 … A + B → N ∈ 0 … A ++ B
9 swrdvalfn ⊢ A ++ B ∈ Word V ∧ M ∈ 0 … N ∧ N ∈ 0 … A ++ B → A ++ B substr M N Fn 0 ..^ N − M
10 2 3 8 9 syl3anc ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … N ∧ N ∈ 0 … A + B → A ++ B substr M N Fn 0 ..^ N − M