Metamath Proof Explorer

Theorem pfxccatin12lem2

Description: Lemma 2 for pfxccatin12 . (Contributed by AV, 30-Mar-2018) (Revised by AV, 9-May-2020)

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

Proof

Step Hyp Ref Expression
1 swrdccatin2.l 
 |-  L = ( # ` A )
2 1 pfxccatin12lem2c 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )
3 simprl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> K e. ( 0 ..^ ( N - M ) ) )
4 swrdfv 
 |-  ( ( ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) /\ K e. ( 0 ..^ ( N - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( A ++ B ) ` ( K + M ) ) )
5 2 3 4 syl2an2r 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( A ++ B ) ` ( K + M ) ) )
6 elfzoelz 
 |-  ( K e. ( 0 ..^ ( N - M ) ) -> K e. ZZ )
7 elfz2nn0 
 |-  ( M e. ( 0 ... L ) <-> ( M e. NN0 /\ L e. NN0 /\ M <_ L ) )
8 nn0cn 
 |-  ( M e. NN0 -> M e. CC )
9 nn0cn 
 |-  ( L e. NN0 -> L e. CC )
10 8 9 anim12i 
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( M e. CC /\ L e. CC ) )
11 zcn 
 |-  ( K e. ZZ -> K e. CC )
12 subcl 
 |-  ( ( L e. CC /\ M e. CC ) -> ( L - M ) e. CC )
13 12 ancoms 
 |-  ( ( M e. CC /\ L e. CC ) -> ( L - M ) e. CC )
14 13 anim1ci 
 |-  ( ( ( M e. CC /\ L e. CC ) /\ K e. CC ) -> ( K e. CC /\ ( L - M ) e. CC ) )
15 subcl 
 |-  ( ( K e. CC /\ ( L - M ) e. CC ) -> ( K - ( L - M ) ) e. CC )
16 14 15 syl 
 |-  ( ( ( M e. CC /\ L e. CC ) /\ K e. CC ) -> ( K - ( L - M ) ) e. CC )
17 16 addridd 
 |-  ( ( ( M e. CC /\ L e. CC ) /\ K e. CC ) -> ( ( K - ( L - M ) ) + 0 ) = ( K - ( L - M ) ) )
18 simpr 
 |-  ( ( ( M e. CC /\ L e. CC ) /\ K e. CC ) -> K e. CC )
19 simplr 
 |-  ( ( ( M e. CC /\ L e. CC ) /\ K e. CC ) -> L e. CC )
20 simpll 
 |-  ( ( ( M e. CC /\ L e. CC ) /\ K e. CC ) -> M e. CC )
21 18 19 20 subsub3d 
 |-  ( ( ( M e. CC /\ L e. CC ) /\ K e. CC ) -> ( K - ( L - M ) ) = ( ( K + M ) - L ) )
22 17 21 eqtr2d 
 |-  ( ( ( M e. CC /\ L e. CC ) /\ K e. CC ) -> ( ( K + M ) - L ) = ( ( K - ( L - M ) ) + 0 ) )
23 10 11 22 syl2an 
 |-  ( ( ( M e. NN0 /\ L e. NN0 ) /\ K e. ZZ ) -> ( ( K + M ) - L ) = ( ( K - ( L - M ) ) + 0 ) )
