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 e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )

Proof

Step Hyp Ref Expression
1 ccatcl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( A ++ B ) e. Word V )
2 1 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) -> ( A ++ B ) e. Word V )
3 simprl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) -> M e. ( 0 ... N ) )
4 ccatlen 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
5 4 oveq2d 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( 0 ... ( # ` ( A ++ B ) ) ) = ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) )
6 5 eleq2d 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( # ` ( A ++ B ) ) ) <-> N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) )
7 6 biimpar 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) )
8 7 adantrl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) )
9 swrdvalfn 
 |-  ( ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
10 2 3 8 9 syl3anc 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )