Metamath Proof Explorer

Theorem tocycf

Description: The permutation cycle builder as a function. (Contributed by Thierry Arnoux, 25-Sep-2023)

Ref Expression
Hypotheses tocycf.c ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
tocycf.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
tocycf.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
Assertion tocycf ( 𝐷 ∈ 𝑉 → 𝐶 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 tocycf.c ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2 tocycf.s ⊢ 𝑆 = ( SymGrp ‘ 𝐷 )
3 tocycf.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 1 tocycval ⊢ ( 𝐷 ∈ 𝑉 → 𝐶 = ( 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↦ ( ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∪ ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) ) ) )
5 simpr ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → 𝑢 = ∅ )
6 5 rneqd ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → ran 𝑢 = ran ∅ )
7 rn0 ⊢ ran ∅ = ∅
8 6 7 eqtrdi ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → ran 𝑢 = ∅ )
9 8 difeq2d ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → ( 𝐷 ∖ ran 𝑢 ) = ( 𝐷 ∖ ∅ ) )
10 dif0 ⊢ ( 𝐷 ∖ ∅ ) = 𝐷
11 9 10 eqtrdi ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → ( 𝐷 ∖ ran 𝑢 ) = 𝐷 )
12 11 reseq2d ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) = ( I ↾ 𝐷 ) )
13 5 cnveqd ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → ◡ 𝑢 = ◡ ∅ )
14 cnv0 ⊢ ◡ ∅ = ∅
15 13 14 eqtrdi ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → ◡ 𝑢 = ∅ )
16 15 coeq2d ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) = ( ( 𝑢 cyclShift 1 ) ∘ ∅ ) )
17 co02 ⊢ ( ( 𝑢 cyclShift 1 ) ∘ ∅ ) = ∅
18 16 17 eqtrdi ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) = ∅ )
19 12 18 uneq12d ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∪ ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) ) = ( ( I ↾ 𝐷 ) ∪ ∅ ) )
20 un0 ⊢ ( ( I ↾ 𝐷 ) ∪ ∅ ) = ( I ↾ 𝐷 )
21 19 20 eqtrdi ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∪ ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) ) = ( I ↾ 𝐷 ) )
22 2 idresperm ⊢ ( 𝐷 ∈ 𝑉 → ( I ↾ 𝐷 ) ∈ ( Base ‘ 𝑆 ) )
23 22 3 eleqtrrdi ⊢ ( 𝐷 ∈ 𝑉 → ( I ↾ 𝐷 ) ∈ 𝐵 )
24 23 ad2antrr ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → ( I ↾ 𝐷 ) ∈ 𝐵 )
25 21 24 eqeltrd ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 = ∅ ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∪ ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) ) ∈ 𝐵 )
26 difexg ⊢ ( 𝐷 ∈ 𝑉 → ( 𝐷 ∖ ran 𝑢 ) ∈ V )
27 26 resiexd ⊢ ( 𝐷 ∈ 𝑉 → ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∈ V )
28 ovex ⊢ ( 𝑢 cyclShift 1 ) ∈ V
29 vex ⊢ 𝑢 ∈ V
30 29 cnvex ⊢ ◡ 𝑢 ∈ V
31 28 30 coex ⊢ ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) ∈ V
32 unexg ⊢ ( ( ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∈ V ∧ ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) ∈ V ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∪ ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) ) ∈ V )
33 27 31 32 sylancl ⊢ ( 𝐷 ∈ 𝑉 → ( ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∪ ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) ) ∈ V )
34 33 adantr ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∪ ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) ) ∈ V )
35 4 34 fvmpt2d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) → ( 𝐶 ‘ 𝑢 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∪ ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) ) )
36 35 adantr ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 ≠ ∅ ) → ( 𝐶 ‘ 𝑢 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∪ ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) ) )
37 simpll ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 ≠ ∅ ) → 𝐷 ∈ 𝑉 )
38 simplr ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 ≠ ∅ ) → 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
39 id ⊢ ( 𝑤 = 𝑢 → 𝑤 = 𝑢 )
40 dmeq ⊢ ( 𝑤 = 𝑢 → dom 𝑤 = dom 𝑢 )
41 eqidd ⊢ ( 𝑤 = 𝑢 → 𝐷 = 𝐷 )
42 39 40 41 f1eq123d ⊢ ( 𝑤 = 𝑢 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) )
43 42 elrab ⊢ ( 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ ( 𝑢 ∈ Word 𝐷 ∧ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) )
44 38 43 sylib ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 ≠ ∅ ) → ( 𝑢 ∈ Word 𝐷 ∧ 𝑢 : dom 𝑢 –1-1→ 𝐷 ) )
45 44 simpld ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 ≠ ∅ ) → 𝑢 ∈ Word 𝐷 )
46 44 simprd ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 ≠ ∅ ) → 𝑢 : dom 𝑢 –1-1→ 𝐷 )
47 1 37 45 46 2 cycpmcl ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 ≠ ∅ ) → ( 𝐶 ‘ 𝑢 ) ∈ ( Base ‘ 𝑆 ) )
48 47 3 eleqtrrdi ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 ≠ ∅ ) → ( 𝐶 ‘ 𝑢 ) ∈ 𝐵 )
49 36 48 eqeltrrd ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) ∧ 𝑢 ≠ ∅ ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∪ ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) ) ∈ 𝐵 )
50 25 49 pm2.61dane ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑢 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑢 ) ) ∪ ( ( 𝑢 cyclShift 1 ) ∘ ◡ 𝑢 ) ) ∈ 𝐵 )
51 4 50 fmpt3d ⊢ ( 𝐷 ∈ 𝑉 → 𝐶 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ 𝐵 )