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 ) " ( `' # " { 3 } ) )
cyc3evpm.a 
|- A = ( pmEven ` D )
Assertion cyc3evpm 
|- ( D e. Fin -> C C_ A )

Proof

Step Hyp Ref Expression
1 cyc3evpm.t 
 |-  C = ( ( toCyc ` D ) " ( `' # " { 3 } ) )
2 cyc3evpm.a 
 |-  A = ( pmEven ` D )
3 simpr 
 |-  ( ( ( ( D e. Fin /\ p e. C ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( ( toCyc ` D ) ` u ) = p ) -> ( ( toCyc ` D ) ` u ) = p )
4 simpl 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> D e. Fin )
5 eqid 
 |-  ( toCyc ` D ) = ( toCyc ` D )
6 simpr 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) )
7 6 elin1d 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> u e. { w e. Word D | w : dom w -1-1-> D } )
8 elrabi 
 |-  ( u e. { w e. Word D | w : dom w -1-1-> D } -> u e. Word D )
9 7 8 syl 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> u e. Word D )
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-1-> D <-> u : dom u -1-1-> D ) )
14 13 elrab 
 |-  ( u e. { w e. Word D | w : dom w -1-1-> D } <-> ( u e. Word D /\ u : dom u -1-1-> D ) )
15 14 simprbi 
 |-  ( u e. { w e. Word D | w : dom w -1-1-> D } -> u : dom u -1-1-> D )
16 7 15 syl 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> u : dom u -1-1-> D )
17 eqid 
 |-  ( SymGrp ` D ) = ( SymGrp ` D )
18 5 4 9 16 17 cycpmcl 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( toCyc ` D ) ` u ) e. ( Base ` ( SymGrp ` D ) ) )
19 c0ex 
 |-  0 e. _V
20 19 tpid1 
 |-  0 e. { 0 , 1 , 2 }
21 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
22 20 21 eleqtrri 
 |-  0 e. ( 0 ..^ 3 )
23 6 elin2d 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> u e. ( `' # " { 3 } ) )
24 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
25 ffn 
 |-  ( # : _V --> ( NN0 u. { +oo } ) -> # Fn _V )
26 elpreima 
 |-  ( # Fn _V -> ( u e. ( `' # " { 3 } ) <-> ( u e. _V /\ ( # ` u ) e. { 3 } ) ) )
27 24 25 26 mp2b 
 |-  ( u e. ( `' # " { 3 } ) <-> ( u e. _V /\ ( # ` u ) e. { 3 } ) )
28 27 simprbi 
 |-  ( u e. ( `' # " { 3 } ) -> ( # ` u ) e. { 3 } )
29 elsni 
 |-  ( ( # ` u ) e. { 3 } -> ( # ` u ) = 3 )
30 23 28 29 3syl 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( # ` u ) = 3 )
31 30 oveq2d 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( 0 ..^ ( # ` u ) ) = ( 0 ..^ 3 ) )
32 22 31 eleqtrrid 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> 0 e. ( 0 ..^ ( # ` u ) ) )
33 wrdsymbcl 
 |-  ( ( u e. Word D /\ 0 e. ( 0 ..^ ( # ` u ) ) ) -> ( u ` 0 ) e. D )
34 9 32 33 syl2anc 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( u ` 0 ) e. D )
35 1ex 
 |-  1 e. _V
36 35 tpid2 
 |-  1 e. { 0 , 1 , 2 }
37 36 21 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
38 37 31 eleqtrrid 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> 1 e. ( 0 ..^ ( # ` u ) ) )
39 wrdsymbcl 
 |-  ( ( u e. Word D /\ 1 e. ( 0 ..^ ( # ` u ) ) ) -> ( u ` 1 ) e. D )
40 9 38 39 syl2anc 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( u ` 1 ) e. D )
41 2ex 
 |-  2 e. _V
42 41 tpid3 
 |-  2 e. { 0 , 1 , 2 }
43 42 21 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
44 43 31 eleqtrrid 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> 2 e. ( 0 ..^ ( # ` u ) ) )
45 wrdsymbcl 
 |-  ( ( u e. Word D /\ 2 e. ( 0 ..^ ( # ` u ) ) ) -> ( u ` 2 ) e. D )
46 9 44 45 syl2anc 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( u ` 2 ) e. D )
47 34 40 46 3jca 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( u ` 0 ) e. D /\ ( u ` 1 ) e. D /\ ( u ` 2 ) e. D ) )
48 eqidd 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( u ` 0 ) = ( u ` 0 ) )
49 eqidd 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( u ` 1 ) = ( u ` 1 ) )
50 eqidd 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( u ` 2 ) = ( u ` 2 ) )
51 48 49 50 3jca 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( u ` 0 ) = ( u ` 0 ) /\ ( u ` 1 ) = ( u ` 1 ) /\ ( u ` 2 ) = ( u ` 2 ) ) )
52 eqwrds3 
 |-  ( ( u e. Word D /\ ( ( u ` 0 ) e. D /\ ( u ` 1 ) e. D /\ ( u ` 2 ) e. D ) ) -> ( u = <" ( u ` 0 ) ( u ` 1 ) ( u ` 2 ) "> <-> ( ( # ` u ) = 3 /\ ( ( u ` 0 ) = ( u ` 0 ) /\ ( u ` 1 ) = ( u ` 1 ) /\ ( u ` 2 ) = ( u ` 2 ) ) ) ) )
53 52 biimpar 
 |-  ( ( ( u e. Word D /\ ( ( u ` 0 ) e. D /\ ( u ` 1 ) e. D /\ ( u ` 2 ) e. D ) ) /\ ( ( # ` u ) = 3 /\ ( ( u ` 0 ) = ( u ` 0 ) /\ ( u ` 1 ) = ( u ` 1 ) /\ ( u ` 2 ) = ( u ` 2 ) ) ) ) -> u = <" ( u ` 0 ) ( u ` 1 ) ( u ` 2 ) "> )
54 9 47 30 51 53 syl22anc 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> u = <" ( u ` 0 ) ( u ` 1 ) ( u ` 2 ) "> )
55 54 fveq2d 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( toCyc ` D ) ` u ) = ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) ( u ` 2 ) "> ) )
56 wrddm 
 |-  ( u e. Word D -> dom u = ( 0 ..^ ( # ` u ) ) )
57 9 56 syl 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> dom u = ( 0 ..^ ( # ` u ) ) )
58 57 31 eqtrd 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> dom u = ( 0 ..^ 3 ) )
59 58 21 eqtrdi 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> dom u = { 0 , 1 , 2 } )
60 f1eq2 
 |-  ( dom u = { 0 , 1 , 2 } -> ( u : dom u -1-1-> D <-> u : { 0 , 1 , 2 } -1-1-> D ) )
61 60 biimpa 
 |-  ( ( dom u = { 0 , 1 , 2 } /\ u : dom u -1-1-> D ) -> u : { 0 , 1 , 2 } -1-1-> D )
62 59 16 61 syl2anc 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> u : { 0 , 1 , 2 } -1-1-> D )
63 19 35 41 3pm3.2i 
 |-  ( 0 e. _V /\ 1 e. _V /\ 2 e. _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 
 |-  { 0 , 1 , 2 } = { 0 , 1 , 2 }
69 68 f13dfv 
 |-  ( ( ( 0 e. _V /\ 1 e. _V /\ 2 e. _V ) /\ ( 0 =/= 1 /\ 0 =/= 2 /\ 1 =/= 2 ) ) -> ( u : { 0 , 1 , 2 } -1-1-> D <-> ( u : { 0 , 1 , 2 } --> D /\ ( ( u ` 0 ) =/= ( u ` 1 ) /\ ( u ` 0 ) =/= ( u ` 2 ) /\ ( u ` 1 ) =/= ( u ` 2 ) ) ) ) )
70 63 67 69 mp2an 
 |-  ( u : { 0 , 1 , 2 } -1-1-> D <-> ( u : { 0 , 1 , 2 } --> D /\ ( ( u ` 0 ) =/= ( u ` 1 ) /\ ( u ` 0 ) =/= ( u ` 2 ) /\ ( u ` 1 ) =/= ( u ` 2 ) ) ) )
71 70 simprbi 
 |-  ( u : { 0 , 1 , 2 } -1-1-> D -> ( ( u ` 0 ) =/= ( u ` 1 ) /\ ( u ` 0 ) =/= ( u ` 2 ) /\ ( u ` 1 ) =/= ( u ` 2 ) ) )
72 62 71 syl 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( u ` 0 ) =/= ( u ` 1 ) /\ ( u ` 0 ) =/= ( u ` 2 ) /\ ( u ` 1 ) =/= ( u ` 2 ) ) )
73 72 simp1d 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( u ` 0 ) =/= ( u ` 1 ) )
74 72 simp3d 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( u ` 1 ) =/= ( u ` 2 ) )
75 72 simp2d 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( u ` 0 ) =/= ( u ` 2 ) )
76 75 necomd 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( u ` 2 ) =/= ( u ` 0 ) )
77 eqid 
 |-  ( +g ` ( SymGrp ` D ) ) = ( +g ` ( SymGrp ` D ) )
78 5 17 4 34 40 46 73 74 76 77 cyc3co2 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) ( u ` 2 ) "> ) = ( ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) ( +g ` ( SymGrp ` D ) ) ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) )
79 5 4 34 46 75 17 cycpm2cl 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) e. ( Base ` ( SymGrp ` D ) ) )
80 5 4 34 40 73 17 cycpm2cl 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) e. ( Base ` ( SymGrp ` D ) ) )
81 eqid 
 |-  ( Base ` ( SymGrp ` D ) ) = ( Base ` ( SymGrp ` D ) )
82 17 81 77 symgov 
 |-  ( ( ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) e. ( Base ` ( SymGrp ` D ) ) /\ ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) e. ( Base ` ( SymGrp ` D ) ) ) -> ( ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) ( +g ` ( SymGrp ` D ) ) ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) = ( ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) o. ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) )
83 79 80 82 syl2anc 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) ( +g ` ( SymGrp ` D ) ) ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) = ( ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) o. ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) )
84 55 78 83 3eqtrd 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( toCyc ` D ) ` u ) = ( ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) o. ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) )
85 84 fveq2d 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` u ) ) = ( ( pmSgn ` D ) ` ( ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) o. ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) ) )
86 eqid 
 |-  ( pmSgn ` D ) = ( pmSgn ` D )
87 17 86 81 psgnco 
 |-  ( ( D e. Fin /\ ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) e. ( Base ` ( SymGrp ` D ) ) /\ ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) e. ( Base ` ( SymGrp ` D ) ) ) -> ( ( pmSgn ` D ) ` ( ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) o. ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) ) = ( ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) ) x. ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) ) )
