Metamath Proof Explorer

Theorem cshwsiun

Description: The set of (different!) words resulting by cyclically shifting a given word is an indexed union. (Contributed by AV, 19-May-2018) (Revised by AV, 8-Jun-2018) (Proof shortened by AV, 8-Nov-2018)

Ref Expression
Hypothesis cshwrepswhash1.m 
|- M = { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w }
Assertion cshwsiun 
|- ( W e. Word V -> M = U_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } )

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m 
 |-  M = { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w }
2 df-rab 
 |-  { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } = { w | ( w e. Word V /\ E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w ) }
3 eqcom 
 |-  ( ( W cyclShift n ) = w <-> w = ( W cyclShift n ) )
4 3 biimpi 
 |-  ( ( W cyclShift n ) = w -> w = ( W cyclShift n ) )
5 4 reximi 
 |-  ( E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w -> E. n e. ( 0 ..^ ( # ` W ) ) w = ( W cyclShift n ) )
6 5 adantl 
 |-  ( ( w e. Word V /\ E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w ) -> E. n e. ( 0 ..^ ( # ` W ) ) w = ( W cyclShift n ) )
7 cshwcl 
 |-  ( W e. Word V -> ( W cyclShift n ) e. Word V )
8 7 adantr 
 |-  ( ( W e. Word V /\ n e. ( 0 ..^ ( # ` W ) ) ) -> ( W cyclShift n ) e. Word V )
9 eleq1 
 |-  ( w = ( W cyclShift n ) -> ( w e. Word V <-> ( W cyclShift n ) e. Word V ) )
10 8 9 syl5ibrcom 
 |-  ( ( W e. Word V /\ n e. ( 0 ..^ ( # ` W ) ) ) -> ( w = ( W cyclShift n ) -> w e. Word V ) )
11 10 rexlimdva 
 |-  ( W e. Word V -> ( E. n e. ( 0 ..^ ( # ` W ) ) w = ( W cyclShift n ) -> w e. Word V ) )
12 eqcom 
 |-  ( w = ( W cyclShift n ) <-> ( W cyclShift n ) = w )
13 12 biimpi 
 |-  ( w = ( W cyclShift n ) -> ( W cyclShift n ) = w )
14 13 reximi 
 |-  ( E. n e. ( 0 ..^ ( # ` W ) ) w = ( W cyclShift n ) -> E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w )
15 11 14 jca2 
 |-  ( W e. Word V -> ( E. n e. ( 0 ..^ ( # ` W ) ) w = ( W cyclShift n ) -> ( w e. Word V /\ E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w ) ) )
16 6 15 impbid2 
 |-  ( W e. Word V -> ( ( w e. Word V /\ E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w ) <-> E. n e. ( 0 ..^ ( # ` W ) ) w = ( W cyclShift n ) ) )
17 velsn 
 |-  ( w e. { ( W cyclShift n ) } <-> w = ( W cyclShift n ) )
18 17 bicomi 
 |-  ( w = ( W cyclShift n ) <-> w e. { ( W cyclShift n ) } )
19 18 a1i 
 |-  ( W e. Word V -> ( w = ( W cyclShift n ) <-> w e. { ( W cyclShift n ) } ) )
20 19 rexbidv 
 |-  ( W e. Word V -> ( E. n e. ( 0 ..^ ( # ` W ) ) w = ( W cyclShift n ) <-> E. n e. ( 0 ..^ ( # ` W ) ) w e. { ( W cyclShift n ) } ) )
21 16 20 bitrd 
 |-  ( W e. Word V -> ( ( w e. Word V /\ E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w ) <-> E. n e. ( 0 ..^ ( # ` W ) ) w e. { ( W cyclShift n ) } ) )
22 21 abbidv 
 |-  ( W e. Word V -> { w | ( w e. Word V /\ E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w ) } = { w | E. n e. ( 0 ..^ ( # ` W ) ) w e. { ( W cyclShift n ) } } )
23 2 22 eqtrid 
 |-  ( W e. Word V -> { w e. Word V | E. n e. ( 0 ..^ ( # ` W ) ) ( W cyclShift n ) = w } = { w | E. n e. ( 0 ..^ ( # ` W ) ) w e. { ( W cyclShift n ) } } )
24 df-iun 
 |-  U_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } = { w | E. n e. ( 0 ..^ ( # ` W ) ) w e. { ( W cyclShift n ) } }
25 23 1 24 3eqtr4g 
 |-  ( W e. Word V -> M = U_ n e. ( 0 ..^ ( # ` W ) ) { ( W cyclShift n ) } )