This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem swrdccat

Description: The subword of a concatenation of two words as concatenation of subwords of the two concatenated words. (Contributed by Alexander van der Vekens, 29-May-2018)

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

Proof

Step Hyp Ref Expression
1 swrdccatin2.l 
 |-  L = ( # ` A )
2 1 pfxccat3 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) )
3 2 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) )
4 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
5 4 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( # ` A ) e. NN0 )
6 1 eqcomi 
 |-  ( # ` A ) = L
7 6 eleq1i 
 |-  ( ( # ` A ) e. NN0 <-> L e. NN0 )
8 elfz2nn0 
 |-  ( M e. ( 0 ... N ) <-> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) )
9 iftrue 
 |-  ( N <_ L -> if ( N <_ L , N , L ) = N )
10 9 adantl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> if ( N <_ L , N , L ) = N )
11 10 opeq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> <. M , if ( N <_ L , N , L ) >. = <. M , N >. )
12 11 oveq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> ( A substr <. M , if ( N <_ L , N , L ) >. ) = ( A substr <. M , N >. ) )
13 iftrue 
 |-  ( 0 <_ ( M - L ) -> if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) = ( M - L ) )
14 13 opeq1d 
 |-  ( 0 <_ ( M - L ) -> <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. = <. ( M - L ) , ( N - L ) >. )
15 14 oveq2d 
 |-  ( 0 <_ ( M - L ) -> ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )
16 15 adantr 
 |-  ( ( 0 <_ ( M - L ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) ) -> ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )
17 simpr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> B e. Word V )
18 nn0z 
 |-  ( L e. NN0 -> L e. ZZ )
19 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
20 19 adantr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> M e. ZZ )
21 zsubcl 
 |-  ( ( M e. ZZ /\ L e. ZZ ) -> ( M - L ) e. ZZ )
22 20 21 sylan 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. ZZ ) -> ( M - L ) e. ZZ )
23 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
24 23 adantl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> N e. ZZ )
25 zsubcl 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( N - L ) e. ZZ )
26 24 25 sylan 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. ZZ ) -> ( N - L ) e. ZZ )
27 22 26 jca 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. ZZ ) -> ( ( M - L ) e. ZZ /\ ( N - L ) e. ZZ ) )
28 18 27 sylan2 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) -> ( ( M - L ) e. ZZ /\ ( N - L ) e. ZZ ) )
29 17 28 anim12i 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( B e. Word V /\ ( ( M - L ) e. ZZ /\ ( N - L ) e. ZZ ) ) )
30 3anass 
 |-  ( ( B e. Word V /\ ( M - L ) e. ZZ /\ ( N - L ) e. ZZ ) <-> ( B e. Word V /\ ( ( M - L ) e. ZZ /\ ( N - L ) e. ZZ ) ) )
31 29 30 sylibr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( B e. Word V /\ ( M - L ) e. ZZ /\ ( N - L ) e. ZZ ) )
32 31 ad2antrl 
 |-  ( ( 0 <_ ( M - L ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) ) -> ( B e. Word V /\ ( M - L ) e. ZZ /\ ( N - L ) e. ZZ ) )
33 nn0re 
 |-  ( M e. NN0 -> M e. RR )
34 nn0re 
 |-  ( N e. NN0 -> N e. RR )
35 33 34 anim12i 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M e. RR /\ N e. RR ) )
36 nn0re 
 |-  ( L e. NN0 -> L e. RR )
37 subge0 
 |-  ( ( M e. RR /\ L e. RR ) -> ( 0 <_ ( M - L ) <-> L <_ M ) )
38 37 adantlr 
 |-  ( ( ( M e. RR /\ N e. RR ) /\ L e. RR ) -> ( 0 <_ ( M - L ) <-> L <_ M ) )
39 simpr 
 |-  ( ( M e. RR /\ N e. RR ) -> N e. RR )
40 39 adantr 
 |-  ( ( ( M e. RR /\ N e. RR ) /\ L e. RR ) -> N e. RR )
41 simpr 
 |-  ( ( ( M e. RR /\ N e. RR ) /\ L e. RR ) -> L e. RR )
42 simpl 
 |-  ( ( M e. RR /\ N e. RR ) -> M e. RR )
43 42 adantr 
 |-  ( ( ( M e. RR /\ N e. RR ) /\ L e. RR ) -> M e. RR )
