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 ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w
Assertion cshwsiun ⊢ W ∈ Word V → M = ⋃ n ∈ 0 ..^ W W cyclShift n

Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m ⊢ M = w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w
2 df-rab ⊢ w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w = w | w ∈ Word V ∧ ∃ n ∈ 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 ⊢ ∃ n ∈ 0 ..^ W W cyclShift n = w → ∃ n ∈ 0 ..^ W w = W cyclShift n
6 5 adantl ⊢ w ∈ Word V ∧ ∃ n ∈ 0 ..^ W W cyclShift n = w → ∃ n ∈ 0 ..^ W w = W cyclShift n
7 cshwcl ⊢ W ∈ Word V → W cyclShift n ∈ Word V
8 7 adantr ⊢ W ∈ Word V ∧ n ∈ 0 ..^ W → W cyclShift n ∈ Word V
9 eleq1 ⊢ w = W cyclShift n → w ∈ Word V ↔ W cyclShift n ∈ Word V
10 8 9 syl5ibrcom ⊢ W ∈ Word V ∧ n ∈ 0 ..^ W → w = W cyclShift n → w ∈ Word V
11 10 rexlimdva ⊢ W ∈ Word V → ∃ n ∈ 0 ..^ W w = W cyclShift n → w ∈ 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 ⊢ ∃ n ∈ 0 ..^ W w = W cyclShift n → ∃ n ∈ 0 ..^ W W cyclShift n = w
15 11 14 jca2 ⊢ W ∈ Word V → ∃ n ∈ 0 ..^ W w = W cyclShift n → w ∈ Word V ∧ ∃ n ∈ 0 ..^ W W cyclShift n = w
16 6 15 impbid2 ⊢ W ∈ Word V → w ∈ Word V ∧ ∃ n ∈ 0 ..^ W W cyclShift n = w ↔ ∃ n ∈ 0 ..^ W w = W cyclShift n
17 velsn ⊢ w ∈ W cyclShift n ↔ w = W cyclShift n
18 17 bicomi ⊢ w = W cyclShift n ↔ w ∈ W cyclShift n
19 18 a1i ⊢ W ∈ Word V → w = W cyclShift n ↔ w ∈ W cyclShift n
20 19 rexbidv ⊢ W ∈ Word V → ∃ n ∈ 0 ..^ W w = W cyclShift n ↔ ∃ n ∈ 0 ..^ W w ∈ W cyclShift n
21 16 20 bitrd ⊢ W ∈ Word V → w ∈ Word V ∧ ∃ n ∈ 0 ..^ W W cyclShift n = w ↔ ∃ n ∈ 0 ..^ W w ∈ W cyclShift n
22 21 abbidv ⊢ W ∈ Word V → w | w ∈ Word V ∧ ∃ n ∈ 0 ..^ W W cyclShift n = w = w | ∃ n ∈ 0 ..^ W w ∈ W cyclShift n
23 2 22 syl5eq ⊢ W ∈ Word V → w ∈ Word V | ∃ n ∈ 0 ..^ W W cyclShift n = w = w | ∃ n ∈ 0 ..^ W w ∈ W cyclShift n
24 df-iun ⊢ ⋃ n ∈ 0 ..^ W W cyclShift n = w | ∃ n ∈ 0 ..^ W w ∈ W cyclShift n
25 23 1 24 3eqtr4g ⊢ W ∈ Word V → M = ⋃ n ∈ 0 ..^ W W cyclShift n