| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | cycpmconjv.s | . . . . . . 7
⊢ 𝑆 = (SymGrp‘𝐷) | 
| 2 |  | cycpmconjv.b | . . . . . . 7
⊢ 𝐵 = (Base‘𝑆) | 
| 3 | 1, 2 | symgbasf1o 19393 | . . . . . 6
⊢ (𝐺 ∈ 𝐵 → 𝐺:𝐷–1-1-onto→𝐷) | 
| 4 | 3 | 3ad2ant2 1134 | . . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝐺:𝐷–1-1-onto→𝐷) | 
| 5 |  | simp3 1138 | . . . . . . . . . 10
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝑊 ∈ dom 𝑀) | 
| 6 |  | cycpmconjv.m | . . . . . . . . . . . . 13
⊢ 𝑀 = (toCyc‘𝐷) | 
| 7 | 6, 1, 2 | tocycf 33138 | . . . . . . . . . . . 12
⊢ (𝐷 ∈ 𝑉 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵) | 
| 8 | 7 | 3ad2ant1 1133 | . . . . . . . . . . 11
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵) | 
| 9 | 8 | fdmd 6745 | . . . . . . . . . 10
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → dom 𝑀 = {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) | 
| 10 | 5, 9 | eleqtrd 2842 | . . . . . . . . 9
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) | 
| 11 |  | id 22 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) | 
| 12 |  | dmeq 5913 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊) | 
| 13 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → 𝐷 = 𝐷) | 
| 14 | 11, 12, 13 | f1eq123d 6839 | . . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑊:dom 𝑊–1-1→𝐷)) | 
| 15 | 14 | elrab 3691 | . . . . . . . . 9
⊢ (𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) | 
| 16 | 10, 15 | sylib 218 | . . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) | 
| 17 | 16 | simprd 495 | . . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝑊:dom 𝑊–1-1→𝐷) | 
| 18 |  | f1f 6803 | . . . . . . 7
⊢ (𝑊:dom 𝑊–1-1→𝐷 → 𝑊:dom 𝑊⟶𝐷) | 
| 19 | 17, 18 | syl 17 | . . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝑊:dom 𝑊⟶𝐷) | 
| 20 | 19 | frnd 6743 | . . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ran 𝑊 ⊆ 𝐷) | 
| 21 | 4, 20 | cycpmconjvlem 33162 | . . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∘ ◡𝐺) = ( I ↾ (𝐷 ∖ ran (𝐺 ↾ ran 𝑊)))) | 
| 22 |  | rnco 6271 | . . . . . 6
⊢ ran
(𝐺 ∘ 𝑊) = ran (𝐺 ↾ ran 𝑊) | 
| 23 | 22 | difeq2i 4122 | . . . . 5
⊢ (𝐷 ∖ ran (𝐺 ∘ 𝑊)) = (𝐷 ∖ ran (𝐺 ↾ ran 𝑊)) | 
| 24 | 23 | reseq2i 5993 | . . . 4
⊢ ( I
↾ (𝐷 ∖ ran
(𝐺 ∘ 𝑊))) = ( I ↾ (𝐷 ∖ ran (𝐺 ↾ ran 𝑊))) | 
| 25 | 21, 24 | eqtr4di 2794 | . . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∘ ◡𝐺) = ( I ↾ (𝐷 ∖ ran (𝐺 ∘ 𝑊)))) | 
| 26 |  | coass 6284 | . . . . 5
⊢ ((((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊) ∘ ◡𝐺) = (((𝐺 ∘ 𝑊) cyclShift 1) ∘ (◡𝑊 ∘ ◡𝐺)) | 
| 27 |  | cnvco 5895 | . . . . . 6
⊢ ◡(𝐺 ∘ 𝑊) = (◡𝑊 ∘ ◡𝐺) | 
| 28 | 27 | coeq2i 5870 | . . . . 5
⊢ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡(𝐺 ∘ 𝑊)) = (((𝐺 ∘ 𝑊) cyclShift 1) ∘ (◡𝑊 ∘ ◡𝐺)) | 
| 29 | 26, 28 | eqtr4i 2767 | . . . 4
⊢ ((((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊) ∘ ◡𝐺) = (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡(𝐺 ∘ 𝑊)) | 
| 30 | 29 | a1i 11 | . . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊) ∘ ◡𝐺) = (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡(𝐺 ∘ 𝑊))) | 
| 31 | 25, 30 | uneq12d 4168 | . 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∘ ◡𝐺) ∪ ((((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊) ∘ ◡𝐺)) = (( I ↾ (𝐷 ∖ ran (𝐺 ∘ 𝑊))) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡(𝐺 ∘ 𝑊)))) | 
| 32 |  | simp2 1137 | . . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝐺 ∈ 𝐵) | 
| 33 | 8, 10 | ffvelcdmd 7104 | . . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝑀‘𝑊) ∈ 𝐵) | 
| 34 |  | cycpmconjv.p | . . . . . . . 8
⊢  + =
(+g‘𝑆) | 
| 35 | 1, 2, 34 | symgcl 19403 | . . . . . . 7
⊢ ((𝐺 ∈ 𝐵 ∧ (𝑀‘𝑊) ∈ 𝐵) → (𝐺 + (𝑀‘𝑊)) ∈ 𝐵) | 
| 36 | 32, 33, 35 | syl2anc 584 | . . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 + (𝑀‘𝑊)) ∈ 𝐵) | 
| 37 |  | eqid 2736 | . . . . . . 7
⊢
(invg‘𝑆) = (invg‘𝑆) | 
| 38 |  | cycpmconjv.l | . . . . . . 7
⊢  − =
(-g‘𝑆) | 
| 39 | 2, 34, 37, 38 | grpsubval 19004 | . . . . . 6
⊢ (((𝐺 + (𝑀‘𝑊)) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐺 + (𝑀‘𝑊)) − 𝐺) = ((𝐺 + (𝑀‘𝑊)) +
((invg‘𝑆)‘𝐺))) | 
| 40 | 36, 32, 39 | syl2anc 584 | . . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) − 𝐺) = ((𝐺 + (𝑀‘𝑊)) +
((invg‘𝑆)‘𝐺))) | 
| 41 | 1, 2, 37 | symginv 19421 | . . . . . . 7
⊢ (𝐺 ∈ 𝐵 → ((invg‘𝑆)‘𝐺) = ◡𝐺) | 
| 42 | 41 | 3ad2ant2 1134 | . . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((invg‘𝑆)‘𝐺) = ◡𝐺) | 
| 43 | 42 | oveq2d 7448 | . . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) +
((invg‘𝑆)‘𝐺)) = ((𝐺 + (𝑀‘𝑊)) + ◡𝐺)) | 
| 44 |  | simp1 1136 | . . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝐷 ∈ 𝑉) | 
| 45 |  | f1ocnv 6859 | . . . . . . . 8
⊢ (𝐺:𝐷–1-1-onto→𝐷 → ◡𝐺:𝐷–1-1-onto→𝐷) | 
| 46 | 4, 45 | syl 17 | . . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ◡𝐺:𝐷–1-1-onto→𝐷) | 
| 47 | 1, 2 | elsymgbas 19392 | . . . . . . . 8
⊢ (𝐷 ∈ 𝑉 → (◡𝐺 ∈ 𝐵 ↔ ◡𝐺:𝐷–1-1-onto→𝐷)) | 
| 48 | 47 | biimpar 477 | . . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ ◡𝐺:𝐷–1-1-onto→𝐷) → ◡𝐺 ∈ 𝐵) | 
| 49 | 44, 46, 48 | syl2anc 584 | . . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ◡𝐺 ∈ 𝐵) | 
| 50 | 1, 2, 34 | symgov 19402 | . . . . . 6
⊢ (((𝐺 + (𝑀‘𝑊)) ∈ 𝐵 ∧ ◡𝐺 ∈ 𝐵) → ((𝐺 + (𝑀‘𝑊)) + ◡𝐺) = ((𝐺 + (𝑀‘𝑊)) ∘ ◡𝐺)) | 
| 51 | 36, 49, 50 | syl2anc 584 | . . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) + ◡𝐺) = ((𝐺 + (𝑀‘𝑊)) ∘ ◡𝐺)) | 
| 52 | 40, 43, 51 | 3eqtrd 2780 | . . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) − 𝐺) = ((𝐺 + (𝑀‘𝑊)) ∘ ◡𝐺)) | 
| 53 | 1, 2, 34 | symgov 19402 | . . . . . . . 8
⊢ ((𝐺 ∈ 𝐵 ∧ (𝑀‘𝑊) ∈ 𝐵) → (𝐺 + (𝑀‘𝑊)) = (𝐺 ∘ (𝑀‘𝑊))) | 
| 54 | 32, 33, 53 | syl2anc 584 | . . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 + (𝑀‘𝑊)) = (𝐺 ∘ (𝑀‘𝑊))) | 
| 55 | 16 | simpld 494 | . . . . . . . . 9
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝑊 ∈ Word 𝐷) | 
| 56 | 6, 44, 55, 17 | tocycfv 33130 | . . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝑀‘𝑊) = (( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊))) | 
| 57 | 56 | coeq2d 5872 | . . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ (𝑀‘𝑊)) = (𝐺 ∘ (( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊)))) | 
| 58 |  | coundi 6266 | . . . . . . . 8
⊢ (𝐺 ∘ (( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊))) = ((𝐺 ∘ ( I ↾ (𝐷 ∖ ran 𝑊))) ∪ (𝐺 ∘ ((𝑊 cyclShift 1) ∘ ◡𝑊))) | 
| 59 | 58 | a1i 11 | . . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ (( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊))) = ((𝐺 ∘ ( I ↾ (𝐷 ∖ ran 𝑊))) ∪ (𝐺 ∘ ((𝑊 cyclShift 1) ∘ ◡𝑊)))) | 
| 60 | 54, 57, 59 | 3eqtrd 2780 | . . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 + (𝑀‘𝑊)) = ((𝐺 ∘ ( I ↾ (𝐷 ∖ ran 𝑊))) ∪ (𝐺 ∘ ((𝑊 cyclShift 1) ∘ ◡𝑊)))) | 
| 61 |  | coires1 6283 | . . . . . . . 8
⊢ (𝐺 ∘ ( I ↾ (𝐷 ∖ ran 𝑊))) = (𝐺 ↾ (𝐷 ∖ ran 𝑊)) | 
| 62 | 61 | a1i 11 | . . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ ( I ↾ (𝐷 ∖ ran 𝑊))) = (𝐺 ↾ (𝐷 ∖ ran 𝑊))) | 
| 63 |  | coass 6284 | . . . . . . . 8
⊢ ((𝐺 ∘ (𝑊 cyclShift 1)) ∘ ◡𝑊) = (𝐺 ∘ ((𝑊 cyclShift 1) ∘ ◡𝑊)) | 
| 64 |  | 1zzd 12650 | . . . . . . . . . 10
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 1 ∈ ℤ) | 
| 65 |  | f1of 6847 | . . . . . . . . . . 11
⊢ (𝐺:𝐷–1-1-onto→𝐷 → 𝐺:𝐷⟶𝐷) | 
| 66 | 4, 65 | syl 17 | . . . . . . . . . 10
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝐺:𝐷⟶𝐷) | 
| 67 |  | cshco 14876 | . . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ ∧ 𝐺:𝐷⟶𝐷) → (𝐺 ∘ (𝑊 cyclShift 1)) = ((𝐺 ∘ 𝑊) cyclShift 1)) | 
| 68 | 55, 64, 66, 67 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ (𝑊 cyclShift 1)) = ((𝐺 ∘ 𝑊) cyclShift 1)) | 
| 69 | 68 | coeq1d 5871 | . . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 ∘ (𝑊 cyclShift 1)) ∘ ◡𝑊) = (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊)) | 
| 70 | 63, 69 | eqtr3id 2790 | . . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ ((𝑊 cyclShift 1) ∘ ◡𝑊)) = (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊)) | 
| 71 | 62, 70 | uneq12d 4168 | . . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 ∘ ( I ↾ (𝐷 ∖ ran 𝑊))) ∪ (𝐺 ∘ ((𝑊 cyclShift 1) ∘ ◡𝑊))) = ((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊))) | 
| 72 | 60, 71 | eqtrd 2776 | . . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 + (𝑀‘𝑊)) = ((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊))) | 
| 73 | 72 | coeq1d 5871 | . . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) ∘ ◡𝐺) = (((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊)) ∘ ◡𝐺)) | 
| 74 | 52, 73 | eqtrd 2776 | . . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) − 𝐺) = (((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊)) ∘ ◡𝐺)) | 
| 75 |  | coundir 6267 | . . 3
⊢ (((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊)) ∘ ◡𝐺) = (((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∘ ◡𝐺) ∪ ((((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊) ∘ ◡𝐺)) | 
| 76 | 74, 75 | eqtrdi 2792 | . 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) − 𝐺) = (((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∘ ◡𝐺) ∪ ((((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊) ∘ ◡𝐺))) | 
| 77 |  | wrdco 14871 | . . . 4
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐺:𝐷⟶𝐷) → (𝐺 ∘ 𝑊) ∈ Word 𝐷) | 
| 78 | 55, 66, 77 | syl2anc 584 | . . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ 𝑊) ∈ Word 𝐷) | 
| 79 |  | f1of1 6846 | . . . . . 6
⊢ (𝐺:𝐷–1-1-onto→𝐷 → 𝐺:𝐷–1-1→𝐷) | 
| 80 | 4, 79 | syl 17 | . . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝐺:𝐷–1-1→𝐷) | 
| 81 |  | f1co 6814 | . . . . 5
⊢ ((𝐺:𝐷–1-1→𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷) → (𝐺 ∘ 𝑊):dom 𝑊–1-1→𝐷) | 
| 82 | 80, 17, 81 | syl2anc 584 | . . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ 𝑊):dom 𝑊–1-1→𝐷) | 
| 83 | 66 | fdmd 6745 | . . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → dom 𝐺 = 𝐷) | 
| 84 | 20, 83 | sseqtrrd 4020 | . . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ran 𝑊 ⊆ dom 𝐺) | 
| 85 |  | dmcosseq 5986 | . . . . . 6
⊢ (ran
𝑊 ⊆ dom 𝐺 → dom (𝐺 ∘ 𝑊) = dom 𝑊) | 
| 86 | 84, 85 | syl 17 | . . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → dom (𝐺 ∘ 𝑊) = dom 𝑊) | 
| 87 |  | f1eq2 6799 | . . . . 5
⊢ (dom
(𝐺 ∘ 𝑊) = dom 𝑊 → ((𝐺 ∘ 𝑊):dom (𝐺 ∘ 𝑊)–1-1→𝐷 ↔ (𝐺 ∘ 𝑊):dom 𝑊–1-1→𝐷)) | 
| 88 | 86, 87 | syl 17 | . . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 ∘ 𝑊):dom (𝐺 ∘ 𝑊)–1-1→𝐷 ↔ (𝐺 ∘ 𝑊):dom 𝑊–1-1→𝐷)) | 
| 89 | 82, 88 | mpbird 257 | . . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ 𝑊):dom (𝐺 ∘ 𝑊)–1-1→𝐷) | 
| 90 | 6, 44, 78, 89 | tocycfv 33130 | . 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝑀‘(𝐺 ∘ 𝑊)) = (( I ↾ (𝐷 ∖ ran (𝐺 ∘ 𝑊))) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡(𝐺 ∘ 𝑊)))) | 
| 91 | 31, 76, 90 | 3eqtr4d 2786 | 1
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) − 𝐺) = (𝑀‘(𝐺 ∘ 𝑊))) |