Metamath Proof Explorer

Theorem cyc3evpm

Description: 3-Cycles are even permutations. (Contributed by Thierry Arnoux, 24-Sep-2023)

Ref Expression
Hypotheses cyc3evpm.t ⊢C=toCyc⁡D.-13
cyc3evpm.a ⊢A=pmEven⁡D
Assertion cyc3evpm ⊢D∈Fin→C⊆A

Proof

Step Hyp Ref Expression
1 cyc3evpm.t ⊢C=toCyc⁡D.-13
2 cyc3evpm.a ⊢A=pmEven⁡D
3 simpr ⊢D∈Fin∧p∈C∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13∧toCyc⁡D⁡u=p→toCyc⁡D⁡u=p
4 simpl ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→D∈Fin
5 eqid ⊢toCyc⁡D=toCyc⁡D
6 simpr ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13
7 6 elin1d ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u∈w∈WordD|w:dom⁡w⟶1-1D
8 elrabi ⊢u∈w∈WordD|w:dom⁡w⟶1-1D→u∈WordD
9 7 8 syl ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u∈WordD
10 id ⊢w=u→w=u
11 dmeq ⊢w=u→dom⁡w=dom⁡u
12 eqidd ⊢w=u→D=D
13 10 11 12 f1eq123d ⊢w=u→w:dom⁡w⟶1-1D↔u:dom⁡u⟶1-1D
14 13 elrab ⊢u∈w∈WordD|w:dom⁡w⟶1-1D↔u∈WordD∧u:dom⁡u⟶1-1D
15 14 simprbi ⊢u∈w∈WordD|w:dom⁡w⟶1-1D→u:dom⁡u⟶1-1D
16 7 15 syl ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u:dom⁡u⟶1-1D
17 eqid ⊢SymGrp⁡D=SymGrp⁡D
18 5 4 9 16 17 cycpmcl ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→toCyc⁡D⁡u∈BaseSymGrp⁡D
19 c0ex ⊢0∈V
20 19 tpid1 ⊢0∈012
21 fzo0to3tp ⊢0..^3=012
22 20 21 eleqtrri ⊢0∈0..^3
23 6 elin2d ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u∈.-13
24 hashf ⊢.:V⟶ℕ0∪+∞
25 ffn ⊢.:V⟶ℕ0∪+∞→.FnV
26 elpreima ⊢.FnV→u∈.-13↔u∈V∧u∈3
27 24 25 26 mp2b ⊢u∈.-13↔u∈V∧u∈3
28 27 simprbi ⊢u∈.-13→u∈3
29 elsni ⊢u∈3→u=3
30 23 28 29 3syl ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u=3
31 30 oveq2d ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→0..^u=0..^3
32 22 31 eleqtrrid ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→0∈0..^u
33 wrdsymbcl ⊢u∈WordD∧0∈0..^u→u⁡0∈D
34 9 32 33 syl2anc ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡0∈D
35 1ex ⊢1∈V
36 35 tpid2 ⊢1∈012
37 36 21 eleqtrri ⊢1∈0..^3
38 37 31 eleqtrrid ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→1∈0..^u
39 wrdsymbcl ⊢u∈WordD∧1∈0..^u→u⁡1∈D
40 9 38 39 syl2anc ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡1∈D
41 2ex ⊢2∈V
42 41 tpid3 ⊢2∈012
43 42 21 eleqtrri ⊢2∈0..^3
44 43 31 eleqtrrid ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→2∈0..^u
45 wrdsymbcl ⊢u∈WordD∧2∈0..^u→u⁡2∈D
46 9 44 45 syl2anc ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡2∈D
47 34 40 46 3jca ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡0∈D∧u⁡1∈D∧u⁡2∈D
48 eqidd ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡0=u⁡0
49 eqidd ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡1=u⁡1
50 eqidd ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡2=u⁡2
51 48 49 50 3jca ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡0=u⁡0∧u⁡1=u⁡1∧u⁡2=u⁡2
52 eqwrds3 ⊢u∈WordD∧u⁡0∈D∧u⁡1∈D∧u⁡2∈D→u=⟨“u⁡0u⁡1u⁡2”⟩↔u=3∧u⁡0=u⁡0∧u⁡1=u⁡1∧u⁡2=u⁡2
53 52 biimpar ⊢u∈WordD∧u⁡0∈D∧u⁡1∈D∧u⁡2∈D∧u=3∧u⁡0=u⁡0∧u⁡1=u⁡1∧u⁡2=u⁡2→u=⟨“u⁡0u⁡1u⁡2”⟩
54 9 47 30 51 53 syl22anc ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u=⟨“u⁡0u⁡1u⁡2”⟩
55 54 fveq2d ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→toCyc⁡D⁡u=toCyc⁡D⁡⟨“u⁡0u⁡1u⁡2”⟩
56 wrddm ⊢u∈WordD→dom⁡u=0..^u
57 9 56 syl ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→dom⁡u=0..^u
58 57 31 eqtrd ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→dom⁡u=0..^3
59 58 21 eqtrdi ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→dom⁡u=012
60 f1eq2 ⊢dom⁡u=012→u:dom⁡u⟶1-1D↔u:012⟶1-1D
61 60 biimpa ⊢dom⁡u=012∧u:dom⁡u⟶1-1D→u:012⟶1-1D
62 59 16 61 syl2anc ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u:012⟶1-1D
63 19 35 41 3pm3.2i ⊢0∈V∧1∈V∧2∈V
64 0ne1 ⊢0≠1
65 0ne2 ⊢0≠2
66 1ne2 ⊢1≠2
67 64 65 66 3pm3.2i ⊢0≠1∧0≠2∧1≠2
68 eqid ⊢012=012
69 68 f13dfv ⊢0∈V∧1∈V∧2∈V∧0≠1∧0≠2∧1≠2→u:012⟶1-1D↔u:012⟶D∧u⁡0≠u⁡1∧u⁡0≠u⁡2∧u⁡1≠u⁡2
70 63 67 69 mp2an ⊢u:012⟶1-1D↔u:012⟶D∧u⁡0≠u⁡1∧u⁡0≠u⁡2∧u⁡1≠u⁡2
71 70 simprbi ⊢u:012⟶1-1D→u⁡0≠u⁡1∧u⁡0≠u⁡2∧u⁡1≠u⁡2
72 62 71 syl ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡0≠u⁡1∧u⁡0≠u⁡2∧u⁡1≠u⁡2
73 72 simp1d ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡0≠u⁡1
74 72 simp3d ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡1≠u⁡2
75 72 simp2d ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡0≠u⁡2
76 75 necomd ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡2≠u⁡0
77 eqid ⊢+SymGrp⁡D=+SymGrp⁡D
78 5 17 4 34 40 46 73 74 76 77 cyc3co2 ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→toCyc⁡D⁡⟨“u⁡0u⁡1u⁡2”⟩=toCyc⁡D⁡⟨“u⁡0u⁡2”⟩+SymGrp⁡DtoCyc⁡D⁡⟨“u⁡0u⁡1”⟩
79 5 4 34 46 75 17 cycpm2cl ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→toCyc⁡D⁡⟨“u⁡0u⁡2”⟩∈BaseSymGrp⁡D
80 5 4 34 40 73 17 cycpm2cl ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→toCyc⁡D⁡⟨“u⁡0u⁡1”⟩∈BaseSymGrp⁡D
81 eqid ⊢BaseSymGrp⁡D=BaseSymGrp⁡D
82 17 81 77 symgov ⊢toCyc⁡D⁡⟨“u⁡0u⁡2”⟩∈BaseSymGrp⁡D∧toCyc⁡D⁡⟨“u⁡0u⁡1”⟩∈BaseSymGrp⁡D→toCyc⁡D⁡⟨“u⁡0u⁡2”⟩+SymGrp⁡DtoCyc⁡D⁡⟨“u⁡0u⁡1”⟩=toCyc⁡D⁡⟨“u⁡0u⁡2”⟩∘toCyc⁡D⁡⟨“u⁡0u⁡1”⟩
83 79 80 82 syl2anc ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→toCyc⁡D⁡⟨“u⁡0u⁡2”⟩+SymGrp⁡DtoCyc⁡D⁡⟨“u⁡0u⁡1”⟩=toCyc⁡D⁡⟨“u⁡0u⁡2”⟩∘toCyc⁡D⁡⟨“u⁡0u⁡1”⟩
84 55 78 83 3eqtrd ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→toCyc⁡D⁡u=toCyc⁡D⁡⟨“u⁡0u⁡2”⟩∘toCyc⁡D⁡⟨“u⁡0u⁡1”⟩
85 84 fveq2d ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→pmSgn⁡D⁡toCyc⁡D⁡u=pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡2”⟩∘toCyc⁡D⁡⟨“u⁡0u⁡1”⟩
86 eqid ⊢pmSgn⁡D=pmSgn⁡D
87 17 86 81 psgnco ⊢D∈Fin∧toCyc⁡D⁡⟨“u⁡0u⁡2”⟩∈BaseSymGrp⁡D∧toCyc⁡D⁡⟨“u⁡0u⁡1”⟩∈BaseSymGrp⁡D→pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡2”⟩∘toCyc⁡D⁡⟨“u⁡0u⁡1”⟩=pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡2”⟩⁢pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡1”⟩
88 4 79 80 87 syl3anc ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡2”⟩∘toCyc⁡D⁡⟨“u⁡0u⁡1”⟩=pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡2”⟩⁢pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡1”⟩
89 eqid ⊢pmTrsp⁡D=pmTrsp⁡D
90 5 4 34 46 75 89 cycpm2tr ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→toCyc⁡D⁡⟨“u⁡0u⁡2”⟩=pmTrsp⁡D⁡u⁡0u⁡2
91 34 46 prssd ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡0u⁡2⊆D
92 pr2nelem ⊢u⁡0∈D∧u⁡2∈D∧u⁡0≠u⁡2→u⁡0u⁡2≈2𝑜
93 34 46 75 92 syl3anc ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡0u⁡2≈2𝑜
94 eqid ⊢ran⁡pmTrsp⁡D=ran⁡pmTrsp⁡D
95 89 94 pmtrrn ⊢D∈Fin∧u⁡0u⁡2⊆D∧u⁡0u⁡2≈2𝑜→pmTrsp⁡D⁡u⁡0u⁡2∈ran⁡pmTrsp⁡D
96 4 91 93 95 syl3anc ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→pmTrsp⁡D⁡u⁡0u⁡2∈ran⁡pmTrsp⁡D
97 90 96 eqeltrd ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→toCyc⁡D⁡⟨“u⁡0u⁡2”⟩∈ran⁡pmTrsp⁡D
98 17 94 86 psgnpmtr ⊢toCyc⁡D⁡⟨“u⁡0u⁡2”⟩∈ran⁡pmTrsp⁡D→pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡2”⟩=−1
99 97 98 syl ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡2”⟩=−1
100 5 4 34 40 73 89 cycpm2tr ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→toCyc⁡D⁡⟨“u⁡0u⁡1”⟩=pmTrsp⁡D⁡u⁡0u⁡1
101 34 40 prssd ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡0u⁡1⊆D
102 pr2nelem ⊢u⁡0∈D∧u⁡1∈D∧u⁡0≠u⁡1→u⁡0u⁡1≈2𝑜
103 34 40 73 102 syl3anc ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→u⁡0u⁡1≈2𝑜
104 89 94 pmtrrn ⊢D∈Fin∧u⁡0u⁡1⊆D∧u⁡0u⁡1≈2𝑜→pmTrsp⁡D⁡u⁡0u⁡1∈ran⁡pmTrsp⁡D
105 4 101 103 104 syl3anc ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→pmTrsp⁡D⁡u⁡0u⁡1∈ran⁡pmTrsp⁡D
106 100 105 eqeltrd ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→toCyc⁡D⁡⟨“u⁡0u⁡1”⟩∈ran⁡pmTrsp⁡D
107 17 94 86 psgnpmtr ⊢toCyc⁡D⁡⟨“u⁡0u⁡1”⟩∈ran⁡pmTrsp⁡D→pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡1”⟩=−1
108 106 107 syl ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡1”⟩=−1
109 99 108 oveq12d ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡2”⟩⁢pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡1”⟩=-1⁢-1
110 neg1mulneg1e1 ⊢-1⁢-1=1
111 109 110 eqtrdi ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡2”⟩⁢pmSgn⁡D⁡toCyc⁡D⁡⟨“u⁡0u⁡1”⟩=1
112 85 88 111 3eqtrd ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→pmSgn⁡D⁡toCyc⁡D⁡u=1
113 17 81 86 psgnevpmb ⊢D∈Fin→toCyc⁡D⁡u∈pmEven⁡D↔toCyc⁡D⁡u∈BaseSymGrp⁡D∧pmSgn⁡D⁡toCyc⁡D⁡u=1
114 113 biimpar ⊢D∈Fin∧toCyc⁡D⁡u∈BaseSymGrp⁡D∧pmSgn⁡D⁡toCyc⁡D⁡u=1→toCyc⁡D⁡u∈pmEven⁡D
115 4 18 112 114 syl12anc ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→toCyc⁡D⁡u∈pmEven⁡D
116 115 2 eleqtrrdi ⊢D∈Fin∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13→toCyc⁡D⁡u∈A
117 116 ad4ant13 ⊢D∈Fin∧p∈C∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13∧toCyc⁡D⁡u=p→toCyc⁡D⁡u∈A
118 3 117 eqeltrrd ⊢D∈Fin∧p∈C∧u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13∧toCyc⁡D⁡u=p→p∈A
119 nfcv ⊢Ⅎ_utoCyc⁡D
120 5 17 81 tocycf ⊢D∈Fin→toCyc⁡D:w∈WordD|w:dom⁡w⟶1-1D⟶BaseSymGrp⁡D
121 120 ffnd ⊢D∈Fin→toCyc⁡DFnw∈WordD|w:dom⁡w⟶1-1D
122 121 adantr ⊢D∈Fin∧p∈C→toCyc⁡DFnw∈WordD|w:dom⁡w⟶1-1D
123 simpr ⊢D∈Fin∧p∈C→p∈C
124 123 1 eleqtrdi ⊢D∈Fin∧p∈C→p∈toCyc⁡D.-13
125 119 122 124 fvelimad ⊢D∈Fin∧p∈C→∃u∈w∈WordD|w:dom⁡w⟶1-1D∩.-13toCyc⁡D⁡u=p
126 118 125 r19.29a ⊢D∈Fin∧p∈C→p∈A
127 126 ex ⊢D∈Fin→p∈C→p∈A
128 127 ssrdv ⊢D∈Fin→C⊆A