# 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 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
Assertion cshwsiun ( 𝑊 ∈ Word 𝑉𝑀 = 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } )

### Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m 𝑀 = { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 }
2 df-rab { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = { 𝑤 ∣ ( 𝑤 ∈ Word 𝑉 ∧ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ) }
3 eqcom ( ( 𝑊 cyclShift 𝑛 ) = 𝑤𝑤 = ( 𝑊 cyclShift 𝑛 ) )
4 3 biimpi ( ( 𝑊 cyclShift 𝑛 ) = 𝑤𝑤 = ( 𝑊 cyclShift 𝑛 ) )
5 4 reximi ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 → ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) )
6 5 adantl ( ( 𝑤 ∈ Word 𝑉 ∧ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ) → ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) )
7 cshwcl ( 𝑊 ∈ Word 𝑉 → ( 𝑊 cyclShift 𝑛 ) ∈ Word 𝑉 )
8 7 adantr ( ( 𝑊 ∈ Word 𝑉𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝑛 ) ∈ Word 𝑉 )
9 eleq1 ( 𝑤 = ( 𝑊 cyclShift 𝑛 ) → ( 𝑤 ∈ Word 𝑉 ↔ ( 𝑊 cyclShift 𝑛 ) ∈ Word 𝑉 ) )
10 8 9 syl5ibrcom ( ( 𝑊 ∈ Word 𝑉𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑤 = ( 𝑊 cyclShift 𝑛 ) → 𝑤 ∈ Word 𝑉 ) )
11 10 rexlimdva ( 𝑊 ∈ Word 𝑉 → ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) → 𝑤 ∈ Word 𝑉 ) )
12 eqcom ( 𝑤 = ( 𝑊 cyclShift 𝑛 ) ↔ ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
13 12 biimpi ( 𝑤 = ( 𝑊 cyclShift 𝑛 ) → ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
14 13 reximi ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) → ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 )
15 11 14 jca2 ( 𝑊 ∈ Word 𝑉 → ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) → ( 𝑤 ∈ Word 𝑉 ∧ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ) ) )
16 6 15 impbid2 ( 𝑊 ∈ Word 𝑉 → ( ( 𝑤 ∈ Word 𝑉 ∧ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ) ↔ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ) )
17 velsn ( 𝑤 ∈ { ( 𝑊 cyclShift 𝑛 ) } ↔ 𝑤 = ( 𝑊 cyclShift 𝑛 ) )
18 17 bicomi ( 𝑤 = ( 𝑊 cyclShift 𝑛 ) ↔ 𝑤 ∈ { ( 𝑊 cyclShift 𝑛 ) } )
19 18 a1i ( 𝑊 ∈ Word 𝑉 → ( 𝑤 = ( 𝑊 cyclShift 𝑛 ) ↔ 𝑤 ∈ { ( 𝑊 cyclShift 𝑛 ) } ) )
20 19 rexbidv ( 𝑊 ∈ Word 𝑉 → ( ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 = ( 𝑊 cyclShift 𝑛 ) ↔ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 ∈ { ( 𝑊 cyclShift 𝑛 ) } ) )
21 16 20 bitrd ( 𝑊 ∈ Word 𝑉 → ( ( 𝑤 ∈ Word 𝑉 ∧ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ) ↔ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 ∈ { ( 𝑊 cyclShift 𝑛 ) } ) )
22 21 abbidv ( 𝑊 ∈ Word 𝑉 → { 𝑤 ∣ ( 𝑤 ∈ Word 𝑉 ∧ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 ) } = { 𝑤 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 ∈ { ( 𝑊 cyclShift 𝑛 ) } } )
23 2 22 syl5eq ( 𝑊 ∈ Word 𝑉 → { 𝑤 ∈ Word 𝑉 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ( 𝑊 cyclShift 𝑛 ) = 𝑤 } = { 𝑤 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 ∈ { ( 𝑊 cyclShift 𝑛 ) } } )
24 df-iun 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } = { 𝑤 ∣ ∃ 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) 𝑤 ∈ { ( 𝑊 cyclShift 𝑛 ) } }
25 23 1 24 3eqtr4g ( 𝑊 ∈ Word 𝑉𝑀 = 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) { ( 𝑊 cyclShift 𝑛 ) } )