Metamath Proof Explorer

Theorem pfxeq

Description: The prefixes of two words are equal iff they have the same length and the same symbols at each position. (Contributed by Alexander van der Vekens, 7-Aug-2018) (Revised by AV, 4-May-2020)

Ref Expression
Assertion pfxeq 
|- ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( W prefix M ) = ( U prefix N ) <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( W ` i ) = ( U ` i ) ) ) )

Proof

Step Hyp Ref Expression
1 pfxcl 
 |-  ( W e. Word V -> ( W prefix M ) e. Word V )
2 pfxcl 
 |-  ( U e. Word V -> ( U prefix N ) e. Word V )
3 eqwrd 
 |-  ( ( ( W prefix M ) e. Word V /\ ( U prefix N ) e. Word V ) -> ( ( W prefix M ) = ( U prefix N ) <-> ( ( # ` ( W prefix M ) ) = ( # ` ( U prefix N ) ) /\ A. i e. ( 0 ..^ ( # ` ( W prefix M ) ) ) ( ( W prefix M ) ` i ) = ( ( U prefix N ) ` i ) ) ) )
4 1 2 3 syl2an 
 |-  ( ( W e. Word V /\ U e. Word V ) -> ( ( W prefix M ) = ( U prefix N ) <-> ( ( # ` ( W prefix M ) ) = ( # ` ( U prefix N ) ) /\ A. i e. ( 0 ..^ ( # ` ( W prefix M ) ) ) ( ( W prefix M ) ` i ) = ( ( U prefix N ) ` i ) ) ) )
5 4 3ad2ant2 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( W prefix M ) = ( U prefix N ) <-> ( ( # ` ( W prefix M ) ) = ( # ` ( U prefix N ) ) /\ A. i e. ( 0 ..^ ( # ` ( W prefix M ) ) ) ( ( W prefix M ) ` i ) = ( ( U prefix N ) ` i ) ) ) )
6 simp2l 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> W e. Word V )
7 simpl 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> M e. NN0 )
8 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
9 8 adantr 
 |-  ( ( W e. Word V /\ U e. Word V ) -> ( # ` W ) e. NN0 )
10 simpl 
 |-  ( ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) -> M <_ ( # ` W ) )
11 7 9 10 3anim123i 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( M e. NN0 /\ ( # ` W ) e. NN0 /\ M <_ ( # ` W ) ) )
12 elfz2nn0 
 |-  ( M e. ( 0 ... ( # ` W ) ) <-> ( M e. NN0 /\ ( # ` W ) e. NN0 /\ M <_ ( # ` W ) ) )
13 11 12 sylibr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> M e. ( 0 ... ( # ` W ) ) )
14 pfxlen 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W prefix M ) ) = M )
15 6 13 14 syl2anc 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( # ` ( W prefix M ) ) = M )
16 simp2r 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> U e. Word V )
17 simpr 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> N e. NN0 )
18 lencl 
 |-  ( U e. Word V -> ( # ` U ) e. NN0 )
19 18 adantl 
 |-  ( ( W e. Word V /\ U e. Word V ) -> ( # ` U ) e. NN0 )
20 simpr 
 |-  ( ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) -> N <_ ( # ` U ) )
21 17 19 20 3anim123i 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( N e. NN0 /\ ( # ` U ) e. NN0 /\ N <_ ( # ` U ) ) )
22 elfz2nn0 
 |-  ( N e. ( 0 ... ( # ` U ) ) <-> ( N e. NN0 /\ ( # ` U ) e. NN0 /\ N <_ ( # ` U ) ) )
23 21 22 sylibr 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> N e. ( 0 ... ( # ` U ) ) )
24 pfxlen 
 |-  ( ( U e. Word V /\ N e. ( 0 ... ( # ` U ) ) ) -> ( # ` ( U prefix N ) ) = N )
25 16 23 24 syl2anc 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( # ` ( U prefix N ) ) = N )
26 15 25 eqeq12d 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( # ` ( W prefix M ) ) = ( # ` ( U prefix N ) ) <-> M = N ) )
27 26 anbi1d 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( ( # ` ( W prefix M ) ) = ( # ` ( U prefix N ) ) /\ A. i e. ( 0 ..^ ( # ` ( W prefix M ) ) ) ( ( W prefix M ) ` i ) = ( ( U prefix N ) ` i ) ) <-> ( M = N /\ A. i e. ( 0 ..^ ( # ` ( W prefix M ) ) ) ( ( W prefix M ) ` i ) = ( ( U prefix N ) ` i ) ) ) )
28 15 adantr 
 |-  ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) -> ( # ` ( W prefix M ) ) = M )
29 28 oveq2d 
 |-  ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) -> ( 0 ..^ ( # ` ( W prefix M ) ) ) = ( 0 ..^ M ) )
30 29 raleqdv 
 |-  ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) -> ( A. i e. ( 0 ..^ ( # ` ( W prefix M ) ) ) ( ( W prefix M ) ` i ) = ( ( U prefix N ) ` i ) <-> A. i e. ( 0 ..^ M ) ( ( W prefix M ) ` i ) = ( ( U prefix N ) ` i ) ) )
31 6 ad2antrr 
 |-  ( ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) /\ i e. ( 0 ..^ M ) ) -> W e. Word V )
32 13 ad2antrr 
 |-  ( ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) /\ i e. ( 0 ..^ M ) ) -> M e. ( 0 ... ( # ` W ) ) )
33 simpr 
 |-  ( ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ M ) )
34 pfxfv 
 |-  ( ( W e. Word V /\ M e. ( 0 ... ( # ` W ) ) /\ i e. ( 0 ..^ M ) ) -> ( ( W prefix M ) ` i ) = ( W ` i ) )
35 31 32 33 34 syl3anc 
 |-  ( ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) /\ i e. ( 0 ..^ M ) ) -> ( ( W prefix M ) ` i ) = ( W ` i ) )
36 16 ad2antrr 
 |-  ( ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) /\ i e. ( 0 ..^ M ) ) -> U e. Word V )
37 23 ad2antrr 
 |-  ( ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) /\ i e. ( 0 ..^ M ) ) -> N e. ( 0 ... ( # ` U ) ) )
38 oveq2 
 |-  ( M = N -> ( 0 ..^ M ) = ( 0 ..^ N ) )
39 38 eleq2d 
 |-  ( M = N -> ( i e. ( 0 ..^ M ) <-> i e. ( 0 ..^ N ) ) )
40 39 adantl 
 |-  ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) -> ( i e. ( 0 ..^ M ) <-> i e. ( 0 ..^ N ) ) )
41 40 biimpa 
 |-  ( ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ..^ N ) )
42 pfxfv 
 |-  ( ( U e. Word V /\ N e. ( 0 ... ( # ` U ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( U prefix N ) ` i ) = ( U ` i ) )
43 36 37 41 42 syl3anc 
 |-  ( ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) /\ i e. ( 0 ..^ M ) ) -> ( ( U prefix N ) ` i ) = ( U ` i ) )
44 35 43 eqeq12d 
 |-  ( ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) /\ i e. ( 0 ..^ M ) ) -> ( ( ( W prefix M ) ` i ) = ( ( U prefix N ) ` i ) <-> ( W ` i ) = ( U ` i ) ) )
45 44 ralbidva 
 |-  ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) -> ( A. i e. ( 0 ..^ M ) ( ( W prefix M ) ` i ) = ( ( U prefix N ) ` i ) <-> A. i e. ( 0 ..^ M ) ( W ` i ) = ( U ` i ) ) )
46 30 45 bitrd 
 |-  ( ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) /\ M = N ) -> ( A. i e. ( 0 ..^ ( # ` ( W prefix M ) ) ) ( ( W prefix M ) ` i ) = ( ( U prefix N ) ` i ) <-> A. i e. ( 0 ..^ M ) ( W ` i ) = ( U ` i ) ) )
47 46 pm5.32da 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( M = N /\ A. i e. ( 0 ..^ ( # ` ( W prefix M ) ) ) ( ( W prefix M ) ` i ) = ( ( U prefix N ) ` i ) ) <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( W ` i ) = ( U ` i ) ) ) )
48 5 27 47 3bitrd 
 |-  ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( W e. Word V /\ U e. Word V ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( W prefix M ) = ( U prefix N ) <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( W ` i ) = ( U ` i ) ) ) )
49 48 3com12 
 |-  ( ( ( W e. Word V /\ U e. Word V ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( M <_ ( # ` W ) /\ N <_ ( # ` U ) ) ) -> ( ( W prefix M ) = ( U prefix N ) <-> ( M = N /\ A. i e. ( 0 ..^ M ) ( W ` i ) = ( U ` i ) ) ) )