88 4 79 80 87 syl3anc 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( pmSgn ` D ) ` ( ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) o. ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) ) = ( ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) ) x. ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) ) )
89 eqid 
 |-  ( pmTrsp ` D ) = ( pmTrsp ` D )
90 5 4 34 46 75 89 cycpm2tr 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) = ( ( pmTrsp ` D ) ` { ( u ` 0 ) , ( u ` 2 ) } ) )
91 34 46 prssd 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> { ( u ` 0 ) , ( u ` 2 ) } C_ D )
92 pr2nelem 
 |-  ( ( ( u ` 0 ) e. D /\ ( u ` 2 ) e. D /\ ( u ` 0 ) =/= ( u ` 2 ) ) -> { ( u ` 0 ) , ( u ` 2 ) } ~~ 2o )
93 34 46 75 92 syl3anc 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> { ( u ` 0 ) , ( u ` 2 ) } ~~ 2o )
94 eqid 
 |-  ran ( pmTrsp ` D ) = ran ( pmTrsp ` D )
95 89 94 pmtrrn 
 |-  ( ( D e. Fin /\ { ( u ` 0 ) , ( u ` 2 ) } C_ D /\ { ( u ` 0 ) , ( u ` 2 ) } ~~ 2o ) -> ( ( pmTrsp ` D ) ` { ( u ` 0 ) , ( u ` 2 ) } ) e. ran ( pmTrsp ` D ) )
96 4 91 93 95 syl3anc 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( pmTrsp ` D ) ` { ( u ` 0 ) , ( u ` 2 ) } ) e. ran ( pmTrsp ` D ) )
97 90 96 eqeltrd 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) e. ran ( pmTrsp ` D ) )
98 17 94 86 psgnpmtr 
 |-  ( ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) e. ran ( pmTrsp ` D ) -> ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) ) = -u 1 )
