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∈WordV∧B∈WordV→M∈0…N∧N∈0…L+B→A++BsubstrMN=ifN≤LAsubstrMNifL≤MBsubstrM−LN−LAsubstrML++BprefixN−L

Proof

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