Proof of Theorem scshwfzeqfzo
Step | Hyp | Ref
| Expression |
1 | | lencl 13179 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ Word 𝑉 → (#‘𝑋) ∈
ℕ0) |
2 | | elnn0uz 11601 |
. . . . . . . . . . . 12
⊢
((#‘𝑋) ∈
ℕ0 ↔ (#‘𝑋) ∈
(ℤ≥‘0)) |
3 | 1, 2 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ Word 𝑉 → (#‘𝑋) ∈
(ℤ≥‘0)) |
4 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝑋)) → (#‘𝑋) ∈
(ℤ≥‘0)) |
5 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑁 = (#‘𝑋) → (𝑁 ∈ (ℤ≥‘0)
↔ (#‘𝑋) ∈
(ℤ≥‘0))) |
6 | 5 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝑋)) → (𝑁 ∈ (ℤ≥‘0)
↔ (#‘𝑋) ∈
(ℤ≥‘0))) |
7 | 4, 6 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑁 = (#‘𝑋)) → 𝑁 ∈
(ℤ≥‘0)) |
8 | 7 | 3adant2 1073 |
. . . . . . . 8
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → 𝑁 ∈
(ℤ≥‘0)) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → 𝑁 ∈
(ℤ≥‘0)) |
10 | | fzisfzounsn 12445 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘0) → (0...𝑁) = ((0..^𝑁) ∪ {𝑁})) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → (0...𝑁) = ((0..^𝑁) ∪ {𝑁})) |
12 | 11 | rexeqdv 3122 |
. . . . 5
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑋 cyclShift 𝑛) ↔ ∃𝑛 ∈ ((0..^𝑁) ∪ {𝑁})𝑦 = (𝑋 cyclShift 𝑛))) |
13 | | rexun 3755 |
. . . . 5
⊢
(∃𝑛 ∈
((0..^𝑁) ∪ {𝑁})𝑦 = (𝑋 cyclShift 𝑛) ↔ (∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛) ∨ ∃𝑛 ∈ {𝑁}𝑦 = (𝑋 cyclShift 𝑛))) |
14 | 12, 13 | syl6bb 275 |
. . . 4
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑋 cyclShift 𝑛) ↔ (∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛) ∨ ∃𝑛 ∈ {𝑁}𝑦 = (𝑋 cyclShift 𝑛)))) |
15 | | ax-1 6 |
. . . . . 6
⊢
(∃𝑛 ∈
(0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛) → (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛))) |
16 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(#‘𝑋) ∈
V |
17 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑁 = (#‘𝑋) → (𝑁 ∈ V ↔ (#‘𝑋) ∈ V)) |
18 | 16, 17 | mpbiri 247 |
. . . . . . . . . . 11
⊢ (𝑁 = (#‘𝑋) → 𝑁 ∈ V) |
19 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑁 → (𝑋 cyclShift 𝑛) = (𝑋 cyclShift 𝑁)) |
20 | 19 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (𝑦 = (𝑋 cyclShift 𝑛) ↔ 𝑦 = (𝑋 cyclShift 𝑁))) |
21 | 20 | rexsng 4166 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ V → (∃𝑛 ∈ {𝑁}𝑦 = (𝑋 cyclShift 𝑛) ↔ 𝑦 = (𝑋 cyclShift 𝑁))) |
22 | 18, 21 | syl 17 |
. . . . . . . . . 10
⊢ (𝑁 = (#‘𝑋) → (∃𝑛 ∈ {𝑁}𝑦 = (𝑋 cyclShift 𝑛) ↔ 𝑦 = (𝑋 cyclShift 𝑁))) |
23 | 22 | 3ad2ant3 1077 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → (∃𝑛 ∈ {𝑁}𝑦 = (𝑋 cyclShift 𝑛) ↔ 𝑦 = (𝑋 cyclShift 𝑁))) |
24 | 23 | adantr 480 |
. . . . . . . 8
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → (∃𝑛 ∈ {𝑁}𝑦 = (𝑋 cyclShift 𝑛) ↔ 𝑦 = (𝑋 cyclShift 𝑁))) |
25 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑁 = (#‘𝑋) → (𝑋 cyclShift 𝑁) = (𝑋 cyclShift (#‘𝑋))) |
26 | 25 | 3ad2ant3 1077 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → (𝑋 cyclShift 𝑁) = (𝑋 cyclShift (#‘𝑋))) |
27 | | cshwn 13394 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ Word 𝑉 → (𝑋 cyclShift (#‘𝑋)) = 𝑋) |
28 | 27 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → (𝑋 cyclShift (#‘𝑋)) = 𝑋) |
29 | 26, 28 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → (𝑋 cyclShift 𝑁) = 𝑋) |
30 | 29 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → (𝑦 = (𝑋 cyclShift 𝑁) ↔ 𝑦 = 𝑋)) |
31 | 30 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → (𝑦 = (𝑋 cyclShift 𝑁) ↔ 𝑦 = 𝑋)) |
32 | | cshw0 13391 |
. . . . . . . . . . . . . . 15
⊢ (𝑋 ∈ Word 𝑉 → (𝑋 cyclShift 0) = 𝑋) |
33 | 32 | 3ad2ant1 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → (𝑋 cyclShift 0) = 𝑋) |
34 | | lennncl 13180 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅) → (#‘𝑋) ∈
ℕ) |
35 | 34 | 3adant3 1074 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → (#‘𝑋) ∈ ℕ) |
36 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 = (#‘𝑋) → (𝑁 ∈ ℕ ↔ (#‘𝑋) ∈
ℕ)) |
37 | 36 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → (𝑁 ∈ ℕ ↔ (#‘𝑋) ∈
ℕ)) |
38 | 35, 37 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → 𝑁 ∈ ℕ) |
39 | | lbfzo0 12375 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
(0..^𝑁) ↔ 𝑁 ∈
ℕ) |
40 | 38, 39 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → 0 ∈ (0..^𝑁)) |
41 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (0 =
𝑛 → (𝑋 cyclShift 0) = (𝑋 cyclShift 𝑛)) |
42 | 41 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 =
𝑛 → ((𝑋 cyclShift 0) = 𝑋 ↔ (𝑋 cyclShift 𝑛) = 𝑋)) |
43 | 42 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 0 → ((𝑋 cyclShift 0) = 𝑋 ↔ (𝑋 cyclShift 𝑛) = 𝑋)) |
44 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 cyclShift 𝑛) = 𝑋 ↔ 𝑋 = (𝑋 cyclShift 𝑛)) |
45 | 43, 44 | syl6bb 275 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 0 → ((𝑋 cyclShift 0) = 𝑋 ↔ 𝑋 = (𝑋 cyclShift 𝑛))) |
46 | 45 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑛 = 0) → ((𝑋 cyclShift 0) = 𝑋 ↔ 𝑋 = (𝑋 cyclShift 𝑛))) |
47 | 46 | biimpd 218 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑛 = 0) → ((𝑋 cyclShift 0) = 𝑋 → 𝑋 = (𝑋 cyclShift 𝑛))) |
48 | 40, 47 | rspcimedv 3284 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → ((𝑋 cyclShift 0) = 𝑋 → ∃𝑛 ∈ (0..^𝑁)𝑋 = (𝑋 cyclShift 𝑛))) |
49 | 33, 48 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → ∃𝑛 ∈ (0..^𝑁)𝑋 = (𝑋 cyclShift 𝑛)) |
50 | 49 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → ∃𝑛 ∈ (0..^𝑁)𝑋 = (𝑋 cyclShift 𝑛)) |
51 | 50 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) ∧ 𝑦 = 𝑋) → ∃𝑛 ∈ (0..^𝑁)𝑋 = (𝑋 cyclShift 𝑛)) |
52 | | eqeq1 2614 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑋 → (𝑦 = (𝑋 cyclShift 𝑛) ↔ 𝑋 = (𝑋 cyclShift 𝑛))) |
53 | 52 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) ∧ 𝑦 = 𝑋) → (𝑦 = (𝑋 cyclShift 𝑛) ↔ 𝑋 = (𝑋 cyclShift 𝑛))) |
54 | 53 | rexbidv 3034 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) ∧ 𝑦 = 𝑋) → (∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0..^𝑁)𝑋 = (𝑋 cyclShift 𝑛))) |
55 | 51, 54 | mpbird 246 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) ∧ 𝑦 = 𝑋) → ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛)) |
56 | 55 | ex 449 |
. . . . . . . . 9
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → (𝑦 = 𝑋 → ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛))) |
57 | 31, 56 | sylbid 229 |
. . . . . . . 8
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → (𝑦 = (𝑋 cyclShift 𝑁) → ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛))) |
58 | 24, 57 | sylbid 229 |
. . . . . . 7
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → (∃𝑛 ∈ {𝑁}𝑦 = (𝑋 cyclShift 𝑛) → ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛))) |
59 | 58 | com12 32 |
. . . . . 6
⊢
(∃𝑛 ∈
{𝑁}𝑦 = (𝑋 cyclShift 𝑛) → (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛))) |
60 | 15, 59 | jaoi 393 |
. . . . 5
⊢
((∃𝑛 ∈
(0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛) ∨ ∃𝑛 ∈ {𝑁}𝑦 = (𝑋 cyclShift 𝑛)) → (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛))) |
61 | 60 | com12 32 |
. . . 4
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → ((∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛) ∨ ∃𝑛 ∈ {𝑁}𝑦 = (𝑋 cyclShift 𝑛)) → ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛))) |
62 | 14, 61 | sylbid 229 |
. . 3
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑋 cyclShift 𝑛) → ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛))) |
63 | | fzossfz 12357 |
. . . 4
⊢
(0..^𝑁) ⊆
(0...𝑁) |
64 | | ssrexv 3630 |
. . . 4
⊢
((0..^𝑁) ⊆
(0...𝑁) →
(∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛) → ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑋 cyclShift 𝑛))) |
65 | 63, 64 | mp1i 13 |
. . 3
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → (∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛) → ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑋 cyclShift 𝑛))) |
66 | 62, 65 | impbid 201 |
. 2
⊢ (((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) ∧ 𝑦 ∈ Word 𝑉) → (∃𝑛 ∈ (0...𝑁)𝑦 = (𝑋 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛))) |
67 | 66 | rabbidva 3163 |
1
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑋 cyclShift 𝑛)} = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛)}) |