99 97 98 syl 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) ) = -u 1 )
100 5 4 34 40 73 89 cycpm2tr 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) = ( ( pmTrsp ` D ) ` { ( u ` 0 ) , ( u ` 1 ) } ) )
101 34 40 prssd 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> { ( u ` 0 ) , ( u ` 1 ) } C_ D )
102 pr2nelem 
 |-  ( ( ( u ` 0 ) e. D /\ ( u ` 1 ) e. D /\ ( u ` 0 ) =/= ( u ` 1 ) ) -> { ( u ` 0 ) , ( u ` 1 ) } ~~ 2o )
103 34 40 73 102 syl3anc 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> { ( u ` 0 ) , ( u ` 1 ) } ~~ 2o )
104 89 94 pmtrrn 
 |-  ( ( D e. Fin /\ { ( u ` 0 ) , ( u ` 1 ) } C_ D /\ { ( u ` 0 ) , ( u ` 1 ) } ~~ 2o ) -> ( ( pmTrsp ` D ) ` { ( u ` 0 ) , ( u ` 1 ) } ) e. ran ( pmTrsp ` D ) )
105 4 101 103 104 syl3anc 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( pmTrsp ` D ) ` { ( u ` 0 ) , ( u ` 1 ) } ) e. ran ( pmTrsp ` D ) )
106 100 105 eqeltrd 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) e. ran ( pmTrsp ` D ) )
107 17 94 86 psgnpmtr 
 |-  ( ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) e. ran ( pmTrsp ` D ) -> ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) = -u 1 )
