| Step | Hyp | Ref
| Expression |
| 1 | | tocyc01.1 |
. . . . 5
⊢ 𝐶 = (toCyc‘𝐷) |
| 2 | | simpl 482 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) → 𝐷 ∈ 𝑉) |
| 3 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) → 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) |
| 4 | 3 | elin1d 4204 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) → 𝑊 ∈ dom 𝐶) |
| 5 | | eqid 2737 |
. . . . . . . . . 10
⊢
(SymGrp‘𝐷) =
(SymGrp‘𝐷) |
| 6 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘(SymGrp‘𝐷)) = (Base‘(SymGrp‘𝐷)) |
| 7 | 1, 5, 6 | tocycf 33137 |
. . . . . . . . 9
⊢ (𝐷 ∈ 𝑉 → 𝐶:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘(SymGrp‘𝐷))) |
| 8 | | fdm 6745 |
. . . . . . . . 9
⊢ (𝐶:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶(Base‘(SymGrp‘𝐷)) → dom 𝐶 = {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
| 9 | 2, 7, 8 | 3syl 18 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) → dom 𝐶 = {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
| 10 | 4, 9 | eleqtrd 2843 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) → 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
| 11 | | id 22 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) |
| 12 | | dmeq 5914 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊) |
| 13 | | eqidd 2738 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → 𝐷 = 𝐷) |
| 14 | 11, 12, 13 | f1eq123d 6840 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑊:dom 𝑊–1-1→𝐷)) |
| 15 | 14 | elrab 3692 |
. . . . . . 7
⊢ (𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) |
| 16 | 10, 15 | sylib 218 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) → (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) |
| 17 | 16 | simpld 494 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) → 𝑊 ∈ Word 𝐷) |
| 18 | 16 | simprd 495 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) → 𝑊:dom 𝑊–1-1→𝐷) |
| 19 | 1, 2, 17, 18 | tocycfv 33129 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) → (𝐶‘𝑊) = (( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊))) |
| 20 | 19 | adantr 480 |
. . 3
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 0)
→ (𝐶‘𝑊) = (( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊))) |
| 21 | | hasheq0 14402 |
. . . . . 6
⊢ (𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1})) →
((♯‘𝑊) = 0
↔ 𝑊 =
∅)) |
| 22 | 3, 21 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) →
((♯‘𝑊) = 0
↔ 𝑊 =
∅)) |
| 23 | 22 | biimpa 476 |
. . . 4
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 0)
→ 𝑊 =
∅) |
| 24 | | rneq 5947 |
. . . . . . . . . 10
⊢ (𝑊 = ∅ → ran 𝑊 = ran ∅) |
| 25 | | rn0 5936 |
. . . . . . . . . 10
⊢ ran
∅ = ∅ |
| 26 | 24, 25 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑊 = ∅ → ran 𝑊 = ∅) |
| 27 | 26 | difeq2d 4126 |
. . . . . . . 8
⊢ (𝑊 = ∅ → (𝐷 ∖ ran 𝑊) = (𝐷 ∖ ∅)) |
| 28 | | dif0 4378 |
. . . . . . . 8
⊢ (𝐷 ∖ ∅) = 𝐷 |
| 29 | 27, 28 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑊 = ∅ → (𝐷 ∖ ran 𝑊) = 𝐷) |
| 30 | 29 | reseq2d 5997 |
. . . . . 6
⊢ (𝑊 = ∅ → ( I ↾
(𝐷 ∖ ran 𝑊)) = ( I ↾ 𝐷)) |
| 31 | | cnveq 5884 |
. . . . . . . . 9
⊢ (𝑊 = ∅ → ◡𝑊 = ◡∅) |
| 32 | | cnv0 6160 |
. . . . . . . . 9
⊢ ◡∅ = ∅ |
| 33 | 31, 32 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑊 = ∅ → ◡𝑊 = ∅) |
| 34 | 33 | coeq2d 5873 |
. . . . . . 7
⊢ (𝑊 = ∅ → ((𝑊 cyclShift 1) ∘ ◡𝑊) = ((𝑊 cyclShift 1) ∘
∅)) |
| 35 | | co02 6280 |
. . . . . . 7
⊢ ((𝑊 cyclShift 1) ∘ ∅) =
∅ |
| 36 | 34, 35 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑊 = ∅ → ((𝑊 cyclShift 1) ∘ ◡𝑊) = ∅) |
| 37 | 30, 36 | uneq12d 4169 |
. . . . 5
⊢ (𝑊 = ∅ → (( I ↾
(𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊)) = (( I ↾ 𝐷) ∪ ∅)) |
| 38 | | un0 4394 |
. . . . 5
⊢ (( I
↾ 𝐷) ∪ ∅) =
( I ↾ 𝐷) |
| 39 | 37, 38 | eqtrdi 2793 |
. . . 4
⊢ (𝑊 = ∅ → (( I ↾
(𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊)) = ( I ↾ 𝐷)) |
| 40 | 23, 39 | syl 17 |
. . 3
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 0)
→ (( I ↾ (𝐷
∖ ran 𝑊)) ∪
((𝑊 cyclShift 1) ∘
◡𝑊)) = ( I ↾ 𝐷)) |
| 41 | 20, 40 | eqtrd 2777 |
. 2
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 0)
→ (𝐶‘𝑊) = ( I ↾ 𝐷)) |
| 42 | 19 | adantr 480 |
. . 3
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 1)
→ (𝐶‘𝑊) = (( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊))) |
| 43 | 17 | adantr 480 |
. . . . . . 7
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 1)
→ 𝑊 ∈ Word 𝐷) |
| 44 | | 1zzd 12648 |
. . . . . . 7
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 1)
→ 1 ∈ ℤ) |
| 45 | | simpr 484 |
. . . . . . 7
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 1)
→ (♯‘𝑊) =
1) |
| 46 | | 1cshid 32944 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ ∧
(♯‘𝑊) = 1)
→ (𝑊 cyclShift 1) =
𝑊) |
| 47 | 43, 44, 45, 46 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 1)
→ (𝑊 cyclShift 1) =
𝑊) |
| 48 | 47 | coeq1d 5872 |
. . . . 5
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 1)
→ ((𝑊 cyclShift 1)
∘ ◡𝑊) = (𝑊 ∘ ◡𝑊)) |
| 49 | | wrdf 14557 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝐷 → 𝑊:(0..^(♯‘𝑊))⟶𝐷) |
| 50 | | ffun 6739 |
. . . . . 6
⊢ (𝑊:(0..^(♯‘𝑊))⟶𝐷 → Fun 𝑊) |
| 51 | | funcocnv2 6873 |
. . . . . 6
⊢ (Fun
𝑊 → (𝑊 ∘ ◡𝑊) = ( I ↾ ran 𝑊)) |
| 52 | 43, 49, 50, 51 | 4syl 19 |
. . . . 5
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 1)
→ (𝑊 ∘ ◡𝑊) = ( I ↾ ran 𝑊)) |
| 53 | 48, 52 | eqtrd 2777 |
. . . 4
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 1)
→ ((𝑊 cyclShift 1)
∘ ◡𝑊) = ( I ↾ ran 𝑊)) |
| 54 | 53 | uneq2d 4168 |
. . 3
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 1)
→ (( I ↾ (𝐷
∖ ran 𝑊)) ∪
((𝑊 cyclShift 1) ∘
◡𝑊)) = (( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ( I ↾ ran 𝑊))) |
| 55 | | resundi 6011 |
. . . 4
⊢ ( I
↾ ((𝐷 ∖ ran
𝑊) ∪ ran 𝑊)) = (( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ( I ↾ ran 𝑊)) |
| 56 | | frn 6743 |
. . . . . . 7
⊢ (𝑊:(0..^(♯‘𝑊))⟶𝐷 → ran 𝑊 ⊆ 𝐷) |
| 57 | | undifr 4483 |
. . . . . . 7
⊢ (ran
𝑊 ⊆ 𝐷 ↔ ((𝐷 ∖ ran 𝑊) ∪ ran 𝑊) = 𝐷) |
| 58 | 56, 57 | sylib 218 |
. . . . . 6
⊢ (𝑊:(0..^(♯‘𝑊))⟶𝐷 → ((𝐷 ∖ ran 𝑊) ∪ ran 𝑊) = 𝐷) |
| 59 | 43, 49, 58 | 3syl 18 |
. . . . 5
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 1)
→ ((𝐷 ∖ ran
𝑊) ∪ ran 𝑊) = 𝐷) |
| 60 | 59 | reseq2d 5997 |
. . . 4
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 1)
→ ( I ↾ ((𝐷
∖ ran 𝑊) ∪ ran
𝑊)) = ( I ↾ 𝐷)) |
| 61 | 55, 60 | eqtr3id 2791 |
. . 3
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 1)
→ (( I ↾ (𝐷
∖ ran 𝑊)) ∪ ( I
↾ ran 𝑊)) = ( I
↾ 𝐷)) |
| 62 | 42, 54, 61 | 3eqtrd 2781 |
. 2
⊢ (((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) ∧
(♯‘𝑊) = 1)
→ (𝐶‘𝑊) = ( I ↾ 𝐷)) |
| 63 | 3 | elin2d 4205 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) → 𝑊 ∈ (◡♯ “ {0, 1})) |
| 64 | | hashf 14377 |
. . . . . 6
⊢
♯:V⟶(ℕ0 ∪ {+∞}) |
| 65 | | ffn 6736 |
. . . . . 6
⊢
(♯:V⟶(ℕ0 ∪ {+∞}) → ♯
Fn V) |
| 66 | | elpreima 7078 |
. . . . . 6
⊢ (♯
Fn V → (𝑊 ∈
(◡♯ “ {0, 1}) ↔ (𝑊 ∈ V ∧
(♯‘𝑊) ∈
{0, 1}))) |
| 67 | 64, 65, 66 | mp2b 10 |
. . . . 5
⊢ (𝑊 ∈ (◡♯ “ {0, 1}) ↔ (𝑊 ∈ V ∧
(♯‘𝑊) ∈
{0, 1})) |
| 68 | 63, 67 | sylib 218 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) → (𝑊 ∈ V ∧
(♯‘𝑊) ∈
{0, 1})) |
| 69 | 68 | simprd 495 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) →
(♯‘𝑊) ∈
{0, 1}) |
| 70 | | elpri 4649 |
. . 3
⊢
((♯‘𝑊)
∈ {0, 1} → ((♯‘𝑊) = 0 ∨ (♯‘𝑊) = 1)) |
| 71 | 69, 70 | syl 17 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) →
((♯‘𝑊) = 0 ∨
(♯‘𝑊) =
1)) |
| 72 | 41, 62, 71 | mpjaodan 961 |
1
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) → (𝐶‘𝑊) = ( I ↾ 𝐷)) |