44 letr 
 |-  ( ( N e. RR /\ L e. RR /\ M e. RR ) -> ( ( N <_ L /\ L <_ M ) -> N <_ M ) )
45 40 41 43 44 syl3anc 
 |-  ( ( ( M e. RR /\ N e. RR ) /\ L e. RR ) -> ( ( N <_ L /\ L <_ M ) -> N <_ M ) )
46 45 expcomd 
 |-  ( ( ( M e. RR /\ N e. RR ) /\ L e. RR ) -> ( L <_ M -> ( N <_ L -> N <_ M ) ) )
47 38 46 sylbid 
 |-  ( ( ( M e. RR /\ N e. RR ) /\ L e. RR ) -> ( 0 <_ ( M - L ) -> ( N <_ L -> N <_ M ) ) )
48 47 com23 
 |-  ( ( ( M e. RR /\ N e. RR ) /\ L e. RR ) -> ( N <_ L -> ( 0 <_ ( M - L ) -> N <_ M ) ) )
49 35 36 48 syl2an 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) -> ( N <_ L -> ( 0 <_ ( M - L ) -> N <_ M ) ) )
50 49 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( N <_ L -> ( 0 <_ ( M - L ) -> N <_ M ) ) )
51 50 imp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> ( 0 <_ ( M - L ) -> N <_ M ) )
52 51 impcom 
 |-  ( ( 0 <_ ( M - L ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) ) -> N <_ M )
53 34 adantl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> N e. RR )
54 53 adantr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) -> N e. RR )
55 33 adantr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> M e. RR )
56 55 adantr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) -> M e. RR )
57 36 adantl 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) -> L e. RR )
58 54 56 57 3jca 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) -> ( N e. RR /\ M e. RR /\ L e. RR ) )
59 58 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( N e. RR /\ M e. RR /\ L e. RR ) )
60 59 ad2antrl 
 |-  ( ( 0 <_ ( M - L ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) ) -> ( N e. RR /\ M e. RR /\ L e. RR ) )
61 lesub1 
 |-  ( ( N e. RR /\ M e. RR /\ L e. RR ) -> ( N <_ M <-> ( N - L ) <_ ( M - L ) ) )
62 60 61 syl 
 |-  ( ( 0 <_ ( M - L ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) ) -> ( N <_ M <-> ( N - L ) <_ ( M - L ) ) )
63 52 62 mpbid 
 |-  ( ( 0 <_ ( M - L ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) ) -> ( N - L ) <_ ( M - L ) )
64 swrdlend 
 |-  ( ( B e. Word V /\ ( M - L ) e. ZZ /\ ( N - L ) e. ZZ ) -> ( ( N - L ) <_ ( M - L ) -> ( B substr <. ( M - L ) , ( N - L ) >. ) = (/) ) )
65 32 63 64 sylc 
 |-  ( ( 0 <_ ( M - L ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) ) -> ( B substr <. ( M - L ) , ( N - L ) >. ) = (/) )
66 16 65 eqtrd 
 |-  ( ( 0 <_ ( M - L ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) ) -> ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) = (/) )
67 iffalse 
 |-  ( -. 0 <_ ( M - L ) -> if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) = 0 )
68 67 opeq1d 
 |-  ( -. 0 <_ ( M - L ) -> <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. = <. 0 , ( N - L ) >. )
69 68 oveq2d 
 |-  ( -. 0 <_ ( M - L ) -> ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) = ( B substr <. 0 , ( N - L ) >. ) )
70 17 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> B e. Word V )
71 70 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> B e. Word V )
72 0zd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> 0 e. ZZ )
73 24 18 25 syl2an 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) -> ( N - L ) e. ZZ )
74 73 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( N - L ) e. ZZ )
75 74 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> ( N - L ) e. ZZ )
76 71 72 75 3jca 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> ( B e. Word V /\ 0 e. ZZ /\ ( N - L ) e. ZZ ) )
77 53 36 anim12i 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) -> ( N e. RR /\ L e. RR ) )
78 77 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( N e. RR /\ L e. RR ) )
79 suble0 
 |-  ( ( N e. RR /\ L e. RR ) -> ( ( N - L ) <_ 0 <-> N <_ L ) )
80 78 79 syl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( ( N - L ) <_ 0 <-> N <_ L ) )
81 80 biimpar 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> ( N - L ) <_ 0 )
82 swrdlend 
 |-  ( ( B e. Word V /\ 0 e. ZZ /\ ( N - L ) e. ZZ ) -> ( ( N - L ) <_ 0 -> ( B substr <. 0 , ( N - L ) >. ) = (/) ) )
