Proof of Theorem cshwsiun
Step | Hyp | Ref
| Expression |
1 | | df-rab 2905 |
. . 3
⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑤 ∣ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)} |
2 | | eqcom 2617 |
. . . . . . . . 9
⊢ ((𝑊 cyclShift 𝑛) = 𝑤 ↔ 𝑤 = (𝑊 cyclShift 𝑛)) |
3 | 2 | biimpi 205 |
. . . . . . . 8
⊢ ((𝑊 cyclShift 𝑛) = 𝑤 → 𝑤 = (𝑊 cyclShift 𝑛)) |
4 | 3 | reximi 2994 |
. . . . . . 7
⊢
(∃𝑛 ∈
(0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤 → ∃𝑛 ∈ (0..^(#‘𝑊))𝑤 = (𝑊 cyclShift 𝑛)) |
5 | 4 | adantl 481 |
. . . . . 6
⊢ ((𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤) → ∃𝑛 ∈ (0..^(#‘𝑊))𝑤 = (𝑊 cyclShift 𝑛)) |
6 | | cshwcl 13395 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift 𝑛) ∈ Word 𝑉) |
7 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑛 ∈ (0..^(#‘𝑊))) → (𝑊 cyclShift 𝑛) ∈ Word 𝑉) |
8 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑊 cyclShift 𝑛) → (𝑤 ∈ Word 𝑉 ↔ (𝑊 cyclShift 𝑛) ∈ Word 𝑉)) |
9 | 7, 8 | syl5ibrcom 236 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑛 ∈ (0..^(#‘𝑊))) → (𝑤 = (𝑊 cyclShift 𝑛) → 𝑤 ∈ Word 𝑉)) |
10 | 9 | rexlimdva 3013 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (∃𝑛 ∈ (0..^(#‘𝑊))𝑤 = (𝑊 cyclShift 𝑛) → 𝑤 ∈ Word 𝑉)) |
11 | 10 | imp 444 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))𝑤 = (𝑊 cyclShift 𝑛)) → 𝑤 ∈ Word 𝑉) |
12 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑊 cyclShift 𝑛) ↔ (𝑊 cyclShift 𝑛) = 𝑤) |
13 | 12 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑊 cyclShift 𝑛) → (𝑊 cyclShift 𝑛) = 𝑤) |
14 | 13 | reximi 2994 |
. . . . . . . . 9
⊢
(∃𝑛 ∈
(0..^(#‘𝑊))𝑤 = (𝑊 cyclShift 𝑛) → ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤) |
15 | 14 | adantl 481 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))𝑤 = (𝑊 cyclShift 𝑛)) → ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤) |
16 | 11, 15 | jca 553 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))𝑤 = (𝑊 cyclShift 𝑛)) → (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)) |
17 | 16 | ex 449 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (∃𝑛 ∈ (0..^(#‘𝑊))𝑤 = (𝑊 cyclShift 𝑛) → (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤))) |
18 | 5, 17 | impbid2 215 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → ((𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤) ↔ ∃𝑛 ∈ (0..^(#‘𝑊))𝑤 = (𝑊 cyclShift 𝑛))) |
19 | | velsn 4141 |
. . . . . . . 8
⊢ (𝑤 ∈ {(𝑊 cyclShift 𝑛)} ↔ 𝑤 = (𝑊 cyclShift 𝑛)) |
20 | 19 | bicomi 213 |
. . . . . . 7
⊢ (𝑤 = (𝑊 cyclShift 𝑛) ↔ 𝑤 ∈ {(𝑊 cyclShift 𝑛)}) |
21 | 20 | a1i 11 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (𝑤 = (𝑊 cyclShift 𝑛) ↔ 𝑤 ∈ {(𝑊 cyclShift 𝑛)})) |
22 | 21 | rexbidv 3034 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (∃𝑛 ∈ (0..^(#‘𝑊))𝑤 = (𝑊 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0..^(#‘𝑊))𝑤 ∈ {(𝑊 cyclShift 𝑛)})) |
23 | 18, 22 | bitrd 267 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → ((𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤) ↔ ∃𝑛 ∈ (0..^(#‘𝑊))𝑤 ∈ {(𝑊 cyclShift 𝑛)})) |
24 | 23 | abbidv 2728 |
. . 3
⊢ (𝑊 ∈ Word 𝑉 → {𝑤 ∣ (𝑤 ∈ Word 𝑉 ∧ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤)} = {𝑤 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))𝑤 ∈ {(𝑊 cyclShift 𝑛)}}) |
25 | 1, 24 | syl5eq 2656 |
. 2
⊢ (𝑊 ∈ Word 𝑉 → {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} = {𝑤 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))𝑤 ∈ {(𝑊 cyclShift 𝑛)}}) |
26 | | cshwrepswhash1.m |
. 2
⊢ 𝑀 = {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} |
27 | | df-iun 4457 |
. 2
⊢ ∪ 𝑛 ∈ (0..^(#‘𝑊)){(𝑊 cyclShift 𝑛)} = {𝑤 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))𝑤 ∈ {(𝑊 cyclShift 𝑛)}} |
28 | 25, 26, 27 | 3eqtr4g 2669 |
1
⊢ (𝑊 ∈ Word 𝑉 → 𝑀 = ∪ 𝑛 ∈ (0..^(#‘𝑊)){(𝑊 cyclShift 𝑛)}) |