Metamath Proof Explorer


Theorem pfxsuffeqwrdeq

Description: Two words are equal if and only if they have the same prefix and the same suffix. (Contributed by Alexander van der Vekens, 23-Sep-2018) (Revised by AV, 5-May-2020)

Ref Expression
Assertion pfxsuffeqwrdeq W Word V S Word V I 0 ..^ W W = S W = S W prefix I = S prefix I W substr I W = S substr I W

Proof

Step Hyp Ref Expression
1 eqwrd W Word V S Word V W = S W = S i 0 ..^ W W i = S i
2 1 3adant3 W Word V S Word V I 0 ..^ W W = S W = S i 0 ..^ W W i = S i
3 elfzofz I 0 ..^ W I 0 W
4 fzosplit I 0 W 0 ..^ W = 0 ..^ I I ..^ W
5 3 4 syl I 0 ..^ W 0 ..^ W = 0 ..^ I I ..^ W
6 5 3ad2ant3 W Word V S Word V I 0 ..^ W 0 ..^ W = 0 ..^ I I ..^ W
7 6 adantr W Word V S Word V I 0 ..^ W W = S 0 ..^ W = 0 ..^ I I ..^ W
8 7 raleqdv W Word V S Word V I 0 ..^ W W = S i 0 ..^ W W i = S i i 0 ..^ I I ..^ W W i = S i
9 ralunb i 0 ..^ I I ..^ W W i = S i i 0 ..^ I W i = S i i I ..^ W W i = S i
10 8 9 bitrdi W Word V S Word V I 0 ..^ W W = S i 0 ..^ W W i = S i i 0 ..^ I W i = S i i I ..^ W W i = S i
11 eqidd W Word V S Word V I 0 ..^ W W = S I = I
12 3simpa W Word V S Word V I 0 ..^ W W Word V S Word V
13 12 adantr W Word V S Word V I 0 ..^ W W = S W Word V S Word V
14 elfzonn0 I 0 ..^ W I 0
15 14 14 jca I 0 ..^ W I 0 I 0
16 15 3ad2ant3 W Word V S Word V I 0 ..^ W I 0 I 0
17 16 adantr W Word V S Word V I 0 ..^ W W = S I 0 I 0
18 elfzo0le I 0 ..^ W I W
19 18 3ad2ant3 W Word V S Word V I 0 ..^ W I W
20 19 adantr W Word V S Word V I 0 ..^ W W = S I W
21 breq2 W = S I W I S
22 21 adantl W Word V S Word V I 0 ..^ W W = S I W I S
23 20 22 mpbid W Word V S Word V I 0 ..^ W W = S I S
24 pfxeq W Word V S Word V I 0 I 0 I W I S W prefix I = S prefix I I = I i 0 ..^ I W i = S i
25 13 17 20 23 24 syl112anc W Word V S Word V I 0 ..^ W W = S W prefix I = S prefix I I = I i 0 ..^ I W i = S i
26 11 25 mpbirand W Word V S Word V I 0 ..^ W W = S W prefix I = S prefix I i 0 ..^ I W i = S i
27 lencl W Word V W 0
28 27 14 anim12ci W Word V I 0 ..^ W I 0 W 0
29 28 3adant2 W Word V S Word V I 0 ..^ W I 0 W 0
30 29 adantr W Word V S Word V I 0 ..^ W W = S I 0 W 0
31 27 nn0red W Word V W
32 31 leidd W Word V W W
33 32 adantr W Word V W = S W W
34 eqle W W = S W S
35 31 34 sylan W Word V W = S W S
36 33 35 jca W Word V W = S W W W S
37 36 3ad2antl1 W Word V S Word V I 0 ..^ W W = S W W W S
38 swrdspsleq W Word V S Word V I 0 W 0 W W W S W substr I W = S substr I W i I ..^ W W i = S i
39 13 30 37 38 syl3anc W Word V S Word V I 0 ..^ W W = S W substr I W = S substr I W i I ..^ W W i = S i
40 26 39 anbi12d W Word V S Word V I 0 ..^ W W = S W prefix I = S prefix I W substr I W = S substr I W i 0 ..^ I W i = S i i I ..^ W W i = S i
41 10 40 bitr4d W Word V S Word V I 0 ..^ W W = S i 0 ..^ W W i = S i W prefix I = S prefix I W substr I W = S substr I W
42 41 pm5.32da W Word V S Word V I 0 ..^ W W = S i 0 ..^ W W i = S i W = S W prefix I = S prefix I W substr I W = S substr I W
43 2 42 bitrd W Word V S Word V I 0 ..^ W W = S W = S W prefix I = S prefix I W substr I W = S substr I W