83 76 81 82 sylc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> ( B substr <. 0 , ( N - L ) >. ) = (/) )
84 69 83 sylan9eq 
 |-  ( ( -. 0 <_ ( M - L ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) ) -> ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) = (/) )
85 66 84 pm2.61ian 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) = (/) )
86 12 85 oveq12d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = ( ( A substr <. M , N >. ) ++ (/) ) )
87 swrdcl 
 |-  ( A e. Word V -> ( A substr <. M , N >. ) e. Word V )
88 ccatrid 
 |-  ( ( A substr <. M , N >. ) e. Word V -> ( ( A substr <. M , N >. ) ++ (/) ) = ( A substr <. M , N >. ) )
89 87 88 syl 
 |-  ( A e. Word V -> ( ( A substr <. M , N >. ) ++ (/) ) = ( A substr <. M , N >. ) )
90 89 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( A substr <. M , N >. ) ++ (/) ) = ( A substr <. M , N >. ) )
91 90 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( ( A substr <. M , N >. ) ++ (/) ) = ( A substr <. M , N >. ) )
92 91 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> ( ( A substr <. M , N >. ) ++ (/) ) = ( A substr <. M , N >. ) )
93 86 92 eqtrd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ N <_ L ) -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = ( A substr <. M , N >. ) )
94 iffalse 
 |-  ( -. N <_ L -> if ( N <_ L , N , L ) = L )
95 94 3ad2ant2 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ L <_ M ) -> if ( N <_ L , N , L ) = L )
96 95 opeq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ L <_ M ) -> <. M , if ( N <_ L , N , L ) >. = <. M , L >. )
97 96 oveq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ L <_ M ) -> ( A substr <. M , if ( N <_ L , N , L ) >. ) = ( A substr <. M , L >. ) )
98 simpl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> A e. Word V )
99 98 20 18 3anim123i 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) -> ( A e. Word V /\ M e. ZZ /\ L e. ZZ ) )
100 99 3expb 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( A e. Word V /\ M e. ZZ /\ L e. ZZ ) )
101 swrdlend 
 |-  ( ( A e. Word V /\ M e. ZZ /\ L e. ZZ ) -> ( L <_ M -> ( A substr <. M , L >. ) = (/) ) )
102 100 101 syl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( L <_ M -> ( A substr <. M , L >. ) = (/) ) )
103 102 imp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ L <_ M ) -> ( A substr <. M , L >. ) = (/) )
104 103 3adant2 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ L <_ M ) -> ( A substr <. M , L >. ) = (/) )
105 97 104 eqtrd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ L <_ M ) -> ( A substr <. M , if ( N <_ L , N , L ) >. ) = (/) )
106 55 36 37 syl2an 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) -> ( 0 <_ ( M - L ) <-> L <_ M ) )
107 106 biimprd 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) -> ( L <_ M -> 0 <_ ( M - L ) ) )
108 107 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( L <_ M -> 0 <_ ( M - L ) ) )
109 108 imp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ L <_ M ) -> 0 <_ ( M - L ) )
110 109 3adant2 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ L <_ M ) -> 0 <_ ( M - L ) )
111 110 14 syl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ L <_ M ) -> <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. = <. ( M - L ) , ( N - L ) >. )
112 111 oveq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ L <_ M ) -> ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )
113 105 112 oveq12d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ L <_ M ) -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = ( (/) ++ ( B substr <. ( M - L ) , ( N - L ) >. ) ) )
114 swrdcl 
 |-  ( B e. Word V -> ( B substr <. ( M - L ) , ( N - L ) >. ) e. Word V )
