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

Metamath Proof Explorer

Theorem pfxccat3

Description: The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 30-Mar-2018) (Revised by AV, 10-May-2020)

Ref Expression
Hypothesis swrdccatin2.l 
|- L = ( # ` A )
Assertion 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 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l 
 |-  L = ( # ` A )
2 simpll 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ N <_ L ) -> ( A e. Word V /\ B e. Word V ) )
3 simplrl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ N <_ L ) -> M e. ( 0 ... N ) )
4 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
5 elfznn0 
 |-  ( N e. ( 0 ... ( L + ( # ` B ) ) ) -> N e. NN0 )
6 5 adantr 
 |-  ( ( N e. ( 0 ... ( L + ( # ` B ) ) ) /\ ( # ` A ) e. NN0 ) -> N e. NN0 )
7 6 adantr 
 |-  ( ( ( N e. ( 0 ... ( L + ( # ` B ) ) ) /\ ( # ` A ) e. NN0 ) /\ N <_ L ) -> N e. NN0 )
8 simplr 
 |-  ( ( ( N e. ( 0 ... ( L + ( # ` B ) ) ) /\ ( # ` A ) e. NN0 ) /\ N <_ L ) -> ( # ` A ) e. NN0 )
9 1 breq2i 
 |-  ( N <_ L <-> N <_ ( # ` A ) )
10 9 biimpi 
 |-  ( N <_ L -> N <_ ( # ` A ) )
11 10 adantl 
 |-  ( ( ( N e. ( 0 ... ( L + ( # ` B ) ) ) /\ ( # ` A ) e. NN0 ) /\ N <_ L ) -> N <_ ( # ` A ) )
12 elfz2nn0 
 |-  ( N e. ( 0 ... ( # ` A ) ) <-> ( N e. NN0 /\ ( # ` A ) e. NN0 /\ N <_ ( # ` A ) ) )
13 7 8 11 12 syl3anbrc 
 |-  ( ( ( N e. ( 0 ... ( L + ( # ` B ) ) ) /\ ( # ` A ) e. NN0 ) /\ N <_ L ) -> N e. ( 0 ... ( # ` A ) ) )
14 13 exp31 
 |-  ( N e. ( 0 ... ( L + ( # ` B ) ) ) -> ( ( # ` A ) e. NN0 -> ( N <_ L -> N e. ( 0 ... ( # ` A ) ) ) ) )
15 14 adantl 
 |-  ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( # ` A ) e. NN0 -> ( N <_ L -> N e. ( 0 ... ( # ` A ) ) ) ) )
16 4 15 syl5com 
 |-  ( A e. Word V -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( N <_ L -> N e. ( 0 ... ( # ` A ) ) ) ) )
17 16 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( N <_ L -> N e. ( 0 ... ( # ` A ) ) ) ) )
18 17 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) -> ( N <_ L -> N e. ( 0 ... ( # ` A ) ) ) )
19 18 imp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ N <_ L ) -> N e. ( 0 ... ( # ` A ) ) )
20 3 19 jca 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ N <_ L ) -> ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) )
21 swrdccatin1 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` A ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) ) )
22 2 20 21 sylc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ N <_ L ) -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) )
23 simp1l 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ -. N <_ L /\ L <_ M ) -> ( A e. Word V /\ B e. Word V ) )
24 1 eleq1i 
 |-  ( L e. NN0 <-> ( # ` A ) e. NN0 )
25 elfz2nn0 
 |-  ( M e. ( 0 ... N ) <-> ( M e. NN0 /\ N e. NN0 /\ M <_ N ) )
26 nn0z 
 |-  ( L e. NN0 -> L e. ZZ )
27 26 adantl 
 |-  ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ L e. NN0 ) -> L e. ZZ )
28 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
29 28 3ad2ant2 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> N e. ZZ )
30 29 adantr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ L e. NN0 ) -> N e. ZZ )
31 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
32 31 3ad2ant1 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> M e. ZZ )
33 32 adantr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ L e. NN0 ) -> M e. ZZ )
34 27 30 33 3jca 
 |-  ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ L e. NN0 ) -> ( L e. ZZ /\ N e. ZZ /\ M e. ZZ ) )
35 34 adantr 
 |-  ( ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ L e. NN0 ) /\ L <_ M ) -> ( L e. ZZ /\ N e. ZZ /\ M e. ZZ ) )
36 simpl3 
 |-  ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ L e. NN0 ) -> M <_ N )
37 36 anim1ci 
 |-  ( ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ L e. NN0 ) /\ L <_ M ) -> ( L <_ M /\ M <_ N ) )
38 elfz2 
 |-  ( M e. ( L ... N ) <-> ( ( L e. ZZ /\ N e. ZZ /\ M e. ZZ ) /\ ( L <_ M /\ M <_ N ) ) )
39 35 37 38 sylanbrc 
 |-  ( ( ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) /\ L e. NN0 ) /\ L <_ M ) -> M e. ( L ... N ) )
40 39 exp31 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( L e. NN0 -> ( L <_ M -> M e. ( L ... N ) ) ) )
41 25 40 sylbi 
 |-  ( M e. ( 0 ... N ) -> ( L e. NN0 -> ( L <_ M -> M e. ( L ... N ) ) ) )
42 41 adantr 
 |-  ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( L e. NN0 -> ( L <_ M -> M e. ( L ... N ) ) ) )
43 42 com12 
 |-  ( L e. NN0 -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( L <_ M -> M e. ( L ... N ) ) ) )
44 24 43 sylbir 
 |-  ( ( # ` A ) e. NN0 -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( L <_ M -> M e. ( L ... N ) ) ) )
45 4 44 syl 
 |-  ( A e. Word V -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( L <_ M -> M e. ( L ... N ) ) ) )
46 45 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( L <_ M -> M e. ( L ... N ) ) ) )
47 46 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) -> ( L <_ M -> M e. ( L ... N ) ) )
48 47 a1d 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) -> ( -. N <_ L -> ( L <_ M -> M e. ( L ... N ) ) ) )
49 48 3imp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ -. N <_ L /\ L <_ M ) -> M e. ( L ... N ) )
50 elfz2nn0 
 |-  ( N e. ( 0 ... ( L + ( # ` B ) ) ) <-> ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) )
51 nn0z 
 |-  ( ( # ` A ) e. NN0 -> ( # ` A ) e. ZZ )
52 1 51 eqeltrid 
 |-  ( ( # ` A ) e. NN0 -> L e. ZZ )
53 52 adantr 
 |-  ( ( ( # ` A ) e. NN0 /\ -. N <_ L ) -> L e. ZZ )
54 53 adantl 
 |-  ( ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) /\ ( ( # ` A ) e. NN0 /\ -. N <_ L ) ) -> L e. ZZ )
55 nn0z 
 |-  ( ( L + ( # ` B ) ) e. NN0 -> ( L + ( # ` B ) ) e. ZZ )
56 55 3ad2ant2 
 |-  ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) -> ( L + ( # ` B ) ) e. ZZ )
57 56 adantr 
 |-  ( ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) /\ ( ( # ` A ) e. NN0 /\ -. N <_ L ) ) -> ( L + ( # ` B ) ) e. ZZ )
58 28 3ad2ant1 
 |-  ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) -> N e. ZZ )
59 58 adantr 
 |-  ( ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) /\ ( ( # ` A ) e. NN0 /\ -. N <_ L ) ) -> N e. ZZ )
60 54 57 59 3jca 
 |-  ( ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) /\ ( ( # ` A ) e. NN0 /\ -. N <_ L ) ) -> ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) )
61 1 eqcomi 
 |-  ( # ` A ) = L
62 61 eleq1i 
 |-  ( ( # ` A ) e. NN0 <-> L e. NN0 )
63 nn0re 
 |-  ( L e. NN0 -> L e. RR )
64 nn0re 
 |-  ( N e. NN0 -> N e. RR )
65 ltnle 
 |-  ( ( L e. RR /\ N e. RR ) -> ( L < N <-> -. N <_ L ) )
66 63 64 65 syl2anr 
 |-  ( ( N e. NN0 /\ L e. NN0 ) -> ( L < N <-> -. N <_ L ) )
67 66 bicomd 
 |-  ( ( N e. NN0 /\ L e. NN0 ) -> ( -. N <_ L <-> L < N ) )
68 ltle 
 |-  ( ( L e. RR /\ N e. RR ) -> ( L < N -> L <_ N ) )
69 63 64 68 syl2anr 
 |-  ( ( N e. NN0 /\ L e. NN0 ) -> ( L < N -> L <_ N ) )
70 67 69 sylbid 
 |-  ( ( N e. NN0 /\ L e. NN0 ) -> ( -. N <_ L -> L <_ N ) )
71 70 ex 
 |-  ( N e. NN0 -> ( L e. NN0 -> ( -. N <_ L -> L <_ N ) ) )
72 62 71 biimtrid 
 |-  ( N e. NN0 -> ( ( # ` A ) e. NN0 -> ( -. N <_ L -> L <_ N ) ) )
73 72 3ad2ant1 
 |-  ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) -> ( ( # ` A ) e. NN0 -> ( -. N <_ L -> L <_ N ) ) )
74 73 imp32 
 |-  ( ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) /\ ( ( # ` A ) e. NN0 /\ -. N <_ L ) ) -> L <_ N )
75 simpl3 
 |-  ( ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) /\ ( ( # ` A ) e. NN0 /\ -. N <_ L ) ) -> N <_ ( L + ( # ` B ) ) )
76 74 75 jca 
 |-  ( ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) /\ ( ( # ` A ) e. NN0 /\ -. N <_ L ) ) -> ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) )
77 elfz2 
 |-  ( N e. ( L ... ( L + ( # ` B ) ) ) <-> ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) ) )
78 60 76 77 sylanbrc 
 |-  ( ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) /\ ( ( # ` A ) e. NN0 /\ -. N <_ L ) ) -> N e. ( L ... ( L + ( # ` B ) ) ) )
79 78 exp32 
 |-  ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) -> ( ( # ` A ) e. NN0 -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
80 50 79 sylbi 
 |-  ( N e. ( 0 ... ( L + ( # ` B ) ) ) -> ( ( # ` A ) e. NN0 -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
81 80 adantl 
 |-  ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( # ` A ) e. NN0 -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
82 4 81 syl5com 
 |-  ( A e. Word V -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
83 82 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
84 83 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) )
85 84 a1dd 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) -> ( -. N <_ L -> ( L <_ M -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
86 85 3imp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ -. N <_ L /\ L <_ M ) -> N e. ( L ... ( L + ( # ` B ) ) ) )
87 49 86 jca 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ -. N <_ L /\ L <_ M ) -> ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) )
88 1 swrdccatin2 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) ) )
89 23 87 88 sylc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ -. N <_ L /\ L <_ M ) -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )
90 simp1l 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ -. N <_ L /\ -. L <_ M ) -> ( A e. Word V /\ B e. Word V ) )
91 nn0re 
 |-  ( M e. NN0 -> M e. RR )
92 91 adantr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> M e. RR )
93 ltnle 
 |-  ( ( M e. RR /\ L e. RR ) -> ( M < L <-> -. L <_ M ) )
94 92 63 93 syl2anr 
 |-  ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( M < L <-> -. L <_ M ) )
95 94 bicomd 
 |-  ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( -. L <_ M <-> M < L ) )
96 simpll 
 |-  ( ( ( M e. NN0 /\ L e. NN0 ) /\ M < L ) -> M e. NN0 )
97 simplr 
 |-  ( ( ( M e. NN0 /\ L e. NN0 ) /\ M < L ) -> L e. NN0 )
98 ltle 
 |-  ( ( M e. RR /\ L e. RR ) -> ( M < L -> M <_ L ) )
99 91 63 98 syl2an 
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( M < L -> M <_ L ) )
100 99 imp 
 |-  ( ( ( M e. NN0 /\ L e. NN0 ) /\ M < L ) -> M <_ L )
101 elfz2nn0 
 |-  ( M e. ( 0 ... L ) <-> ( M e. NN0 /\ L e. NN0 /\ M <_ L ) )
102 96 97 100 101 syl3anbrc 
 |-  ( ( ( M e. NN0 /\ L e. NN0 ) /\ M < L ) -> M e. ( 0 ... L ) )
103 102 exp31 
 |-  ( M e. NN0 -> ( L e. NN0 -> ( M < L -> M e. ( 0 ... L ) ) ) )
104 103 adantr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( L e. NN0 -> ( M < L -> M e. ( 0 ... L ) ) ) )
105 104 impcom 
 |-  ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( M < L -> M e. ( 0 ... L ) ) )
106 95 105 sylbid 
 |-  ( ( L e. NN0 /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( -. L <_ M -> M e. ( 0 ... L ) ) )
107 106 expcom 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( L e. NN0 -> ( -. L <_ M -> M e. ( 0 ... L ) ) ) )
108 107 3adant3 
 |-  ( ( M e. NN0 /\ N e. NN0 /\ M <_ N ) -> ( L e. NN0 -> ( -. L <_ M -> M e. ( 0 ... L ) ) ) )
109 25 108 sylbi 
 |-  ( M e. ( 0 ... N ) -> ( L e. NN0 -> ( -. L <_ M -> M e. ( 0 ... L ) ) ) )
110 62 109 biimtrid 
 |-  ( M e. ( 0 ... N ) -> ( ( # ` A ) e. NN0 -> ( -. L <_ M -> M e. ( 0 ... L ) ) ) )
111 110 adantr 
 |-  ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( # ` A ) e. NN0 -> ( -. L <_ M -> M e. ( 0 ... L ) ) ) )
112 4 111 syl5com 
 |-  ( A e. Word V -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( -. L <_ M -> M e. ( 0 ... L ) ) ) )
113 112 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( -. L <_ M -> M e. ( 0 ... L ) ) ) )
114 113 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) -> ( -. L <_ M -> M e. ( 0 ... L ) ) )
115 114 a1d 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) -> ( -. N <_ L -> ( -. L <_ M -> M e. ( 0 ... L ) ) ) )
116 115 3imp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ -. N <_ L /\ -. L <_ M ) -> M e. ( 0 ... L ) )
117 64 3ad2ant1 
 |-  ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) -> N e. RR )
118 65 bicomd 
 |-  ( ( L e. RR /\ N e. RR ) -> ( -. N <_ L <-> L < N ) )
119 63 117 118 syl2an 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) ) -> ( -. N <_ L <-> L < N ) )
120 26 adantr 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) ) -> L e. ZZ )
121 56 adantl 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) ) -> ( L + ( # ` B ) ) e. ZZ )
122 58 adantl 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) ) -> N e. ZZ )
123 120 121 122 3jca 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) ) -> ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) )
124 123 adantr 
 |-  ( ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) ) /\ L < N ) -> ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) )
125 63 117 68 syl2an 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) ) -> ( L < N -> L <_ N ) )
126 125 imp 
 |-  ( ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) ) /\ L < N ) -> L <_ N )
127 simplr3 
 |-  ( ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) ) /\ L < N ) -> N <_ ( L + ( # ` B ) ) )
128 126 127 jca 
 |-  ( ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) ) /\ L < N ) -> ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) )
129 124 128 77 sylanbrc 
 |-  ( ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) ) /\ L < N ) -> N e. ( L ... ( L + ( # ` B ) ) ) )
130 129 ex 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) ) -> ( L < N -> N e. ( L ... ( L + ( # ` B ) ) ) ) )
131 119 130 sylbid 
 |-  ( ( L e. NN0 /\ ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) ) -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) )
132 131 ex 
 |-  ( L e. NN0 -> ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
133 62 132 sylbi 
 |-  ( ( # ` A ) e. NN0 -> ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
134 4 133 syl 
 |-  ( A e. Word V -> ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
135 134 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
136 135 com12 
 |-  ( ( N e. NN0 /\ ( L + ( # ` B ) ) e. NN0 /\ N <_ ( L + ( # ` B ) ) ) -> ( ( A e. Word V /\ B e. Word V ) -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
137 50 136 sylbi 
 |-  ( N e. ( 0 ... ( L + ( # ` B ) ) ) -> ( ( A e. Word V /\ B e. Word V ) -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
138 137 adantl 
 |-  ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( A e. Word V /\ B e. Word V ) -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
139 138 impcom 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) -> ( -. N <_ L -> N e. ( L ... ( L + ( # ` B ) ) ) ) )
140 139 a1dd 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) -> ( -. N <_ L -> ( -. L <_ M -> N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
141 140 3imp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ -. N <_ L /\ -. L <_ M ) -> N e. ( L ... ( L + ( # ` B ) ) ) )
142 116 141 jca 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ -. N <_ L /\ -. L <_ M ) -> ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) )
143 1 pfxccatin12 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) )
144 90 142 143 sylc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + ( # ` B ) ) ) ) ) /\ -. N <_ L /\ -. L <_ M ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) )
145 22 89 144 2if2 
 |-  ( ( ( 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 ) ) ) ) ) )
146 145 ex 
 |-  ( ( 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 ) ) ) ) ) ) )