Metamath Proof Explorer

Theorem eqwrds3

Description: A word is equal with a length 3 string iff it has length 3 and the same symbol at each position. (Contributed by AV, 12-May-2021)

Ref Expression
Assertion eqwrds3 
|- ( ( W e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( W = <" A B C "> <-> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = A /\ ( W ` 1 ) = B /\ ( W ` 2 ) = C ) ) ) )

Proof

Step Hyp Ref Expression
1 s3cl 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> <" A B C "> e. Word V )
2 eqwrd 
 |-  ( ( W e. Word V /\ <" A B C "> e. Word V ) -> ( W = <" A B C "> <-> ( ( # ` W ) = ( # ` <" A B C "> ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( <" A B C "> ` i ) ) ) )
3 1 2 sylan2 
 |-  ( ( W e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( W = <" A B C "> <-> ( ( # ` W ) = ( # ` <" A B C "> ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( <" A B C "> ` i ) ) ) )
4 s3len 
 |-  ( # ` <" A B C "> ) = 3
5 4 eqeq2i 
 |-  ( ( # ` W ) = ( # ` <" A B C "> ) <-> ( # ` W ) = 3 )
6 5 a1i 
 |-  ( ( W e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( # ` W ) = ( # ` <" A B C "> ) <-> ( # ` W ) = 3 ) )
7 6 anbi1d 
 |-  ( ( W e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( ( # ` W ) = ( # ` <" A B C "> ) /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( <" A B C "> ` i ) ) <-> ( ( # ` W ) = 3 /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( <" A B C "> ` i ) ) ) )
8 oveq2 
 |-  ( ( # ` W ) = 3 -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ 3 ) )
9 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
10 8 9 eqtrdi 
 |-  ( ( # ` W ) = 3 -> ( 0 ..^ ( # ` W ) ) = { 0 , 1 , 2 } )
11 10 raleqdv 
 |-  ( ( # ` W ) = 3 -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( <" A B C "> ` i ) <-> A. i e. { 0 , 1 , 2 } ( W ` i ) = ( <" A B C "> ` i ) ) )
12 fveq2 
 |-  ( i = 0 -> ( W ` i ) = ( W ` 0 ) )
13 fveq2 
 |-  ( i = 0 -> ( <" A B C "> ` i ) = ( <" A B C "> ` 0 ) )
14 12 13 eqeq12d 
 |-  ( i = 0 -> ( ( W ` i ) = ( <" A B C "> ` i ) <-> ( W ` 0 ) = ( <" A B C "> ` 0 ) ) )
15 s3fv0 
 |-  ( A e. V -> ( <" A B C "> ` 0 ) = A )
16 15 3ad2ant1 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( <" A B C "> ` 0 ) = A )
17 16 eqeq2d 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( W ` 0 ) = ( <" A B C "> ` 0 ) <-> ( W ` 0 ) = A ) )
18 14 17 sylan9bbr 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ i = 0 ) -> ( ( W ` i ) = ( <" A B C "> ` i ) <-> ( W ` 0 ) = A ) )
19 fveq2 
 |-  ( i = 1 -> ( W ` i ) = ( W ` 1 ) )
20 fveq2 
 |-  ( i = 1 -> ( <" A B C "> ` i ) = ( <" A B C "> ` 1 ) )
21 19 20 eqeq12d 
 |-  ( i = 1 -> ( ( W ` i ) = ( <" A B C "> ` i ) <-> ( W ` 1 ) = ( <" A B C "> ` 1 ) ) )
22 s3fv1 
 |-  ( B e. V -> ( <" A B C "> ` 1 ) = B )
23 22 3ad2ant2 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( <" A B C "> ` 1 ) = B )
24 23 eqeq2d 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( W ` 1 ) = ( <" A B C "> ` 1 ) <-> ( W ` 1 ) = B ) )
25 21 24 sylan9bbr 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ i = 1 ) -> ( ( W ` i ) = ( <" A B C "> ` i ) <-> ( W ` 1 ) = B ) )
26 fveq2 
 |-  ( i = 2 -> ( W ` i ) = ( W ` 2 ) )
27 fveq2 
 |-  ( i = 2 -> ( <" A B C "> ` i ) = ( <" A B C "> ` 2 ) )
28 26 27 eqeq12d 
 |-  ( i = 2 -> ( ( W ` i ) = ( <" A B C "> ` i ) <-> ( W ` 2 ) = ( <" A B C "> ` 2 ) ) )
29 s3fv2 
 |-  ( C e. V -> ( <" A B C "> ` 2 ) = C )
30 29 3ad2ant3 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( <" A B C "> ` 2 ) = C )
31 30 eqeq2d 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( ( W ` 2 ) = ( <" A B C "> ` 2 ) <-> ( W ` 2 ) = C ) )
32 28 31 sylan9bbr 
 |-  ( ( ( A e. V /\ B e. V /\ C e. V ) /\ i = 2 ) -> ( ( W ` i ) = ( <" A B C "> ` i ) <-> ( W ` 2 ) = C ) )
33 0zd 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> 0 e. ZZ )
34 1zzd 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> 1 e. ZZ )
35 2z 
 |-  2 e. ZZ
36 35 a1i 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> 2 e. ZZ )
37 18 25 32 33 34 36 raltpd 
 |-  ( ( A e. V /\ B e. V /\ C e. V ) -> ( A. i e. { 0 , 1 , 2 } ( W ` i ) = ( <" A B C "> ` i ) <-> ( ( W ` 0 ) = A /\ ( W ` 1 ) = B /\ ( W ` 2 ) = C ) ) )
38 37 adantl 
 |-  ( ( W e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( A. i e. { 0 , 1 , 2 } ( W ` i ) = ( <" A B C "> ` i ) <-> ( ( W ` 0 ) = A /\ ( W ` 1 ) = B /\ ( W ` 2 ) = C ) ) )
39 11 38 sylan9bbr 
 |-  ( ( ( W e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) /\ ( # ` W ) = 3 ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( <" A B C "> ` i ) <-> ( ( W ` 0 ) = A /\ ( W ` 1 ) = B /\ ( W ` 2 ) = C ) ) )
40 39 pm5.32da 
 |-  ( ( W e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( ( ( # ` W ) = 3 /\ A. i e. ( 0 ..^ ( # ` W ) ) ( W ` i ) = ( <" A B C "> ` i ) ) <-> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = A /\ ( W ` 1 ) = B /\ ( W ` 2 ) = C ) ) ) )
41 3 7 40 3bitrd 
 |-  ( ( W e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( W = <" A B C "> <-> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = A /\ ( W ` 1 ) = B /\ ( W ` 2 ) = C ) ) ) )