115 114 adantl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( B substr <. ( M - L ) , ( N - L ) >. ) e. Word V )
116 ccatlid 
 |-  ( ( B substr <. ( M - L ) , ( N - L ) >. ) e. Word V -> ( (/) ++ ( B substr <. ( M - L ) , ( N - L ) >. ) ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )
117 115 116 syl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( (/) ++ ( B substr <. ( M - L ) , ( N - L ) >. ) ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )
118 117 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( (/) ++ ( B substr <. ( M - L ) , ( N - L ) >. ) ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )
119 118 3ad2ant1 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ L <_ M ) -> ( (/) ++ ( B substr <. ( M - L ) , ( N - L ) >. ) ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )
120 113 119 eqtrd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ L <_ M ) -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )
121 94 3ad2ant2 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ -. L <_ M ) -> if ( N <_ L , N , L ) = L )
122 121 opeq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ -. L <_ M ) -> <. M , if ( N <_ L , N , L ) >. = <. M , L >. )
123 122 oveq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ -. L <_ M ) -> ( A substr <. M , if ( N <_ L , N , L ) >. ) = ( A substr <. M , L >. ) )
124 33 36 37 syl2an 
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( 0 <_ ( M - L ) <-> L <_ M ) )
125 124 adantlr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) -> ( 0 <_ ( M - L ) <-> L <_ M ) )
126 125 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( 0 <_ ( M - L ) <-> L <_ M ) )
127 126 biimpd 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( 0 <_ ( M - L ) -> L <_ M ) )
128 127 con3dimp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. L <_ M ) -> -. 0 <_ ( M - L ) )
129 128 3adant2 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ -. L <_ M ) -> -. 0 <_ ( M - L ) )
130 129 67 syl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ -. L <_ M ) -> if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) = 0 )
131 130 opeq1d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ -. L <_ M ) -> <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. = <. 0 , ( N - L ) >. )
132 131 oveq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ -. L <_ M ) -> ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) = ( B substr <. 0 , ( N - L ) >. ) )
133 70 3ad2ant1 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ -. L <_ M ) -> B e. Word V )
134 simplrr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L ) -> L e. NN0 )
135 simprlr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> N e. NN0 )
136 135 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L ) -> N e. NN0 )
137 ltnle 
 |-  ( ( L e. RR /\ N e. RR ) -> ( L < N <-> -. N <_ L ) )
138 ltle 
 |-  ( ( L e. RR /\ N e. RR ) -> ( L < N -> L <_ N ) )
139 137 138 sylbird 
 |-  ( ( L e. RR /\ N e. RR ) -> ( -. N <_ L -> L <_ N ) )
140 36 53 139 syl2anr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) -> ( -. N <_ L -> L <_ N ) )
141 140 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( -. N <_ L -> L <_ N ) )
142 141 imp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L ) -> L <_ N )
143 nn0sub2 
 |-  ( ( L e. NN0 /\ N e. NN0 /\ L <_ N ) -> ( N - L ) e. NN0 )
144 134 136 142 143 syl3anc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L ) -> ( N - L ) e. NN0 )
145 144 3adant3 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ -. L <_ M ) -> ( N - L ) e. NN0 )
146 133 145 jca 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ -. L <_ M ) -> ( B e. Word V /\ ( N - L ) e. NN0 ) )
147 pfxval 
 |-  ( ( B e. Word V /\ ( N - L ) e. NN0 ) -> ( B prefix ( N - L ) ) = ( B substr <. 0 , ( N - L ) >. ) )
148 146 147 syl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ -. L <_ M ) -> ( B prefix ( N - L ) ) = ( B substr <. 0 , ( N - L ) >. ) )
149 132 148 eqtr4d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ -. L <_ M ) -> ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) = ( B prefix ( N - L ) ) )
150 123 149 oveq12d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) /\ -. N <_ L /\ -. L <_ M ) -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) )
151 93 120 150 2if2 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( ( M e. NN0 /\ N e. NN0 ) /\ L e. NN0 ) ) -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) )
152 151 exp32 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. NN0 /\ N e. NN0 ) -> ( L e. NN0 -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) ) )
153 152 com12 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( ( A e. Word V /\ B e. Word V ) -> ( L e. NN0 -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) ) )
154 153 3adant3 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( ( A e. Word V /\ B e. Word V ) -> ( L e. NN0 -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) ) )
155 8 154 sylbi 
 |-  ( M e. ( 0 ... N ) -> ( ( A e. Word V /\ B e. Word V ) -> ( L e. NN0 -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) ) )
156 155 adantr 
 |-  ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A e. Word V /\ B e. Word V ) -> ( L e. NN0 -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) ) )
157 156 com13 
 |-  ( L e. NN0 -> ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) ) )
158 7 157 sylbi 
 |-  ( ( # ` A ) e. NN0 -> ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) ) )
159 5 158 mpcom 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) )
160 159 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) -> ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) )
161 3 160 eqtr4d 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) )
162 161 ex 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) ) )