Metamath Proof Explorer

Theorem tocyc01

Description: Permutation cycles built from the empty set or a singleton are the identity. (Contributed by Thierry Arnoux, 21-Nov-2023)

Ref Expression
Hypothesis tocyc01.1 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
Assertion tocyc01 ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ( 𝐶 ‘ 𝑊 ) = ( I ↾ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 tocyc01.1 ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
2 simpl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝐷 ∈ 𝑉 )
3 simpr ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) )
4 3 elin1d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝑊 ∈ dom 𝐶 )
5 eqid ⊢ ( SymGrp ‘ 𝐷 ) = ( SymGrp ‘ 𝐷 )
6 eqid ⊢ ( Base ‘ ( SymGrp ‘ 𝐷 ) ) = ( Base ‘ ( SymGrp ‘ 𝐷 ) )
7 1 5 6 tocycf ⊢ ( 𝐷 ∈ 𝑉 → 𝐶 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ ( SymGrp ‘ 𝐷 ) ) )
8 fdm ⊢ ( 𝐶 : { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ⟶ ( Base ‘ ( SymGrp ‘ 𝐷 ) ) → dom 𝐶 = { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
9 2 7 8 3syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → dom 𝐶 = { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
10 4 9 eleqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } )
11 id ⊢ ( 𝑤 = 𝑊 → 𝑤 = 𝑊 )
12 dmeq ⊢ ( 𝑤 = 𝑊 → dom 𝑤 = dom 𝑊 )
13 eqidd ⊢ ( 𝑤 = 𝑊 → 𝐷 = 𝐷 )
14 11 12 13 f1eq123d ⊢ ( 𝑤 = 𝑊 → ( 𝑤 : dom 𝑤 –1-1→ 𝐷 ↔ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
15 14 elrab ⊢ ( 𝑊 ∈ { 𝑤 ∈ Word 𝐷 ∣ 𝑤 : dom 𝑤 –1-1→ 𝐷 } ↔ ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
16 10 15 sylib ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ( 𝑊 ∈ Word 𝐷 ∧ 𝑊 : dom 𝑊 –1-1→ 𝐷 ) )
17 16 simpld ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝑊 ∈ Word 𝐷 )
18 16 simprd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝑊 : dom 𝑊 –1-1→ 𝐷 )
19 1 2 17 18 tocycfv ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ( 𝐶 ‘ 𝑊 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) )
20 19 adantr ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 0 ) → ( 𝐶 ‘ 𝑊 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) )
21 hasheq0 ⊢ ( 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) → ( ( ♯ ‘ 𝑊 ) = 0 ↔ 𝑊 = ∅ ) )
22 3 21 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ( ( ♯ ‘ 𝑊 ) = 0 ↔ 𝑊 = ∅ ) )
23 22 biimpa ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 0 ) → 𝑊 = ∅ )
24 rneq ⊢ ( 𝑊 = ∅ → ran 𝑊 = ran ∅ )
25 rn0 ⊢ ran ∅ = ∅
26 24 25 eqtrdi ⊢ ( 𝑊 = ∅ → ran 𝑊 = ∅ )
27 26 difeq2d ⊢ ( 𝑊 = ∅ → ( 𝐷 ∖ ran 𝑊 ) = ( 𝐷 ∖ ∅ ) )
28 dif0 ⊢ ( 𝐷 ∖ ∅ ) = 𝐷
29 27 28 eqtrdi ⊢ ( 𝑊 = ∅ → ( 𝐷 ∖ ran 𝑊 ) = 𝐷 )
30 29 reseq2d ⊢ ( 𝑊 = ∅ → ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) = ( I ↾ 𝐷 ) )
31 cnveq ⊢ ( 𝑊 = ∅ → ◡ 𝑊 = ◡ ∅ )
32 cnv0 ⊢ ◡ ∅ = ∅
33 31 32 eqtrdi ⊢ ( 𝑊 = ∅ → ◡ 𝑊 = ∅ )
34 33 coeq2d ⊢ ( 𝑊 = ∅ → ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) = ( ( 𝑊 cyclShift 1 ) ∘ ∅ ) )
35 co02 ⊢ ( ( 𝑊 cyclShift 1 ) ∘ ∅ ) = ∅
36 34 35 eqtrdi ⊢ ( 𝑊 = ∅ → ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) = ∅ )
37 30 36 uneq12d ⊢ ( 𝑊 = ∅ → ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) = ( ( I ↾ 𝐷 ) ∪ ∅ ) )
38 un0 ⊢ ( ( I ↾ 𝐷 ) ∪ ∅ ) = ( I ↾ 𝐷 )
39 37 38 eqtrdi ⊢ ( 𝑊 = ∅ → ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) = ( I ↾ 𝐷 ) )
40 23 39 syl ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 0 ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) = ( I ↾ 𝐷 ) )
41 20 40 eqtrd ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 0 ) → ( 𝐶 ‘ 𝑊 ) = ( I ↾ 𝐷 ) )
42 19 adantr ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝐶 ‘ 𝑊 ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) )
43 17 adantr ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → 𝑊 ∈ Word 𝐷 )
44 1zzd ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → 1 ∈ ℤ )
45 simpr ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( ♯ ‘ 𝑊 ) = 1 )
46 1cshid ⊢ ( ( 𝑊 ∈ Word 𝐷 ∧ 1 ∈ ℤ ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝑊 cyclShift 1 ) = 𝑊 )
47 43 44 45 46 syl3anc ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝑊 cyclShift 1 ) = 𝑊 )
48 47 coeq1d ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) = ( 𝑊 ∘ ◡ 𝑊 ) )
49 wrdf ⊢ ( 𝑊 ∈ Word 𝐷 → 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐷 )
50 ffun ⊢ ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐷 → Fun 𝑊 )
51 funcocnv2 ⊢ ( Fun 𝑊 → ( 𝑊 ∘ ◡ 𝑊 ) = ( I ↾ ran 𝑊 ) )
52 43 49 50 51 4syl ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝑊 ∘ ◡ 𝑊 ) = ( I ↾ ran 𝑊 ) )
53 48 52 eqtrd ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) = ( I ↾ ran 𝑊 ) )
54 53 uneq2d ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( ( 𝑊 cyclShift 1 ) ∘ ◡ 𝑊 ) ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( I ↾ ran 𝑊 ) ) )
55 resundi ⊢ ( I ↾ ( ( 𝐷 ∖ ran 𝑊 ) ∪ ran 𝑊 ) ) = ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( I ↾ ran 𝑊 ) )
56 frn ⊢ ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐷 → ran 𝑊 ⊆ 𝐷 )
57 undifr ⊢ ( ran 𝑊 ⊆ 𝐷 ↔ ( ( 𝐷 ∖ ran 𝑊 ) ∪ ran 𝑊 ) = 𝐷 )
58 56 57 sylib ⊢ ( 𝑊 : ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ⟶ 𝐷 → ( ( 𝐷 ∖ ran 𝑊 ) ∪ ran 𝑊 ) = 𝐷 )
59 43 49 58 3syl ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( ( 𝐷 ∖ ran 𝑊 ) ∪ ran 𝑊 ) = 𝐷 )
60 59 reseq2d ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( I ↾ ( ( 𝐷 ∖ ran 𝑊 ) ∪ ran 𝑊 ) ) = ( I ↾ 𝐷 ) )
61 55 60 eqtr3id ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( ( I ↾ ( 𝐷 ∖ ran 𝑊 ) ) ∪ ( I ↾ ran 𝑊 ) ) = ( I ↾ 𝐷 ) )
62 42 54 61 3eqtrd ⊢ ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) ∧ ( ♯ ‘ 𝑊 ) = 1 ) → ( 𝐶 ‘ 𝑊 ) = ( I ↾ 𝐷 ) )
63 3 elin2d ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → 𝑊 ∈ ( ◡ ♯ “ { 0 , 1 } ) )
64 hashf ⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
65 ffn ⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → ♯ Fn V )
66 elpreima ⊢ ( ♯ Fn V → ( 𝑊 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ ( 𝑊 ∈ V ∧ ( ♯ ‘ 𝑊 ) ∈ { 0 , 1 } ) ) )
67 64 65 66 mp2b ⊢ ( 𝑊 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ ( 𝑊 ∈ V ∧ ( ♯ ‘ 𝑊 ) ∈ { 0 , 1 } ) )
68 63 67 sylib ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ( 𝑊 ∈ V ∧ ( ♯ ‘ 𝑊 ) ∈ { 0 , 1 } ) )
69 68 simprd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ( ♯ ‘ 𝑊 ) ∈ { 0 , 1 } )
70 elpri ⊢ ( ( ♯ ‘ 𝑊 ) ∈ { 0 , 1 } → ( ( ♯ ‘ 𝑊 ) = 0 ∨ ( ♯ ‘ 𝑊 ) = 1 ) )
71 69 70 syl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ( ( ♯ ‘ 𝑊 ) = 0 ∨ ( ♯ ‘ 𝑊 ) = 1 ) )
72 41 62 71 mpjaodan ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑊 ∈ ( dom 𝐶 ∩ ( ◡ ♯ “ { 0 , 1 } ) ) ) → ( 𝐶 ‘ 𝑊 ) = ( I ↾ 𝐷 ) )