Step | Hyp | Ref
| Expression |
1 | | cycpmconjv.s |
. . . . . . 7
⊢ 𝑆 = (SymGrp‘𝐷) |
2 | | cycpmconjv.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑆) |
3 | 1, 2 | symgbasf1o 18767 |
. . . . . 6
⊢ (𝐺 ∈ 𝐵 → 𝐺:𝐷–1-1-onto→𝐷) |
4 | 3 | 3ad2ant2 1136 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝐺:𝐷–1-1-onto→𝐷) |
5 | | simp3 1140 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝑊 ∈ dom 𝑀) |
6 | | cycpmconjv.m |
. . . . . . . . . . . . 13
⊢ 𝑀 = (toCyc‘𝐷) |
7 | 6, 1, 2 | tocycf 31103 |
. . . . . . . . . . . 12
⊢ (𝐷 ∈ 𝑉 → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵) |
8 | 7 | 3ad2ant1 1135 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝑀:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵) |
9 | 8 | fdmd 6556 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → dom 𝑀 = {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
10 | 5, 9 | eleqtrd 2840 |
. . . . . . . . 9
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}) |
11 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) |
12 | | dmeq 5772 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → dom 𝑤 = dom 𝑊) |
13 | | eqidd 2738 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → 𝐷 = 𝐷) |
14 | 11, 12, 13 | f1eq123d 6653 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (𝑤:dom 𝑤–1-1→𝐷 ↔ 𝑊:dom 𝑊–1-1→𝐷)) |
15 | 14 | elrab 3602 |
. . . . . . . . 9
⊢ (𝑊 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷} ↔ (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) |
16 | 10, 15 | sylib 221 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷)) |
17 | 16 | simprd 499 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝑊:dom 𝑊–1-1→𝐷) |
18 | | f1f 6615 |
. . . . . . 7
⊢ (𝑊:dom 𝑊–1-1→𝐷 → 𝑊:dom 𝑊⟶𝐷) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝑊:dom 𝑊⟶𝐷) |
20 | 19 | frnd 6553 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ran 𝑊 ⊆ 𝐷) |
21 | 4, 20 | cycpmconjvlem 31127 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∘ ◡𝐺) = ( I ↾ (𝐷 ∖ ran (𝐺 ↾ ran 𝑊)))) |
22 | | rnco 6116 |
. . . . . 6
⊢ ran
(𝐺 ∘ 𝑊) = ran (𝐺 ↾ ran 𝑊) |
23 | 22 | difeq2i 4034 |
. . . . 5
⊢ (𝐷 ∖ ran (𝐺 ∘ 𝑊)) = (𝐷 ∖ ran (𝐺 ↾ ran 𝑊)) |
24 | 23 | reseq2i 5848 |
. . . 4
⊢ ( I
↾ (𝐷 ∖ ran
(𝐺 ∘ 𝑊))) = ( I ↾ (𝐷 ∖ ran (𝐺 ↾ ran 𝑊))) |
25 | 21, 24 | eqtr4di 2796 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∘ ◡𝐺) = ( I ↾ (𝐷 ∖ ran (𝐺 ∘ 𝑊)))) |
26 | | coass 6129 |
. . . . 5
⊢ ((((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊) ∘ ◡𝐺) = (((𝐺 ∘ 𝑊) cyclShift 1) ∘ (◡𝑊 ∘ ◡𝐺)) |
27 | | cnvco 5754 |
. . . . . 6
⊢ ◡(𝐺 ∘ 𝑊) = (◡𝑊 ∘ ◡𝐺) |
28 | 27 | coeq2i 5729 |
. . . . 5
⊢ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡(𝐺 ∘ 𝑊)) = (((𝐺 ∘ 𝑊) cyclShift 1) ∘ (◡𝑊 ∘ ◡𝐺)) |
29 | 26, 28 | eqtr4i 2768 |
. . . 4
⊢ ((((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊) ∘ ◡𝐺) = (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡(𝐺 ∘ 𝑊)) |
30 | 29 | a1i 11 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊) ∘ ◡𝐺) = (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡(𝐺 ∘ 𝑊))) |
31 | 25, 30 | uneq12d 4078 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∘ ◡𝐺) ∪ ((((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊) ∘ ◡𝐺)) = (( I ↾ (𝐷 ∖ ran (𝐺 ∘ 𝑊))) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡(𝐺 ∘ 𝑊)))) |
32 | | simp2 1139 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝐺 ∈ 𝐵) |
33 | 8, 10 | ffvelrnd 6905 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝑀‘𝑊) ∈ 𝐵) |
34 | | cycpmconjv.p |
. . . . . . . 8
⊢ + =
(+g‘𝑆) |
35 | 1, 2, 34 | symgcl 18777 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝐵 ∧ (𝑀‘𝑊) ∈ 𝐵) → (𝐺 + (𝑀‘𝑊)) ∈ 𝐵) |
36 | 32, 33, 35 | syl2anc 587 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 + (𝑀‘𝑊)) ∈ 𝐵) |
37 | | eqid 2737 |
. . . . . . 7
⊢
(invg‘𝑆) = (invg‘𝑆) |
38 | | cycpmconjv.l |
. . . . . . 7
⊢ − =
(-g‘𝑆) |
39 | 2, 34, 37, 38 | grpsubval 18413 |
. . . . . 6
⊢ (((𝐺 + (𝑀‘𝑊)) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐺 + (𝑀‘𝑊)) − 𝐺) = ((𝐺 + (𝑀‘𝑊)) +
((invg‘𝑆)‘𝐺))) |
40 | 36, 32, 39 | syl2anc 587 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) − 𝐺) = ((𝐺 + (𝑀‘𝑊)) +
((invg‘𝑆)‘𝐺))) |
41 | 1, 2, 37 | symginv 18794 |
. . . . . . 7
⊢ (𝐺 ∈ 𝐵 → ((invg‘𝑆)‘𝐺) = ◡𝐺) |
42 | 41 | 3ad2ant2 1136 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((invg‘𝑆)‘𝐺) = ◡𝐺) |
43 | 42 | oveq2d 7229 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) +
((invg‘𝑆)‘𝐺)) = ((𝐺 + (𝑀‘𝑊)) + ◡𝐺)) |
44 | | simp1 1138 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝐷 ∈ 𝑉) |
45 | | f1ocnv 6673 |
. . . . . . . 8
⊢ (𝐺:𝐷–1-1-onto→𝐷 → ◡𝐺:𝐷–1-1-onto→𝐷) |
46 | 4, 45 | syl 17 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ◡𝐺:𝐷–1-1-onto→𝐷) |
47 | 1, 2 | elsymgbas 18766 |
. . . . . . . 8
⊢ (𝐷 ∈ 𝑉 → (◡𝐺 ∈ 𝐵 ↔ ◡𝐺:𝐷–1-1-onto→𝐷)) |
48 | 47 | biimpar 481 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ ◡𝐺:𝐷–1-1-onto→𝐷) → ◡𝐺 ∈ 𝐵) |
49 | 44, 46, 48 | syl2anc 587 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ◡𝐺 ∈ 𝐵) |
50 | 1, 2, 34 | symgov 18776 |
. . . . . 6
⊢ (((𝐺 + (𝑀‘𝑊)) ∈ 𝐵 ∧ ◡𝐺 ∈ 𝐵) → ((𝐺 + (𝑀‘𝑊)) + ◡𝐺) = ((𝐺 + (𝑀‘𝑊)) ∘ ◡𝐺)) |
51 | 36, 49, 50 | syl2anc 587 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) + ◡𝐺) = ((𝐺 + (𝑀‘𝑊)) ∘ ◡𝐺)) |
52 | 40, 43, 51 | 3eqtrd 2781 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) − 𝐺) = ((𝐺 + (𝑀‘𝑊)) ∘ ◡𝐺)) |
53 | 1, 2, 34 | symgov 18776 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝐵 ∧ (𝑀‘𝑊) ∈ 𝐵) → (𝐺 + (𝑀‘𝑊)) = (𝐺 ∘ (𝑀‘𝑊))) |
54 | 32, 33, 53 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 + (𝑀‘𝑊)) = (𝐺 ∘ (𝑀‘𝑊))) |
55 | 16 | simpld 498 |
. . . . . . . . 9
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝑊 ∈ Word 𝐷) |
56 | 6, 44, 55, 17 | tocycfv 31095 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝑀‘𝑊) = (( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊))) |
57 | 56 | coeq2d 5731 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ (𝑀‘𝑊)) = (𝐺 ∘ (( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊)))) |
58 | | coundi 6111 |
. . . . . . . 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 2781 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 + (𝑀‘𝑊)) = ((𝐺 ∘ ( I ↾ (𝐷 ∖ ran 𝑊))) ∪ (𝐺 ∘ ((𝑊 cyclShift 1) ∘ ◡𝑊)))) |
61 | | coires1 6128 |
. . . . . . . 8
⊢ (𝐺 ∘ ( I ↾ (𝐷 ∖ ran 𝑊))) = (𝐺 ↾ (𝐷 ∖ ran 𝑊)) |
62 | 61 | a1i 11 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ ( I ↾ (𝐷 ∖ ran 𝑊))) = (𝐺 ↾ (𝐷 ∖ ran 𝑊))) |
63 | | coass 6129 |
. . . . . . . 8
⊢ ((𝐺 ∘ (𝑊 cyclShift 1)) ∘ ◡𝑊) = (𝐺 ∘ ((𝑊 cyclShift 1) ∘ ◡𝑊)) |
64 | | 1zzd 12208 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 1 ∈ ℤ) |
65 | | f1of 6661 |
. . . . . . . . . . 11
⊢ (𝐺:𝐷–1-1-onto→𝐷 → 𝐺:𝐷⟶𝐷) |
66 | 4, 65 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝐺:𝐷⟶𝐷) |
67 | | cshco 14401 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ ∧ 𝐺:𝐷⟶𝐷) → (𝐺 ∘ (𝑊 cyclShift 1)) = ((𝐺 ∘ 𝑊) cyclShift 1)) |
68 | 55, 64, 66, 67 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ (𝑊 cyclShift 1)) = ((𝐺 ∘ 𝑊) cyclShift 1)) |
69 | 68 | coeq1d 5730 |
. . . . . . . 8
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 ∘ (𝑊 cyclShift 1)) ∘ ◡𝑊) = (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊)) |
70 | 63, 69 | eqtr3id 2792 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ ((𝑊 cyclShift 1) ∘ ◡𝑊)) = (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊)) |
71 | 62, 70 | uneq12d 4078 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 ∘ ( I ↾ (𝐷 ∖ ran 𝑊))) ∪ (𝐺 ∘ ((𝑊 cyclShift 1) ∘ ◡𝑊))) = ((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊))) |
72 | 60, 71 | eqtrd 2777 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 + (𝑀‘𝑊)) = ((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊))) |
73 | 72 | coeq1d 5730 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) ∘ ◡𝐺) = (((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊)) ∘ ◡𝐺)) |
74 | 52, 73 | eqtrd 2777 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) − 𝐺) = (((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊)) ∘ ◡𝐺)) |
75 | | coundir 6112 |
. . 3
⊢ (((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊)) ∘ ◡𝐺) = (((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∘ ◡𝐺) ∪ ((((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊) ∘ ◡𝐺)) |
76 | 74, 75 | eqtrdi 2794 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) − 𝐺) = (((𝐺 ↾ (𝐷 ∖ ran 𝑊)) ∘ ◡𝐺) ∪ ((((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡𝑊) ∘ ◡𝐺))) |
77 | | wrdco 14396 |
. . . 4
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝐺:𝐷⟶𝐷) → (𝐺 ∘ 𝑊) ∈ Word 𝐷) |
78 | 55, 66, 77 | syl2anc 587 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ 𝑊) ∈ Word 𝐷) |
79 | | f1of1 6660 |
. . . . . 6
⊢ (𝐺:𝐷–1-1-onto→𝐷 → 𝐺:𝐷–1-1→𝐷) |
80 | 4, 79 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → 𝐺:𝐷–1-1→𝐷) |
81 | | f1co 6627 |
. . . . 5
⊢ ((𝐺:𝐷–1-1→𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷) → (𝐺 ∘ 𝑊):dom 𝑊–1-1→𝐷) |
82 | 80, 17, 81 | syl2anc 587 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ 𝑊):dom 𝑊–1-1→𝐷) |
83 | 66 | fdmd 6556 |
. . . . . . 7
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → dom 𝐺 = 𝐷) |
84 | 20, 83 | sseqtrrd 3942 |
. . . . . 6
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ran 𝑊 ⊆ dom 𝐺) |
85 | | dmcosseq 5842 |
. . . . . 6
⊢ (ran
𝑊 ⊆ dom 𝐺 → dom (𝐺 ∘ 𝑊) = dom 𝑊) |
86 | 84, 85 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → dom (𝐺 ∘ 𝑊) = dom 𝑊) |
87 | | f1eq2 6611 |
. . . . 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 260 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝐺 ∘ 𝑊):dom (𝐺 ∘ 𝑊)–1-1→𝐷) |
90 | 6, 44, 78, 89 | tocycfv 31095 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → (𝑀‘(𝐺 ∘ 𝑊)) = (( I ↾ (𝐷 ∖ ran (𝐺 ∘ 𝑊))) ∪ (((𝐺 ∘ 𝑊) cyclShift 1) ∘ ◡(𝐺 ∘ 𝑊)))) |
91 | 31, 76, 90 | 3eqtr4d 2787 |
1
⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) − 𝐺) = (𝑀‘(𝐺 ∘ 𝑊))) |