Metamath Proof Explorer

Theorem cycpmconjv

Description: A formula for computing conjugacy classes of cyclic permutations. Formula in property (b) of Lang p. 32. (Contributed by Thierry Arnoux, 9-Oct-2023)

Ref Expression
Hypotheses cycpmconjv.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
cycpmconjv.m ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
cycpmconjv.p ⊢ + = ( +g ‘ 𝑆 )
cycpmconjv.l ⊢ − = ( -g ‘ 𝑆 )
cycpmconjv.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion cycpmconjv ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) − 𝐺 ) = ( 𝑀 ‘ ( 𝐺 ∘ 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 cycpmconjv.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
2 cycpmconjv.m ⊢ 𝑀 = ( toCyc ‘ 𝐷 )
3 cycpmconjv.p ⊢ + = ( +g ‘ 𝑆 )
4 cycpmconjv.l ⊢ − = ( -g ‘ 𝑆 )
5 cycpmconjv.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
6 1 5 symgbasf1o ⊢ ( 𝐺 ∈ 𝐵 → 𝐺 : 𝐷 –1-1-onto→ 𝐷 )
7 6 3ad2ant2 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → 𝐺 : 𝐷 –1-1-onto→ 𝐷 )
8 simp3 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → 𝑊 ∈ dom 𝑀 )
9 2 1 5 tocycf ⊢ ( 𝐷 ∈ 𝑉 → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ 𝐵 )
10 9 3ad2ant1 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → 𝑀 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ 𝐵 )
11 10 fdmd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → dom 𝑀 = { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
12 8 11 eleqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
13 id ⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 )
14 dmeq ⊢ ( 𝑤 = 𝑊 → dom 𝑤 = dom 𝑊 )
15 eqidd ⊢ ( 𝑤 = 𝑊 → 𝐷 = 𝐷 )
16 13 14 15 f1eq123d ⊢ ( 𝑤 = 𝑊 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
17 16 elrab ⊢ ( 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
18 12 17 sylib ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
19 18 simprd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
20 f1f ⊢ ( 𝑊 : dom 𝑊 –1-1→ 𝐷 → 𝑊 : dom 𝑊 ⟶ 𝐷 )
21 19 20 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → 𝑊 : dom 𝑊 ⟶ 𝐷 )
22 21 frnd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ran 𝑊 ⊆ 𝐷 )
23 7 22 cycpmconjvlem ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∘ ◡ 𝐺 ) = ( I ↾ ( 𝐷 ∖ ran ( 𝐺 ↾ ran 𝑊 ) ) ) )
24 rnco ⊢ ran ( 𝐺 ∘ 𝑊 ) = ran ( 𝐺 ↾ ran 𝑊 )
25 24 difeq2i ⊢ ( 𝐷 ∖ ran ( 𝐺 ∘ 𝑊 ) ) = ( 𝐷 ∖ ran ( 𝐺 ↾ ran 𝑊 ) )
26 25 reseq2i ⊢ ( I ↾ ( 𝐷 ∖ ran ( 𝐺 ∘ 𝑊 ) ) ) = ( I ↾ ( 𝐷 ∖ ran ( 𝐺 ↾ ran 𝑊 ) ) )
27 23 26 eqtr4di ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∘ ◡ 𝐺 ) = ( I ↾ ( 𝐷 ∖ ran ( 𝐺 ∘ 𝑊 ) ) ) )
28 coass ⊢ ( ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ 𝑊 ) ∘ ◡ 𝐺 ) = ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ( ◡ 𝑊 ∘ ◡ 𝐺 ) )
29 cnvco ⊢ ◡ ( 𝐺 ∘ 𝑊 ) = ( ◡ 𝑊 ∘ ◡ 𝐺 )
30 29 coeq2i ⊢ ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ ( 𝐺 ∘ 𝑊 ) ) = ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ( ◡ 𝑊 ∘ ◡ 𝐺 ) )
31 28 30 eqtr4i ⊢ ( ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ 𝑊 ) ∘ ◡ 𝐺 ) = ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ ( 𝐺 ∘ 𝑊 ) )
32 31 a1i ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ 𝑊 ) ∘ ◡ 𝐺 ) = ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ ( 𝐺 ∘ 𝑊 ) ) )
33 27 32 uneq12d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( ( 𝐺 ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∘ ◡ 𝐺 ) ∪ ( ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ 𝑊 ) ∘ ◡ 𝐺 ) ) = ( ( I ↾ ( 𝐷 ∖ ran ( 𝐺 ∘ 𝑊 ) ) ) ∪ ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ ( 𝐺 ∘ 𝑊 ) ) ) )
34 simp2 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → 𝐺 ∈ 𝐵 )
35 10 12 ffvelrnd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝑀 ‘ 𝑊 ) ∈ 𝐵 )
36 1 5 3 symgcl ⊢ ( ( 𝐺 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑊 ) ∈ 𝐵 ) → ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) ∈ 𝐵 )
37 34 35 36 syl2anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) ∈ 𝐵 )
38 eqid ⊢ ( invg ‘ 𝑆 ) = ( invg ‘ 𝑆 )
39 5 3 38 4 grpsubval ⊢ ( ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) − 𝐺 ) = ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) + ( ( invg ‘ 𝑆 ) ‘ 𝐺 ) ) )
40 37 34 39 syl2anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) − 𝐺 ) = ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) + ( ( invg ‘ 𝑆 ) ‘ 𝐺 ) ) )
41 1 5 38 symginv ⊢ ( 𝐺 ∈ 𝐵 → ( ( invg ‘ 𝑆 ) ‘ 𝐺 ) = ◡ 𝐺 )
42 41 3ad2ant2 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( invg ‘ 𝑆 ) ‘ 𝐺 ) = ◡ 𝐺 )
43 42 oveq2d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) + ( ( invg ‘ 𝑆 ) ‘ 𝐺 ) ) = ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) + ◡ 𝐺 ) )
44 simp1 ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → 𝐷 ∈ 𝑉 )
45 f1ocnv ⊢ ( 𝐺 : 𝐷 –1-1-onto→ 𝐷 → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐷 )
46 7 45 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐷 )
47 1 5 elsymgbas ⊢ ( 𝐷 ∈ 𝑉 → ( ◡ 𝐺 ∈ 𝐵 ↔ ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) )
48 47 biimpar ⊢ ( ( 𝐷 ∈ 𝑉 ∧ ◡ 𝐺 : 𝐷 –1-1-onto→ 𝐷 ) → ◡ 𝐺 ∈ 𝐵 )
49 44 46 48 syl2anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ◡ 𝐺 ∈ 𝐵 )
50 1 5 3 symgov ⊢ ( ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) ∈ 𝐵 ∧ ◡ 𝐺 ∈ 𝐵 ) → ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) + ◡ 𝐺 ) = ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) ∘ ◡ 𝐺 ) )
51 37 49 50 syl2anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) + ◡ 𝐺 ) = ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) ∘ ◡ 𝐺 ) )
52 40 43 51 3eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) − 𝐺 ) = ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) ∘ ◡ 𝐺 ) )
53 1 5 3 symgov ⊢ ( ( 𝐺 ∈ 𝐵 ∧ ( 𝑀 ‘ 𝑊 ) ∈ 𝐵 ) → ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) = ( 𝐺 ∘ ( 𝑀 ‘ 𝑊 ) ) )
54 34 35 53 syl2anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) = ( 𝐺 ∘ ( 𝑀 ‘ 𝑊 ) ) )
55 18 simpld ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → 𝑊 ∈ Word 𝐷 )
56 2 44 55 19 tocycfv ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝑀 ‘ 𝑊 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) )
57 56 coeq2d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝐺 ∘ ( 𝑀 ‘ 𝑊 ) ) = ( 𝐺 ∘ ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ) )
58 coundi ⊢ ( 𝐺 ∘ ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ) = ( ( 𝐺 ∘ ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ) ∪ ( 𝐺 ∘ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) )
59 58 a1i ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝐺 ∘ ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ) = ( ( 𝐺 ∘ ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ) ∪ ( 𝐺 ∘ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ) )
60 54 57 59 3eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) = ( ( 𝐺 ∘ ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ) ∪ ( 𝐺 ∘ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ) )
61 coires1 ⊢ ( 𝐺 ∘ ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ) = ( 𝐺 ↾ ( 𝐷 ∖ ran 𝑊 ) )
62 61 a1i ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝐺 ∘ ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ) = ( 𝐺 ↾ ( 𝐷 ∖ ran 𝑊 ) ) )
63 coass ⊢ ( ( 𝐺 ∘ ( 𝑊 cyclShift 1 ) ) ∘ ◡ 𝑊 ) = ( 𝐺 ∘ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) )
64 1zzd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → 1 ∈ ℤ )
65 f1of ⊢ ( 𝐺 : 𝐷 –1-1-onto→ 𝐷 → 𝐺 : 𝐷 ⟶ 𝐷 )
66 7 65 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → 𝐺 : 𝐷 ⟶ 𝐷 )
67 cshco ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ ∧ 𝐺 : 𝐷 ⟶ 𝐷 ) → ( 𝐺 ∘ ( 𝑊 cyclShift 1 ) ) = ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) )
68 55 64 66 67 syl3anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝐺 ∘ ( 𝑊 cyclShift 1 ) ) = ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) )
69 68 coeq1d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 ∘ ( 𝑊 cyclShift 1 ) ) ∘ ◡ 𝑊 ) = ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ 𝑊 ) )
70 63 69 eqtr3id ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝐺 ∘ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) = ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ 𝑊 ) )
71 62 70 uneq12d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 ∘ ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ) ∪ ( 𝐺 ∘ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) ) = ( ( 𝐺 ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ 𝑊 ) ) )
72 60 71 eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) = ( ( 𝐺 ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ 𝑊 ) ) )
73 72 coeq1d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) ∘ ◡ 𝐺 ) = ( ( ( 𝐺 ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ 𝑊 ) ) ∘ ◡ 𝐺 ) )
74 52 73 eqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) − 𝐺 ) = ( ( ( 𝐺 ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ 𝑊 ) ) ∘ ◡ 𝐺 ) )
75 coundir ⊢ ( ( ( 𝐺 ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ 𝑊 ) ) ∘ ◡ 𝐺 ) = ( ( ( 𝐺 ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∘ ◡ 𝐺 ) ∪ ( ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ 𝑊 ) ∘ ◡ 𝐺 ) )
76 74 75 eqtrdi ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) − 𝐺 ) = ( ( ( 𝐺 ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∘ ◡ 𝐺 ) ∪ ( ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ 𝑊 ) ∘ ◡ 𝐺 ) ) )
77 wrdco ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 𝐺 : 𝐷 ⟶ 𝐷 ) → ( 𝐺 ∘ 𝑊 ) ∈ Word 𝐷 )
78 55 66 77 syl2anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝐺 ∘ 𝑊 ) ∈ Word 𝐷 )
79 f1of1 ⊢ ( 𝐺 : 𝐷 –1-1-onto→ 𝐷 → 𝐺 : 𝐷 –1-1→ 𝐷 )
80 7 79 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → 𝐺 : 𝐷 –1-1→ 𝐷 )
81 f1co ⊢ ( ( 𝐺 : 𝐷 –1-1→ 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) → ( 𝐺 ∘ 𝑊 ) : dom 𝑊 –1-1→ 𝐷 )
82 80 19 81 syl2anc ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝐺 ∘ 𝑊 ) : dom 𝑊 –1-1→ 𝐷 )
83 66 fdmd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → dom 𝐺 = 𝐷 )
84 22 83 sseqtrrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ran 𝑊 ⊆ dom 𝐺 )
85 dmcosseq ⊢ ( ran 𝑊 ⊆ dom 𝐺 → dom ( 𝐺 ∘ 𝑊 ) = dom 𝑊 )
86 84 85 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → dom ( 𝐺 ∘ 𝑊 ) = dom 𝑊 )
87 f1eq2 ⊢ ( dom ( 𝐺 ∘ 𝑊 ) = dom 𝑊 → ( ( 𝐺 ∘ 𝑊 ) : dom ( 𝐺 ∘ 𝑊 ) –1-1→ 𝐷 ↔ ( 𝐺 ∘ 𝑊 ) : dom 𝑊 –1-1→ 𝐷 ) )
88 86 87 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 ∘ 𝑊 ) : dom ( 𝐺 ∘ 𝑊 ) –1-1→ 𝐷 ↔ ( 𝐺 ∘ 𝑊 ) : dom 𝑊 –1-1→ 𝐷 ) )
89 82 88 mpbird ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝐺 ∘ 𝑊 ) : dom ( 𝐺 ∘ 𝑊 ) –1-1→ 𝐷 )
90 2 44 78 89 tocycfv ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( 𝑀 ‘ ( 𝐺 ∘ 𝑊 ) ) = ( ( I ↾ ( 𝐷 ∖ ran ( 𝐺 ∘ 𝑊 ) ) ) ∪ ( ( ( 𝐺 ∘ 𝑊 ) cyclShift 1 ) ∘ ◡ ( 𝐺 ∘ 𝑊 ) ) ) )
91 33 76 90 3eqtr4d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀 ) → ( ( 𝐺 + ( 𝑀 ‘ 𝑊 ) ) − 𝐺 ) = ( 𝑀 ‘ ( 𝐺 ∘ 𝑊 ) ) )