Metamath Proof Explorer

Theorem swrdccat3b

Description: A suffix of a concatenation is either a suffix of the second concatenated word or a concatenation of a suffix of the first word with the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018) (Revised by Alexander van der Vekens, 30-May-2018) (Proof shortened by AV, 14-Oct-2022)

Ref Expression
Hypothesis swrdccatin2.l 
|- L = ( # ` A )
Assertion swrdccat3b 
|- ( ( A e. Word V /\ B e. Word V ) -> ( M e. ( 0 ... ( L + ( # ` B ) ) ) -> ( ( A ++ B ) substr <. M , ( L + ( # ` B ) ) >. ) = if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l 
 |-  L = ( # ` A )
2 simpl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( A e. Word V /\ B e. Word V ) )
3 simpr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) -> M e. ( 0 ... ( L + ( # ` B ) ) ) )
4 elfzubelfz 
 |-  ( M e. ( 0 ... ( L + ( # ` B ) ) ) -> ( L + ( # ` B ) ) e. ( 0 ... ( L + ( # ` B ) ) ) )
5 4 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( L + ( # ` B ) ) e. ( 0 ... ( L + ( # ` B ) ) ) )
6 1 pfxccat3 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... ( L + ( # ` B ) ) ) /\ ( L + ( # ` B ) ) e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , ( L + ( # ` B ) ) >. ) = if ( ( L + ( # ` B ) ) <_ L , ( A substr <. M , ( L + ( # ` B ) ) >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( ( L + ( # ` B ) ) - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( ( L + ( # ` B ) ) - L ) ) ) ) ) ) )
7 6 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... ( L + ( # ` B ) ) ) /\ ( L + ( # ` B ) ) e. ( 0 ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) substr <. M , ( L + ( # ` B ) ) >. ) = if ( ( L + ( # ` B ) ) <_ L , ( A substr <. M , ( L + ( # ` B ) ) >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( ( L + ( # ` B ) ) - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( ( L + ( # ` B ) ) - L ) ) ) ) ) )
8 2 3 5 7 syl12anc 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , ( L + ( # ` B ) ) >. ) = if ( ( L + ( # ` B ) ) <_ L , ( A substr <. M , ( L + ( # ` B ) ) >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( ( L + ( # ` B ) ) - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( ( L + ( # ` B ) ) - L ) ) ) ) ) )
9 1 swrdccat3blem 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ ( L + ( # ` B ) ) <_ L ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) )
10 iftrue 
 |-  ( L <_ M -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( B substr <. ( M - L ) , ( # ` B ) >. ) )
11 10 3ad2ant3 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ -. ( L + ( # ` B ) ) <_ L /\ L <_ M ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( B substr <. ( M - L ) , ( # ` B ) >. ) )
12 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
13 12 nn0cnd 
 |-  ( A e. Word V -> ( # ` A ) e. CC )
14 lencl 
 |-  ( B e. Word V -> ( # ` B ) e. NN0 )
15 14 nn0cnd 
 |-  ( B e. Word V -> ( # ` B ) e. CC )
16 1 eqcomi 
 |-  ( # ` A ) = L
17 16 eleq1i 
 |-  ( ( # ` A ) e. CC <-> L e. CC )
18 pncan2 
 |-  ( ( L e. CC /\ ( # ` B ) e. CC ) -> ( ( L + ( # ` B ) ) - L ) = ( # ` B ) )
19 17 18 sylanb 
 |-  ( ( ( # ` A ) e. CC /\ ( # ` B ) e. CC ) -> ( ( L + ( # ` B ) ) - L ) = ( # ` B ) )
20 13 15 19 syl2an 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( L + ( # ` B ) ) - L ) = ( # ` B ) )
21 20 eqcomd 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( # ` B ) = ( ( L + ( # ` B ) ) - L ) )
22 21 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( # ` B ) = ( ( L + ( # ` B ) ) - L ) )
23 22 3ad2ant1 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ -. ( L + ( # ` B ) ) <_ L /\ L <_ M ) -> ( # ` B ) = ( ( L + ( # ` B ) ) - L ) )
24 23 opeq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ -. ( L + ( # ` B ) ) <_ L /\ L <_ M ) -> <. ( M - L ) , ( # ` B ) >. = <. ( M - L ) , ( ( L + ( # ` B ) ) - L ) >. )
25 24 oveq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ -. ( L + ( # ` B ) ) <_ L /\ L <_ M ) -> ( B substr <. ( M - L ) , ( # ` B ) >. ) = ( B substr <. ( M - L ) , ( ( L + ( # ` B ) ) - L ) >. ) )
26 11 25 eqtrd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ -. ( L + ( # ` B ) ) <_ L /\ L <_ M ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( B substr <. ( M - L ) , ( ( L + ( # ` B ) ) - L ) >. ) )
27 iffalse 
 |-  ( -. L <_ M -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( ( A substr <. M , L >. ) ++ B ) )
28 27 3ad2ant3 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ -. ( L + ( # ` B ) ) <_ L /\ -. L <_ M ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( ( A substr <. M , L >. ) ++ B ) )
29 20 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( L + ( # ` B ) ) - L ) = ( # ` B ) )
30 29 3ad2ant1 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ -. ( L + ( # ` B ) ) <_ L /\ -. L <_ M ) -> ( ( L + ( # ` B ) ) - L ) = ( # ` B ) )
31 30 oveq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ -. ( L + ( # ` B ) ) <_ L /\ -. L <_ M ) -> ( B prefix ( ( L + ( # ` B ) ) - L ) ) = ( B prefix ( # ` B ) ) )
32 pfxid 
 |-  ( B e. Word V -> ( B prefix ( # ` B ) ) = B )
33 32 adantl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( B prefix ( # ` B ) ) = B )
34 33 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( B prefix ( # ` B ) ) = B )
35 34 3ad2ant1 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ -. ( L + ( # ` B ) ) <_ L /\ -. L <_ M ) -> ( B prefix ( # ` B ) ) = B )
36 31 35 eqtr2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ -. ( L + ( # ` B ) ) <_ L /\ -. L <_ M ) -> B = ( B prefix ( ( L + ( # ` B ) ) - L ) ) )
37 36 oveq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ -. ( L + ( # ` B ) ) <_ L /\ -. L <_ M ) -> ( ( A substr <. M , L >. ) ++ B ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( ( L + ( # ` B ) ) - L ) ) ) )
38 28 37 eqtrd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ -. ( L + ( # ` B ) ) <_ L /\ -. L <_ M ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( ( L + ( # ` B ) ) - L ) ) ) )
39 9 26 38 2if2 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = if ( ( L + ( # ` B ) ) <_ L , ( A substr <. M , ( L + ( # ` B ) ) >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( ( L + ( # ` B ) ) - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( ( L + ( # ` B ) ) - L ) ) ) ) ) )
40 8 39 eqtr4d 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , ( L + ( # ` B ) ) >. ) = if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) )
41 40 ex 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( M e. ( 0 ... ( L + ( # ` B ) ) ) -> ( ( A ++ B ) substr <. M , ( L + ( # ` B ) ) >. ) = if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) ) )