# 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}=\left\{{w}\in \mathrm{Word}{V}|\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\mathrm{cyclShift}{n}={w}\right\}$
Assertion cshwsiun ${⊢}{W}\in \mathrm{Word}{V}\to {M}=\bigcup _{{n}\in \left(0..^\left|{W}\right|\right)}\left\{{W}\mathrm{cyclShift}{n}\right\}$

### Proof

Step Hyp Ref Expression
1 cshwrepswhash1.m ${⊢}{M}=\left\{{w}\in \mathrm{Word}{V}|\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\mathrm{cyclShift}{n}={w}\right\}$
2 df-rab ${⊢}\left\{{w}\in \mathrm{Word}{V}|\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\mathrm{cyclShift}{n}={w}\right\}=\left\{{w}|\left({w}\in \mathrm{Word}{V}\wedge \exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\mathrm{cyclShift}{n}={w}\right)\right\}$
3 eqcom ${⊢}{W}\mathrm{cyclShift}{n}={w}↔{w}={W}\mathrm{cyclShift}{n}$
4 3 biimpi ${⊢}{W}\mathrm{cyclShift}{n}={w}\to {w}={W}\mathrm{cyclShift}{n}$
5 4 reximi ${⊢}\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\mathrm{cyclShift}{n}={w}\to \exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{w}={W}\mathrm{cyclShift}{n}$
6 5 adantl ${⊢}\left({w}\in \mathrm{Word}{V}\wedge \exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\mathrm{cyclShift}{n}={w}\right)\to \exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{w}={W}\mathrm{cyclShift}{n}$
7 cshwcl ${⊢}{W}\in \mathrm{Word}{V}\to {W}\mathrm{cyclShift}{n}\in \mathrm{Word}{V}$
8 7 adantr ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {n}\in \left(0..^\left|{W}\right|\right)\right)\to {W}\mathrm{cyclShift}{n}\in \mathrm{Word}{V}$
9 eleq1 ${⊢}{w}={W}\mathrm{cyclShift}{n}\to \left({w}\in \mathrm{Word}{V}↔{W}\mathrm{cyclShift}{n}\in \mathrm{Word}{V}\right)$
10 8 9 syl5ibrcom ${⊢}\left({W}\in \mathrm{Word}{V}\wedge {n}\in \left(0..^\left|{W}\right|\right)\right)\to \left({w}={W}\mathrm{cyclShift}{n}\to {w}\in \mathrm{Word}{V}\right)$
11 10 rexlimdva ${⊢}{W}\in \mathrm{Word}{V}\to \left(\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{w}={W}\mathrm{cyclShift}{n}\to {w}\in \mathrm{Word}{V}\right)$
12 eqcom ${⊢}{w}={W}\mathrm{cyclShift}{n}↔{W}\mathrm{cyclShift}{n}={w}$
13 12 biimpi ${⊢}{w}={W}\mathrm{cyclShift}{n}\to {W}\mathrm{cyclShift}{n}={w}$
14 13 reximi ${⊢}\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{w}={W}\mathrm{cyclShift}{n}\to \exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\mathrm{cyclShift}{n}={w}$
15 11 14 jca2 ${⊢}{W}\in \mathrm{Word}{V}\to \left(\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{w}={W}\mathrm{cyclShift}{n}\to \left({w}\in \mathrm{Word}{V}\wedge \exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\mathrm{cyclShift}{n}={w}\right)\right)$
16 6 15 impbid2 ${⊢}{W}\in \mathrm{Word}{V}\to \left(\left({w}\in \mathrm{Word}{V}\wedge \exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\mathrm{cyclShift}{n}={w}\right)↔\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{w}={W}\mathrm{cyclShift}{n}\right)$
17 velsn ${⊢}{w}\in \left\{{W}\mathrm{cyclShift}{n}\right\}↔{w}={W}\mathrm{cyclShift}{n}$
18 17 bicomi ${⊢}{w}={W}\mathrm{cyclShift}{n}↔{w}\in \left\{{W}\mathrm{cyclShift}{n}\right\}$
19 18 a1i ${⊢}{W}\in \mathrm{Word}{V}\to \left({w}={W}\mathrm{cyclShift}{n}↔{w}\in \left\{{W}\mathrm{cyclShift}{n}\right\}\right)$
20 19 rexbidv ${⊢}{W}\in \mathrm{Word}{V}\to \left(\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{w}={W}\mathrm{cyclShift}{n}↔\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{w}\in \left\{{W}\mathrm{cyclShift}{n}\right\}\right)$
21 16 20 bitrd ${⊢}{W}\in \mathrm{Word}{V}\to \left(\left({w}\in \mathrm{Word}{V}\wedge \exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\mathrm{cyclShift}{n}={w}\right)↔\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{w}\in \left\{{W}\mathrm{cyclShift}{n}\right\}\right)$
22 21 abbidv ${⊢}{W}\in \mathrm{Word}{V}\to \left\{{w}|\left({w}\in \mathrm{Word}{V}\wedge \exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\mathrm{cyclShift}{n}={w}\right)\right\}=\left\{{w}|\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{w}\in \left\{{W}\mathrm{cyclShift}{n}\right\}\right\}$
23 2 22 syl5eq ${⊢}{W}\in \mathrm{Word}{V}\to \left\{{w}\in \mathrm{Word}{V}|\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{W}\mathrm{cyclShift}{n}={w}\right\}=\left\{{w}|\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{w}\in \left\{{W}\mathrm{cyclShift}{n}\right\}\right\}$
24 df-iun ${⊢}\bigcup _{{n}\in \left(0..^\left|{W}\right|\right)}\left\{{W}\mathrm{cyclShift}{n}\right\}=\left\{{w}|\exists {n}\in \left(0..^\left|{W}\right|\right)\phantom{\rule{.4em}{0ex}}{w}\in \left\{{W}\mathrm{cyclShift}{n}\right\}\right\}$
25 23 1 24 3eqtr4g ${⊢}{W}\in \mathrm{Word}{V}\to {M}=\bigcup _{{n}\in \left(0..^\left|{W}\right|\right)}\left\{{W}\mathrm{cyclShift}{n}\right\}$