Metamath Proof Explorer

Theorem swrdccat3blem

Description: Lemma for swrdccat3b . (Contributed by AV, 30-May-2018)

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

Proof

Step Hyp Ref Expression
1 swrdccatin2.l 
 |-  L = ( # ` A )
2 lencl 
 |-  ( B e. Word V -> ( # ` B ) e. NN0 )
3 nn0le0eq0 
 |-  ( ( # ` B ) e. NN0 -> ( ( # ` B ) <_ 0 <-> ( # ` B ) = 0 ) )
4 3 biimpd 
 |-  ( ( # ` B ) e. NN0 -> ( ( # ` B ) <_ 0 -> ( # ` B ) = 0 ) )
5 2 4 syl 
 |-  ( B e. Word V -> ( ( # ` B ) <_ 0 -> ( # ` B ) = 0 ) )
6 5 adantl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( # ` B ) <_ 0 -> ( # ` B ) = 0 ) )
7 hasheq0 
 |-  ( B e. Word V -> ( ( # ` B ) = 0 <-> B = (/) ) )
8 7 biimpd 
 |-  ( B e. Word V -> ( ( # ` B ) = 0 -> B = (/) ) )
9 8 adantl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( # ` B ) = 0 -> B = (/) ) )
10 9 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` B ) = 0 ) -> B = (/) )
11 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
12 1 eqcomi 
 |-  ( # ` A ) = L
13 12 eleq1i 
 |-  ( ( # ` A ) e. NN0 <-> L e. NN0 )
14 nn0re 
 |-  ( L e. NN0 -> L e. RR )
15 elfz2nn0 
 |-  ( M e. ( 0 ... ( L + 0 ) ) <-> ( M e. NN0 /\ ( L + 0 ) e. NN0 /\ M <_ ( L + 0 ) ) )
16 recn 
 |-  ( L e. RR -> L e. CC )
17 16 addridd 
 |-  ( L e. RR -> ( L + 0 ) = L )
18 17 breq2d 
 |-  ( L e. RR -> ( M <_ ( L + 0 ) <-> M <_ L ) )
19 nn0re 
 |-  ( M e. NN0 -> M e. RR )
20 19 anim1i 
 |-  ( ( M e. NN0 /\ L e. RR ) -> ( M e. RR /\ L e. RR ) )
21 20 ancoms 
 |-  ( ( L e. RR /\ M e. NN0 ) -> ( M e. RR /\ L e. RR ) )
22 letri3 
 |-  ( ( M e. RR /\ L e. RR ) -> ( M = L <-> ( M <_ L /\ L <_ M ) ) )
23 21 22 syl 
 |-  ( ( L e. RR /\ M e. NN0 ) -> ( M = L <-> ( M <_ L /\ L <_ M ) ) )
24 23 biimprd 
 |-  ( ( L e. RR /\ M e. NN0 ) -> ( ( M <_ L /\ L <_ M ) -> M = L ) )
25 24 exp4b 
 |-  ( L e. RR -> ( M e. NN0 -> ( M <_ L -> ( L <_ M -> M = L ) ) ) )
26 25 com23 
 |-  ( L e. RR -> ( M <_ L -> ( M e. NN0 -> ( L <_ M -> M = L ) ) ) )
27 18 26 sylbid 
 |-  ( L e. RR -> ( M <_ ( L + 0 ) -> ( M e. NN0 -> ( L <_ M -> M = L ) ) ) )
28 27 com3l 
 |-  ( M <_ ( L + 0 ) -> ( M e. NN0 -> ( L e. RR -> ( L <_ M -> M = L ) ) ) )
29 28 impcom 
 |-  ( ( M e. NN0 /\ M <_ ( L + 0 ) ) -> ( L e. RR -> ( L <_ M -> M = L ) ) )
30 29 3adant2 
 |-  ( ( M e. NN0 /\ ( L + 0 ) e. NN0 /\ M <_ ( L + 0 ) ) -> ( L e. RR -> ( L <_ M -> M = L ) ) )
31 30 com12 
 |-  ( L e. RR -> ( ( M e. NN0 /\ ( L + 0 ) e. NN0 /\ M <_ ( L + 0 ) ) -> ( L <_ M -> M = L ) ) )
32 15 31 biimtrid 
 |-  ( L e. RR -> ( M e. ( 0 ... ( L + 0 ) ) -> ( L <_ M -> M = L ) ) )
33 14 32 syl 
 |-  ( L e. NN0 -> ( M e. ( 0 ... ( L + 0 ) ) -> ( L <_ M -> M = L ) ) )
34 13 33 sylbi 
 |-  ( ( # ` A ) e. NN0 -> ( M e. ( 0 ... ( L + 0 ) ) -> ( L <_ M -> M = L ) ) )
35 11 34 syl 
 |-  ( A e. Word V -> ( M e. ( 0 ... ( L + 0 ) ) -> ( L <_ M -> M = L ) ) )
36 35 imp 
 |-  ( ( A e. Word V /\ M e. ( 0 ... ( L + 0 ) ) ) -> ( L <_ M -> M = L ) )
37 elfznn0 
 |-  ( M e. ( 0 ... ( L + 0 ) ) -> M e. NN0 )
38 swrd00 
 |-  ( (/) substr <. 0 , 0 >. ) = (/)
39 swrd00 
 |-  ( A substr <. L , L >. ) = (/)
40 38 39 eqtr4i 
 |-  ( (/) substr <. 0 , 0 >. ) = ( A substr <. L , L >. )
41 nn0cn 
 |-  ( L e. NN0 -> L e. CC )
42 41 subidd 
 |-  ( L e. NN0 -> ( L - L ) = 0 )
43 42 opeq1d 
 |-  ( L e. NN0 -> <. ( L - L ) , 0 >. = <. 0 , 0 >. )
44 43 oveq2d 
 |-  ( L e. NN0 -> ( (/) substr <. ( L - L ) , 0 >. ) = ( (/) substr <. 0 , 0 >. ) )
45 41 addridd 
 |-  ( L e. NN0 -> ( L + 0 ) = L )
46 45 opeq2d 
 |-  ( L e. NN0 -> <. L , ( L + 0 ) >. = <. L , L >. )
47 46 oveq2d 
 |-  ( L e. NN0 -> ( A substr <. L , ( L + 0 ) >. ) = ( A substr <. L , L >. ) )
48 40 44 47 3eqtr4a 
 |-  ( L e. NN0 -> ( (/) substr <. ( L - L ) , 0 >. ) = ( A substr <. L , ( L + 0 ) >. ) )
49 48 a1i 
 |-  ( M = L -> ( L e. NN0 -> ( (/) substr <. ( L - L ) , 0 >. ) = ( A substr <. L , ( L + 0 ) >. ) ) )
50 eleq1 
 |-  ( M = L -> ( M e. NN0 <-> L e. NN0 ) )
51 oveq1 
 |-  ( M = L -> ( M - L ) = ( L - L ) )
52 51 opeq1d 
 |-  ( M = L -> <. ( M - L ) , 0 >. = <. ( L - L ) , 0 >. )
53 52 oveq2d 
 |-  ( M = L -> ( (/) substr <. ( M - L ) , 0 >. ) = ( (/) substr <. ( L - L ) , 0 >. ) )
54 opeq1 
 |-  ( M = L -> <. M , ( L + 0 ) >. = <. L , ( L + 0 ) >. )
55 54 oveq2d 
 |-  ( M = L -> ( A substr <. M , ( L + 0 ) >. ) = ( A substr <. L , ( L + 0 ) >. ) )
56 53 55 eqeq12d 
 |-  ( M = L -> ( ( (/) substr <. ( M - L ) , 0 >. ) = ( A substr <. M , ( L + 0 ) >. ) <-> ( (/) substr <. ( L - L ) , 0 >. ) = ( A substr <. L , ( L + 0 ) >. ) ) )
57 49 50 56 3imtr4d 
 |-  ( M = L -> ( M e. NN0 -> ( (/) substr <. ( M - L ) , 0 >. ) = ( A substr <. M , ( L + 0 ) >. ) ) )
58 57 com12 
 |-  ( M e. NN0 -> ( M = L -> ( (/) substr <. ( M - L ) , 0 >. ) = ( A substr <. M , ( L + 0 ) >. ) ) )
59 58 a1d 
 |-  ( M e. NN0 -> ( A e. Word V -> ( M = L -> ( (/) substr <. ( M - L ) , 0 >. ) = ( A substr <. M , ( L + 0 ) >. ) ) ) )
60 37 59 syl 
 |-  ( M e. ( 0 ... ( L + 0 ) ) -> ( A e. Word V -> ( M = L -> ( (/) substr <. ( M - L ) , 0 >. ) = ( A substr <. M , ( L + 0 ) >. ) ) ) )
61 60 impcom 
 |-  ( ( A e. Word V /\ M e. ( 0 ... ( L + 0 ) ) ) -> ( M = L -> ( (/) substr <. ( M - L ) , 0 >. ) = ( A substr <. M , ( L + 0 ) >. ) ) )
62 36 61 syld 
 |-  ( ( A e. Word V /\ M e. ( 0 ... ( L + 0 ) ) ) -> ( L <_ M -> ( (/) substr <. ( M - L ) , 0 >. ) = ( A substr <. M , ( L + 0 ) >. ) ) )
63 62 imp 
 |-  ( ( ( A e. Word V /\ M e. ( 0 ... ( L + 0 ) ) ) /\ L <_ M ) -> ( (/) substr <. ( M - L ) , 0 >. ) = ( A substr <. M , ( L + 0 ) >. ) )
64 swrdcl 
 |-  ( A e. Word V -> ( A substr <. M , L >. ) e. Word V )
65 ccatrid 
 |-  ( ( A substr <. M , L >. ) e. Word V -> ( ( A substr <. M , L >. ) ++ (/) ) = ( A substr <. M , L >. ) )
66 64 65 syl 
 |-  ( A e. Word V -> ( ( A substr <. M , L >. ) ++ (/) ) = ( A substr <. M , L >. ) )
67 13 41 sylbi 
 |-  ( ( # ` A ) e. NN0 -> L e. CC )
68 11 67 syl 
 |-  ( A e. Word V -> L e. CC )
69 addrid 
 |-  ( L e. CC -> ( L + 0 ) = L )
70 69 eqcomd 
 |-  ( L e. CC -> L = ( L + 0 ) )
71 68 70 syl 
 |-  ( A e. Word V -> L = ( L + 0 ) )
72 71 opeq2d 
 |-  ( A e. Word V -> <. M , L >. = <. M , ( L + 0 ) >. )
73 72 oveq2d 
 |-  ( A e. Word V -> ( A substr <. M , L >. ) = ( A substr <. M , ( L + 0 ) >. ) )
74 66 73 eqtrd 
 |-  ( A e. Word V -> ( ( A substr <. M , L >. ) ++ (/) ) = ( A substr <. M , ( L + 0 ) >. ) )
75 74 adantr 
 |-  ( ( A e. Word V /\ M e. ( 0 ... ( L + 0 ) ) ) -> ( ( A substr <. M , L >. ) ++ (/) ) = ( A substr <. M , ( L + 0 ) >. ) )
76 75 adantr 
 |-  ( ( ( A e. Word V /\ M e. ( 0 ... ( L + 0 ) ) ) /\ -. L <_ M ) -> ( ( A substr <. M , L >. ) ++ (/) ) = ( A substr <. M , ( L + 0 ) >. ) )
77 63 76 ifeqda 
 |-  ( ( A e. Word V /\ M e. ( 0 ... ( L + 0 ) ) ) -> if ( L <_ M , ( (/) substr <. ( M - L ) , 0 >. ) , ( ( A substr <. M , L >. ) ++ (/) ) ) = ( A substr <. M , ( L + 0 ) >. ) )
78 77 ex 
 |-  ( A e. Word V -> ( M e. ( 0 ... ( L + 0 ) ) -> if ( L <_ M , ( (/) substr <. ( M - L ) , 0 >. ) , ( ( A substr <. M , L >. ) ++ (/) ) ) = ( A substr <. M , ( L + 0 ) >. ) ) )
79 78 ad3antrrr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` B ) = 0 ) /\ B = (/) ) -> ( M e. ( 0 ... ( L + 0 ) ) -> if ( L <_ M , ( (/) substr <. ( M - L ) , 0 >. ) , ( ( A substr <. M , L >. ) ++ (/) ) ) = ( A substr <. M , ( L + 0 ) >. ) ) )
80 oveq2 
 |-  ( ( # ` B ) = 0 -> ( L + ( # ` B ) ) = ( L + 0 ) )
81 80 oveq2d 
 |-  ( ( # ` B ) = 0 -> ( 0 ... ( L + ( # ` B ) ) ) = ( 0 ... ( L + 0 ) ) )
82 81 eleq2d 
 |-  ( ( # ` B ) = 0 -> ( M e. ( 0 ... ( L + ( # ` B ) ) ) <-> M e. ( 0 ... ( L + 0 ) ) ) )
83 82 adantr 
 |-  ( ( ( # ` B ) = 0 /\ B = (/) ) -> ( M e. ( 0 ... ( L + ( # ` B ) ) ) <-> M e. ( 0 ... ( L + 0 ) ) ) )
84 simpr 
 |-  ( ( ( # ` B ) = 0 /\ B = (/) ) -> B = (/) )
85 opeq2 
 |-  ( ( # ` B ) = 0 -> <. ( M - L ) , ( # ` B ) >. = <. ( M - L ) , 0 >. )
86 85 adantr 
 |-  ( ( ( # ` B ) = 0 /\ B = (/) ) -> <. ( M - L ) , ( # ` B ) >. = <. ( M - L ) , 0 >. )
87 84 86 oveq12d 
 |-  ( ( ( # ` B ) = 0 /\ B = (/) ) -> ( B substr <. ( M - L ) , ( # ` B ) >. ) = ( (/) substr <. ( M - L ) , 0 >. ) )
88 oveq2 
 |-  ( B = (/) -> ( ( A substr <. M , L >. ) ++ B ) = ( ( A substr <. M , L >. ) ++ (/) ) )
89 88 adantl 
 |-  ( ( ( # ` B ) = 0 /\ B = (/) ) -> ( ( A substr <. M , L >. ) ++ B ) = ( ( A substr <. M , L >. ) ++ (/) ) )
90 87 89 ifeq12d 
 |-  ( ( ( # ` B ) = 0 /\ B = (/) ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = if ( L <_ M , ( (/) substr <. ( M - L ) , 0 >. ) , ( ( A substr <. M , L >. ) ++ (/) ) ) )
91 80 opeq2d 
 |-  ( ( # ` B ) = 0 -> <. M , ( L + ( # ` B ) ) >. = <. M , ( L + 0 ) >. )
92 91 oveq2d 
 |-  ( ( # ` B ) = 0 -> ( A substr <. M , ( L + ( # ` B ) ) >. ) = ( A substr <. M , ( L + 0 ) >. ) )
93 92 adantr 
 |-  ( ( ( # ` B ) = 0 /\ B = (/) ) -> ( A substr <. M , ( L + ( # ` B ) ) >. ) = ( A substr <. M , ( L + 0 ) >. ) )
94 90 93 eqeq12d 
 |-  ( ( ( # ` B ) = 0 /\ B = (/) ) -> ( if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) <-> if ( L <_ M , ( (/) substr <. ( M - L ) , 0 >. ) , ( ( A substr <. M , L >. ) ++ (/) ) ) = ( A substr <. M , ( L + 0 ) >. ) ) )
95 83 94 imbi12d 
 |-  ( ( ( # ` B ) = 0 /\ B = (/) ) -> ( ( M e. ( 0 ... ( L + ( # ` B ) ) ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) ) <-> ( M e. ( 0 ... ( L + 0 ) ) -> if ( L <_ M , ( (/) substr <. ( M - L ) , 0 >. ) , ( ( A substr <. M , L >. ) ++ (/) ) ) = ( A substr <. M , ( L + 0 ) >. ) ) ) )
96 95 adantll 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` B ) = 0 ) /\ B = (/) ) -> ( ( M e. ( 0 ... ( L + ( # ` B ) ) ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) ) <-> ( M e. ( 0 ... ( L + 0 ) ) -> if ( L <_ M , ( (/) substr <. ( M - L ) , 0 >. ) , ( ( A substr <. M , L >. ) ++ (/) ) ) = ( A substr <. M , ( L + 0 ) >. ) ) ) )
97 79 96 mpbird 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` B ) = 0 ) /\ B = (/) ) -> ( M e. ( 0 ... ( L + ( # ` B ) ) ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) ) )
98 10 97 mpdan 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( # ` B ) = 0 ) -> ( M e. ( 0 ... ( L + ( # ` B ) ) ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) ) )
99 98 ex 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( # ` B ) = 0 -> ( M e. ( 0 ... ( L + ( # ` B ) ) ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) ) ) )
100 6 99 syld 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( # ` B ) <_ 0 -> ( M e. ( 0 ... ( L + ( # ` B ) ) ) -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) ) ) )
101 100 com23 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( M e. ( 0 ... ( L + ( # ` B ) ) ) -> ( ( # ` B ) <_ 0 -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) ) ) )
102 101 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( # ` B ) <_ 0 -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) ) )
103 102 adantr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ ( L + ( # ` B ) ) <_ L ) -> ( ( # ` B ) <_ 0 -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) ) )
104 1 eleq1i 
 |-  ( L e. NN0 <-> ( # ` A ) e. NN0 )
105 104 14 sylbir 
 |-  ( ( # ` A ) e. NN0 -> L e. RR )
106 11 105 syl 
 |-  ( A e. Word V -> L e. RR )
107 2 nn0red 
 |-  ( B e. Word V -> ( # ` B ) e. RR )
108 leaddle0 
 |-  ( ( L e. RR /\ ( # ` B ) e. RR ) -> ( ( L + ( # ` B ) ) <_ L <-> ( # ` B ) <_ 0 ) )
109 106 107 108 syl2an 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( L + ( # ` B ) ) <_ L <-> ( # ` B ) <_ 0 ) )
110 pm2.24 
 |-  ( ( # ` B ) <_ 0 -> ( -. ( # ` B ) <_ 0 -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) ) )
111 109 110 biimtrdi 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( L + ( # ` B ) ) <_ L -> ( -. ( # ` B ) <_ 0 -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) ) ) )
112 111 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) -> ( ( L + ( # ` B ) ) <_ L -> ( -. ( # ` B ) <_ 0 -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) ) ) )
113 112 imp 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + ( # ` B ) ) ) ) /\ ( L + ( # ` B ) ) <_ L ) -> ( -. ( # ` B ) <_ 0 -> if ( L <_ M , ( B substr <. ( M - L ) , ( # ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + ( # ` B ) ) >. ) ) )
114 103 113 pm2.61d 
 |-  ( ( ( ( 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 ) ) >. ) )