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 𝑛 ) } )