108 106 107 syl 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) = -u 1 )
109 99 108 oveq12d 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) ) x. ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) ) = ( -u 1 x. -u 1 ) )
110 neg1mulneg1e1 
 |-  ( -u 1 x. -u 1 ) = 1
111 109 110 eqtrdi 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 2 ) "> ) ) x. ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` <" ( u ` 0 ) ( u ` 1 ) "> ) ) ) = 1 )
112 85 88 111 3eqtrd 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` u ) ) = 1 )
113 17 81 86 psgnevpmb 
 |-  ( D e. Fin -> ( ( ( toCyc ` D ) ` u ) e. ( pmEven ` D ) <-> ( ( ( toCyc ` D ) ` u ) e. ( Base ` ( SymGrp ` D ) ) /\ ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` u ) ) = 1 ) ) )
114 113 biimpar 
 |-  ( ( D e. Fin /\ ( ( ( toCyc ` D ) ` u ) e. ( Base ` ( SymGrp ` D ) ) /\ ( ( pmSgn ` D ) ` ( ( toCyc ` D ) ` u ) ) = 1 ) ) -> ( ( toCyc ` D ) ` u ) e. ( pmEven ` D ) )
115 4 18 112 114 syl12anc 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( toCyc ` D ) ` u ) e. ( pmEven ` D ) )
116 115 2 eleqtrrdi 
 |-  ( ( D e. Fin /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) -> ( ( toCyc ` D ) ` u ) e. A )
117 116 ad4ant13 
 |-  ( ( ( ( D e. Fin /\ p e. C ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( ( toCyc ` D ) ` u ) = p ) -> ( ( toCyc ` D ) ` u ) e. A )
118 3 117 eqeltrrd 
 |-  ( ( ( ( D e. Fin /\ p e. C ) /\ u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ) /\ ( ( toCyc ` D ) ` u ) = p ) -> p e. A )
119 nfcv 
 |-  F/_ u ( toCyc ` D )
120 5 17 81 tocycf 
 |-  ( D e. Fin -> ( toCyc ` D ) : { w e. Word D | w : dom w -1-1-> D } --> ( Base ` ( SymGrp ` D ) ) )
121 120 ffnd 
 |-  ( D e. Fin -> ( toCyc ` D ) Fn { w e. Word D | w : dom w -1-1-> D } )
122 121 adantr 
 |-  ( ( D e. Fin /\ p e. C ) -> ( toCyc ` D ) Fn { w e. Word D | w : dom w -1-1-> D } )
123 simpr 
 |-  ( ( D e. Fin /\ p e. C ) -> p e. C )
124 123 1 eleqtrdi 
 |-  ( ( D e. Fin /\ p e. C ) -> p e. ( ( toCyc ` D ) " ( `' # " { 3 } ) ) )
125 119 122 124 fvelimad 
 |-  ( ( D e. Fin /\ p e. C ) -> E. u e. ( { w e. Word D | w : dom w -1-1-> D } i^i ( `' # " { 3 } ) ) ( ( toCyc ` D ) ` u ) = p )
126 118 125 r19.29a 
 |-  ( ( D e. Fin /\ p e. C ) -> p e. A )
127 126 ex 
 |-  ( D e. Fin -> ( p e. C -> p e. A ) )
128 127 ssrdv 
 |-  ( D e. Fin -> C C_ A )