24 oveq2 
 |-  ( ( # ` A ) = L -> ( ( K + M ) - ( # ` A ) ) = ( ( K + M ) - L ) )
25 24 eqcoms 
 |-  ( L = ( # ` A ) -> ( ( K + M ) - ( # ` A ) ) = ( ( K + M ) - L ) )
26 25 eqeq1d 
 |-  ( L = ( # ` A ) -> ( ( ( K + M ) - ( # ` A ) ) = ( ( K - ( L - M ) ) + 0 ) <-> ( ( K + M ) - L ) = ( ( K - ( L - M ) ) + 0 ) ) )
27 23 26 imbitrrid 
 |-  ( L = ( # ` A ) -> ( ( ( M e. NN0 /\ L e. NN0 ) /\ K e. ZZ ) -> ( ( K + M ) - ( # ` A ) ) = ( ( K - ( L - M ) ) + 0 ) ) )
28 1 27 ax-mp 
 |-  ( ( ( M e. NN0 /\ L e. NN0 ) /\ K e. ZZ ) -> ( ( K + M ) - ( # ` A ) ) = ( ( K - ( L - M ) ) + 0 ) )
29 28 ex 
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( K e. ZZ -> ( ( K + M ) - ( # ` A ) ) = ( ( K - ( L - M ) ) + 0 ) ) )
30 29 3adant3 
 |-  ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( K e. ZZ -> ( ( K + M ) - ( # ` A ) ) = ( ( K - ( L - M ) ) + 0 ) ) )
31 7 30 sylbi 
 |-  ( M e. ( 0 ... L ) -> ( K e. ZZ -> ( ( K + M ) - ( # ` A ) ) = ( ( K - ( L - M ) ) + 0 ) ) )
32 31 ad2antrl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( K e. ZZ -> ( ( K + M ) - ( # ` A ) ) = ( ( K - ( L - M ) ) + 0 ) ) )
33 6 32 syl5com 
 |-  ( K e. ( 0 ..^ ( N - M ) ) -> ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K + M ) - ( # ` A ) ) = ( ( K - ( L - M ) ) + 0 ) ) )
34 33 adantr 
 |-  ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K + M ) - ( # ` A ) ) = ( ( K - ( L - M ) ) + 0 ) ) )
35 34 impcom 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( K + M ) - ( # ` A ) ) = ( ( K - ( L - M ) ) + 0 ) )
36 35 fveq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( B ` ( ( K + M ) - ( # ` A ) ) ) = ( B ` ( ( K - ( L - M ) ) + 0 ) ) )
37 simpll 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( A e. Word V /\ B e. Word V ) )
38 pfxccatin12lem2a 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> ( K + M ) e. ( L ..^ ( L + ( # ` B ) ) ) ) )
39 38 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> ( K + M ) e. ( L ..^ ( L + ( # ` B ) ) ) ) )
40 39 imp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( K + M ) e. ( L ..^ ( L + ( # ` B ) ) ) )
41 id 
 |-  ( ( # ` A ) = L -> ( # ` A ) = L )
42 oveq1 
 |-  ( ( # ` A ) = L -> ( ( # ` A ) + ( # ` B ) ) = ( L + ( # ` B ) ) )
43 41 42 oveq12d 
 |-  ( ( # ` A ) = L -> ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) = ( L ..^ ( L + ( # ` B ) ) ) )
44 43 eleq2d 
 |-  ( ( # ` A ) = L -> ( ( K + M ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) <-> ( K + M ) e. ( L ..^ ( L + ( # ` B ) ) ) ) )
45 44 eqcoms 
 |-  ( L = ( # ` A ) -> ( ( K + M ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) <-> ( K + M ) e. ( L ..^ ( L + ( # ` B ) ) ) ) )
46 1 45 ax-mp 
 |-  ( ( K + M ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) <-> ( K + M ) e. ( L ..^ ( L + ( # ` B ) ) ) )
47 40 46 sylibr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( K + M ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) )
48 df-3an 
 |-  ( ( A e. Word V /\ B e. Word V /\ ( K + M ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) <-> ( ( A e. Word V /\ B e. Word V ) /\ ( K + M ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) )
49 37 47 48 sylanbrc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( A e. Word V /\ B e. Word V /\ ( K + M ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) )
50 ccatval2 
 |-  ( ( A e. Word V /\ B e. Word V /\ ( K + M ) e. ( ( # ` A ) ..^ ( ( # ` A ) + ( # ` B ) ) ) ) -> ( ( A ++ B ) ` ( K + M ) ) = ( B ` ( ( K + M ) - ( # ` A ) ) ) )
51 49 50 syl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( A ++ B ) ` ( K + M ) ) = ( B ` ( ( K + M ) - ( # ` A ) ) ) )
52 simplr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> B e. Word V )
53 52 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> B e. Word V )
54 lencl 
 |-  ( B e. Word V -> ( # ` B ) e. NN0 )
55 elfzel2 
 |-  ( M e. ( 0 ... L ) -> L e. ZZ )
56 zsubcl 
 |-  ( ( N e. ZZ /\ L e. ZZ ) -> ( N - L ) e. ZZ )
57 56 ancoms 
 |-  ( ( L e. ZZ /\ N e. ZZ ) -> ( N - L ) e. ZZ )
58 57 adantr 
 |-  ( ( ( L e. ZZ /\ N e. ZZ ) /\ L <_ N ) -> ( N - L ) e. ZZ )
59 zre 
 |-  ( N e. ZZ -> N e. RR )
60 zre 
 |-  ( L e. ZZ -> L e. RR )
61 subge0 
 |-  ( ( N e. RR /\ L e. RR ) -> ( 0 <_ ( N - L ) <-> L <_ N ) )
62 59 60 61 syl2anr 
 |-  ( ( L e. ZZ /\ N e. ZZ ) -> ( 0 <_ ( N - L ) <-> L <_ N ) )
63 62 biimprd 
 |-  ( ( L e. ZZ /\ N e. ZZ ) -> ( L <_ N -> 0 <_ ( N - L ) ) )
64 63 imp 
 |-  ( ( ( L e. ZZ /\ N e. ZZ ) /\ L <_ N ) -> 0 <_ ( N - L ) )
65 elnn0z 
 |-  ( ( N - L ) e. NN0 <-> ( ( N - L ) e. ZZ /\ 0 <_ ( N - L ) ) )
66 58 64 65 sylanbrc 
 |-  ( ( ( L e. ZZ /\ N e. ZZ ) /\ L <_ N ) -> ( N - L ) e. NN0 )
67 66 expcom 
 |-  ( L <_ N -> ( ( L e. ZZ /\ N e. ZZ ) -> ( N - L ) e. NN0 ) )
68 67 adantr 
 |-  ( ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) -> ( ( L e. ZZ /\ N e. ZZ ) -> ( N - L ) e. NN0 ) )
69 68 expcomd 
 |-  ( ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) -> ( N e. ZZ -> ( L e. ZZ -> ( N - L ) e. NN0 ) ) )
70 69 com12 
 |-  ( N e. ZZ -> ( ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) -> ( L e. ZZ -> ( N - L ) e. NN0 ) ) )
71 70 3ad2ant3 
 |-  ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) -> ( ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) -> ( L e. ZZ -> ( N - L ) e. NN0 ) ) )
72 71 imp 
 |-  ( ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) ) -> ( L e. ZZ -> ( N - L ) e. NN0 ) )
73 72 com12 
 |-  ( L e. ZZ -> ( ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) ) -> ( N - L ) e. NN0 ) )
74 73 adantr 
 |-  ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) -> ( ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) ) -> ( N - L ) e. NN0 ) )
75 74 imp 
 |-  ( ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) /\ ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) ) ) -> ( N - L ) e. NN0 )
76 simplr 
 |-  ( ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) /\ ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) ) ) -> ( # ` B ) e. NN0 )
77 59 3ad2ant3 
 |-  ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) -> N e. RR )
78 77 adantl 
 |-  ( ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) /\ ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) ) -> N e. RR )
79 60 adantr 
 |-  ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) -> L e. RR )
80 79 adantr 
 |-  ( ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) /\ ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) ) -> L e. RR )
81 nn0re 
 |-  ( ( # ` B ) e. NN0 -> ( # ` B ) e. RR )
82 81 adantl 
 |-  ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) -> ( # ` B ) e. RR )
83 82 adantr 
 |-  ( ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) /\ ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) ) -> ( # ` B ) e. RR )
84 lesubadd2 
 |-  ( ( N e. RR /\ L e. RR /\ ( # ` B ) e. RR ) -> ( ( N - L ) <_ ( # ` B ) <-> N <_ ( L + ( # ` B ) ) ) )
85 84 biimprd 
 |-  ( ( N e. RR /\ L e. RR /\ ( # ` B ) e. RR ) -> ( N <_ ( L + ( # ` B ) ) -> ( N - L ) <_ ( # ` B ) ) )
86 78 80 83 85 syl3anc 
 |-  ( ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) /\ ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) ) -> ( N <_ ( L + ( # ` B ) ) -> ( N - L ) <_ ( # ` B ) ) )
87 86 ex 
 |-  ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) -> ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) -> ( N <_ ( L + ( # ` B ) ) -> ( N - L ) <_ ( # ` B ) ) ) )
88 87 com13 
 |-  ( N <_ ( L + ( # ` B ) ) -> ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) -> ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) -> ( N - L ) <_ ( # ` B ) ) ) )
89 88 adantl 
 |-  ( ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) -> ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) -> ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) -> ( N - L ) <_ ( # ` B ) ) ) )
90 89 impcom 
 |-  ( ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) ) -> ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) -> ( N - L ) <_ ( # ` B ) ) )
91 90 impcom 
 |-  ( ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) /\ ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) ) ) -> ( N - L ) <_ ( # ` B ) )
92 75 76 91 3jca 
 |-  ( ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) /\ ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) ) ) -> ( ( N - L ) e. NN0 /\ ( # ` B ) e. NN0 /\ ( N - L ) <_ ( # ` B ) ) )
93 92 ex 
 |-  ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) -> ( ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) ) -> ( ( N - L ) e. NN0 /\ ( # ` B ) e. NN0 /\ ( N - L ) <_ ( # ` B ) ) ) )
94 elfz2 
 |-  ( N e. ( L ... ( L + ( # ` B ) ) ) <-> ( ( L e. ZZ /\ ( L + ( # ` B ) ) e. ZZ /\ N e. ZZ ) /\ ( L <_ N /\ N <_ ( L + ( # ` B ) ) ) ) )
95 elfz2nn0 
 |-  ( ( N - L ) e. ( 0 ... ( # ` B ) ) <-> ( ( N - L ) e. NN0 /\ ( # ` B ) e. NN0 /\ ( N - L ) <_ ( # ` B ) ) )
96 93 94 95 3imtr4g 
 |-  ( ( L e. ZZ /\ ( # ` B ) e. NN0 ) -> ( N e. ( L ... ( L + ( # ` B ) ) ) -> ( N - L ) e. ( 0 ... ( # ` B ) ) ) )
97 96 ex 
 |-  ( L e. ZZ -> ( ( # ` B ) e. NN0 -> ( N e. ( L ... ( L + ( # ` B ) ) ) -> ( N - L ) e. ( 0 ... ( # ` B ) ) ) ) )
98 97 com23 
 |-  ( L e. ZZ -> ( N e. ( L ... ( L + ( # ` B ) ) ) -> ( ( # ` B ) e. NN0 -> ( N - L ) e. ( 0 ... ( # ` B ) ) ) ) )
99 55 98 syl 
 |-  ( M e. ( 0 ... L ) -> ( N e. ( L ... ( L + ( # ` B ) ) ) -> ( ( # ` B ) e. NN0 -> ( N - L ) e. ( 0 ... ( # ` B ) ) ) ) )
100 99 imp 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( # ` B ) e. NN0 -> ( N - L ) e. ( 0 ... ( # ` B ) ) ) )
101 54 100 syl5com 
 |-  ( B e. Word V -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( N - L ) e. ( 0 ... ( # ` B ) ) ) )
102 101 adantl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( N - L ) e. ( 0 ... ( # ` B ) ) ) )
103 102 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( N - L ) e. ( 0 ... ( # ` B ) ) )
104 103 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( N - L ) e. ( 0 ... ( # ` B ) ) )
105 pfxccatin12lem1 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> ( K - ( L - M ) ) e. ( 0 ..^ ( N - L ) ) ) )
106 105 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> ( K - ( L - M ) ) e. ( 0 ..^ ( N - L ) ) ) )
107 106 imp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( K - ( L - M ) ) e. ( 0 ..^ ( N - L ) ) )
108 pfxfv 
 |-  ( ( B e. Word V /\ ( N - L ) e. ( 0 ... ( # ` B ) ) /\ ( K - ( L - M ) ) e. ( 0 ..^ ( N - L ) ) ) -> ( ( B prefix ( N - L ) ) ` ( K - ( L - M ) ) ) = ( B ` ( K - ( L - M ) ) ) )
109 53 104 107 108 syl3anc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( B prefix ( N - L ) ) ` ( K - ( L - M ) ) ) = ( B ` ( K - ( L - M ) ) ) )
110 6 zcnd 
 |-  ( K e. ( 0 ..^ ( N - M ) ) -> K e. CC )
111 110 ad2antrl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> K e. CC )
112 55 zcnd 
 |-  ( M e. ( 0 ... L ) -> L e. CC )
113 112 ad2antrl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> L e. CC )
114 113 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> L e. CC )
115 elfzelz 
 |-  ( M e. ( 0 ... L ) -> M e. ZZ )
116 115 zcnd 
 |-  ( M e. ( 0 ... L ) -> M e. CC )
117 116 ad2antrl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> M e. CC )
118 117 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> M e. CC )
119 114 118 subcld 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( L - M ) e. CC )
120 111 119 subcld 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( K - ( L - M ) ) e. CC )
121 120 addridd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( K - ( L - M ) ) + 0 ) = ( K - ( L - M ) ) )
122 121 eqcomd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( K - ( L - M ) ) = ( ( K - ( L - M ) ) + 0 ) )
123 122 fveq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( B ` ( K - ( L - M ) ) ) = ( B ` ( ( K - ( L - M ) ) + 0 ) ) )
124 109 123 eqtrd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( B prefix ( N - L ) ) ` ( K - ( L - M ) ) ) = ( B ` ( ( K - ( L - M ) ) + 0 ) ) )
125 36 51 124 3eqtr4d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( A ++ B ) ` ( K + M ) ) = ( ( B prefix ( N - L ) ) ` ( K - ( L - M ) ) ) )
126 simpll 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> A e. Word V )
127 simprl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> M e. ( 0 ... L ) )
128 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
129 elnn0uz 
 |-  ( ( # ` A ) e. NN0 <-> ( # ` A ) e. ( ZZ>= ` 0 ) )
130 eluzfz2 
 |-  ( ( # ` A ) e. ( ZZ>= ` 0 ) -> ( # ` A ) e. ( 0 ... ( # ` A ) ) )
131 129 130 sylbi 
 |-  ( ( # ` A ) e. NN0 -> ( # ` A ) e. ( 0 ... ( # ` A ) ) )
132 1 131 eqeltrid 
 |-  ( ( # ` A ) e. NN0 -> L e. ( 0 ... ( # ` A ) ) )
133 128 132 syl 
 |-  ( A e. Word V -> L e. ( 0 ... ( # ` A ) ) )
134 133 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> L e. ( 0 ... ( # ` A ) ) )
135 134 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> L e. ( 0 ... ( # ` A ) ) )
136 126 127 135 3jca 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( A e. Word V /\ M e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` A ) ) ) )
137 136 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( A e. Word V /\ M e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` A ) ) ) )
138 swrdlen 
 |-  ( ( A e. Word V /\ M e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` A ) ) ) -> ( # ` ( A substr <. M , L >. ) ) = ( L - M ) )
139 137 138 syl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( # ` ( A substr <. M , L >. ) ) = ( L - M ) )
140 139 eqcomd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( L - M ) = ( # ` ( A substr <. M , L >. ) ) )
141 140 oveq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( K - ( L - M ) ) = ( K - ( # ` ( A substr <. M , L >. ) ) ) )
142 141 fveq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( B prefix ( N - L ) ) ` ( K - ( L - M ) ) ) = ( ( B prefix ( N - L ) ) ` ( K - ( # ` ( A substr <. M , L >. ) ) ) ) )
143 5 125 142 3eqtrd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( B prefix ( N - L ) ) ` ( K - ( # ` ( A substr <. M , L >. ) ) ) ) )
144 143 ex 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( K e. ( 0 ..^ ( N - M ) ) /\ -. K e. ( 0 ..^ ( L - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( B prefix ( N - L ) ) ` ( K - ( # ` ( A substr <. M , L >. ) ) ) ) ) )