Step | Hyp | Ref
| Expression |
1 | | tocycf.c |
. . 3
⊢ 𝐶 = (toCyc‘𝐷) |
2 | 1 | tocycval 31094 |
. 2
⊢ (𝐷 ∈ 𝑉 → 𝐶 = (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↦ (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ ◡𝑢)))) |
3 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → 𝑢 = ∅) |
4 | 3 | rneqd 5807 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → ran 𝑢 = ran ∅) |
5 | | rn0 5795 |
. . . . . . . . . 10
⊢ ran
∅ = ∅ |
6 | 4, 5 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → ran 𝑢 = ∅) |
7 | 6 | difeq2d 4037 |
. . . . . . . 8
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → (𝐷 ∖ ran 𝑢) = (𝐷 ∖ ∅)) |
8 | | dif0 4287 |
. . . . . . . 8
⊢ (𝐷 ∖ ∅) = 𝐷 |
9 | 7, 8 | eqtrdi 2794 |
. . . . . . 7
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → (𝐷 ∖ ran 𝑢) = 𝐷) |
10 | 9 | reseq2d 5851 |
. . . . . 6
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → ( I ↾ (𝐷 ∖ ran 𝑢)) = ( I ↾ 𝐷)) |
11 | 3 | cnveqd 5744 |
. . . . . . . . 9
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → ◡𝑢 = ◡∅) |
12 | | cnv0 6004 |
. . . . . . . . 9
⊢ ◡∅ = ∅ |
13 | 11, 12 | eqtrdi 2794 |
. . . . . . . 8
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → ◡𝑢 = ∅) |
14 | 13 | coeq2d 5731 |
. . . . . . 7
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → ((𝑢 cyclShift 1) ∘ ◡𝑢) = ((𝑢 cyclShift 1) ∘
∅)) |
15 | | co02 6124 |
. . . . . . 7
⊢ ((𝑢 cyclShift 1) ∘ ∅) =
∅ |
16 | 14, 15 | eqtrdi 2794 |
. . . . . 6
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → ((𝑢 cyclShift 1) ∘ ◡𝑢) = ∅) |
17 | 10, 16 | uneq12d 4078 |
. . . . 5
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ ◡𝑢)) = (( I ↾ 𝐷) ∪ ∅)) |
18 | | un0 4305 |
. . . . 5
⊢ (( I
↾ 𝐷) ∪ ∅) =
( I ↾ 𝐷) |
19 | 17, 18 | eqtrdi 2794 |
. . . 4
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ ◡𝑢)) = ( I ↾ 𝐷)) |
20 | | tocycf.s |
. . . . . . 7
⊢ 𝑆 = (SymGrp‘𝐷) |
21 | 20 | idresperm 18778 |
. . . . . 6
⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) ∈ (Base‘𝑆)) |
22 | | tocycf.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑆) |
23 | 21, 22 | eleqtrrdi 2849 |
. . . . 5
⊢ (𝐷 ∈ 𝑉 → ( I ↾ 𝐷) ∈ 𝐵) |
24 | 23 | ad2antrr 726 |
. . . 4
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → ( I ↾ 𝐷) ∈ 𝐵) |
25 | 19, 24 | eqeltrd 2838 |
. . 3
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 = ∅) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ ◡𝑢)) ∈ 𝐵) |
26 | | difexg 5220 |
. . . . . . . . 9
⊢ (𝐷 ∈ 𝑉 → (𝐷 ∖ ran 𝑢) ∈ V) |
27 | 26 | resiexd 7032 |
. . . . . . . 8
⊢ (𝐷 ∈ 𝑉 → ( I ↾ (𝐷 ∖ ran 𝑢)) ∈ V) |
28 | | ovex 7246 |
. . . . . . . . 9
⊢ (𝑢 cyclShift 1) ∈
V |
29 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
30 | 29 | cnvex 7703 |
. . . . . . . . 9
⊢ ◡𝑢 ∈ V |
31 | 28, 30 | coex 7708 |
. . . . . . . 8
⊢ ((𝑢 cyclShift 1) ∘ ◡𝑢) ∈ V |
32 | | unexg 7534 |
. . . . . . . 8
⊢ ((( I
↾ (𝐷 ∖ ran
𝑢)) ∈ V ∧ ((𝑢 cyclShift 1) ∘ ◡𝑢) ∈ V) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ ◡𝑢)) ∈ V) |
33 | 27, 31, 32 | sylancl 589 |
. . . . . . 7
⊢ (𝐷 ∈ 𝑉 → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ ◡𝑢)) ∈ V) |
34 | 33 | adantr 484 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ ◡𝑢)) ∈ V) |
35 | 2, 34 | fvmpt2d 6831 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) → (𝐶‘𝑢) = (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ ◡𝑢))) |
36 | 35 | adantr 484 |
. . . 4
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 ≠ ∅) → (𝐶‘𝑢) = (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ ◡𝑢))) |
37 | | simpll 767 |
. . . . . 6
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 ≠ ∅) → 𝐷 ∈ 𝑉) |
38 | | simplr 769 |
. . . . . . . 8
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 ≠ ∅) → 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
39 | | id 22 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑢 → 𝑤 = 𝑢) |
40 | | dmeq 5772 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢) |
41 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑢 → 𝐷 = 𝐷) |
42 | 39, 40, 41 | f1eq123d 6653 |
. . . . . . . . 9
⊢ (𝑤 = 𝑢 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑢:dom 𝑢–1-1→𝐷)) |
43 | 42 | elrab 3602 |
. . . . . . . 8
⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷)) |
44 | 38, 43 | sylib 221 |
. . . . . . 7
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 ≠ ∅) → (𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢–1-1→𝐷)) |
45 | 44 | simpld 498 |
. . . . . 6
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 ≠ ∅) → 𝑢 ∈ Word 𝐷) |
46 | 44 | simprd 499 |
. . . . . 6
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 ≠ ∅) → 𝑢:dom 𝑢–1-1→𝐷) |
47 | 1, 37, 45, 46, 20 | cycpmcl 31102 |
. . . . 5
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 ≠ ∅) → (𝐶‘𝑢) ∈ (Base‘𝑆)) |
48 | 47, 22 | eleqtrrdi 2849 |
. . . 4
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 ≠ ∅) → (𝐶‘𝑢) ∈ 𝐵) |
49 | 36, 48 | eqeltrrd 2839 |
. . 3
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) ∧ 𝑢 ≠ ∅) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ ◡𝑢)) ∈ 𝐵) |
50 | 25, 49 | pm2.61dane 3029 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) → (( I ↾ (𝐷 ∖ ran 𝑢)) ∪ ((𝑢 cyclShift 1) ∘ ◡𝑢)) ∈ 𝐵) |
51 | 2, 50 | fmpt3d 6933 |
1
⊢ (𝐷 ∈ 𝑉 → 𝐶:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵) |