Metamath Proof Explorer

Theorem cyc3genpm

Description: The alternating group A is generated by 3-cycles. Property (a) of Lang p. 32 . (Contributed by Thierry Arnoux, 27-Sep-2023)

Ref Expression
Hypotheses cyc3genpm.t 
|- C = ( M " ( `' # " { 3 } ) )
cyc3genpm.a 
|- A = ( pmEven ` D )
cyc3genpm.s 
|- S = ( SymGrp ` D )
cyc3genpm.n 
|- N = ( # ` D )
cyc3genpm.m 
|- M = ( toCyc ` D )
Assertion cyc3genpm 
|- ( D e. Fin -> ( Q e. A <-> E. w e. Word C Q = ( S gsum w ) ) )

Proof

Step Hyp Ref Expression
1 cyc3genpm.t 
 |-  C = ( M " ( `' # " { 3 } ) )
2 cyc3genpm.a 
 |-  A = ( pmEven ` D )
3 cyc3genpm.s 
 |-  S = ( SymGrp ` D )
4 cyc3genpm.n 
 |-  N = ( # ` D )
5 cyc3genpm.m 
 |-  M = ( toCyc ` D )
6 simplr 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> v e. Word ran ( pmTrsp ` D ) )
7 lencl 
 |-  ( v e. Word ran ( pmTrsp ` D ) -> ( # ` v ) e. NN0 )
8 7 ad2antlr 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> ( # ` v ) e. NN0 )
9 8 nn0zd 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> ( # ` v ) e. ZZ )
10 simpr 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> Q = ( S gsum v ) )
11 10 fveq2d 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> ( ( pmSgn ` D ) ` Q ) = ( ( pmSgn ` D ) ` ( S gsum v ) ) )
12 simplll 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> D e. Fin )
13 simpllr 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> Q e. A )
14 13 2 eleqtrdi 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> Q e. ( pmEven ` D ) )
15 eqid 
 |-  ( Base ` S ) = ( Base ` S )
16 eqid 
 |-  ( pmSgn ` D ) = ( pmSgn ` D )
17 3 15 16 psgnevpm 
 |-  ( ( D e. Fin /\ Q e. ( pmEven ` D ) ) -> ( ( pmSgn ` D ) ` Q ) = 1 )
18 12 14 17 syl2anc 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> ( ( pmSgn ` D ) ` Q ) = 1 )
19 eqid 
 |-  ran ( pmTrsp ` D ) = ran ( pmTrsp ` D )
20 3 19 16 psgnvalii 
 |-  ( ( D e. Fin /\ v e. Word ran ( pmTrsp ` D ) ) -> ( ( pmSgn ` D ) ` ( S gsum v ) ) = ( -u 1 ^ ( # ` v ) ) )
21 12 6 20 syl2anc 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> ( ( pmSgn ` D ) ` ( S gsum v ) ) = ( -u 1 ^ ( # ` v ) ) )
22 11 18 21 3eqtr3rd 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> ( -u 1 ^ ( # ` v ) ) = 1 )
23 m1exp1 
 |-  ( ( # ` v ) e. ZZ -> ( ( -u 1 ^ ( # ` v ) ) = 1 <-> 2 || ( # ` v ) ) )
24 23 biimpa 
 |-  ( ( ( # ` v ) e. ZZ /\ ( -u 1 ^ ( # ` v ) ) = 1 ) -> 2 || ( # ` v ) )
25 9 22 24 syl2anc 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> 2 || ( # ` v ) )
26 oveq2 
 |-  ( x = (/) -> ( S gsum x ) = ( S gsum (/) ) )
27 26 eqeq1d 
 |-  ( x = (/) -> ( ( S gsum x ) = ( S gsum w ) <-> ( S gsum (/) ) = ( S gsum w ) ) )
28 27 rexbidv 
 |-  ( x = (/) -> ( E. w e. Word C ( S gsum x ) = ( S gsum w ) <-> E. w e. Word C ( S gsum (/) ) = ( S gsum w ) ) )
29 28 imbi2d 
 |-  ( x = (/) -> ( ( D e. Fin -> E. w e. Word C ( S gsum x ) = ( S gsum w ) ) <-> ( D e. Fin -> E. w e. Word C ( S gsum (/) ) = ( S gsum w ) ) ) )
30 oveq2 
 |-  ( x = u -> ( S gsum x ) = ( S gsum u ) )
31 30 eqeq1d 
 |-  ( x = u -> ( ( S gsum x ) = ( S gsum w ) <-> ( S gsum u ) = ( S gsum w ) ) )
32 31 rexbidv 
 |-  ( x = u -> ( E. w e. Word C ( S gsum x ) = ( S gsum w ) <-> E. w e. Word C ( S gsum u ) = ( S gsum w ) ) )
33 32 imbi2d 
 |-  ( x = u -> ( ( D e. Fin -> E. w e. Word C ( S gsum x ) = ( S gsum w ) ) <-> ( D e. Fin -> E. w e. Word C ( S gsum u ) = ( S gsum w ) ) ) )
34 oveq2 
 |-  ( x = ( u ++ <" i j "> ) -> ( S gsum x ) = ( S gsum ( u ++ <" i j "> ) ) )
35 34 eqeq1d 
 |-  ( x = ( u ++ <" i j "> ) -> ( ( S gsum x ) = ( S gsum w ) <-> ( S gsum ( u ++ <" i j "> ) ) = ( S gsum w ) ) )
36 35 rexbidv 
 |-  ( x = ( u ++ <" i j "> ) -> ( E. w e. Word C ( S gsum x ) = ( S gsum w ) <-> E. w e. Word C ( S gsum ( u ++ <" i j "> ) ) = ( S gsum w ) ) )
37 36 imbi2d 
 |-  ( x = ( u ++ <" i j "> ) -> ( ( D e. Fin -> E. w e. Word C ( S gsum x ) = ( S gsum w ) ) <-> ( D e. Fin -> E. w e. Word C ( S gsum ( u ++ <" i j "> ) ) = ( S gsum w ) ) ) )
38 oveq2 
 |-  ( x = v -> ( S gsum x ) = ( S gsum v ) )
39 38 eqeq1d 
 |-  ( x = v -> ( ( S gsum x ) = ( S gsum w ) <-> ( S gsum v ) = ( S gsum w ) ) )
40 39 rexbidv 
 |-  ( x = v -> ( E. w e. Word C ( S gsum x ) = ( S gsum w ) <-> E. w e. Word C ( S gsum v ) = ( S gsum w ) ) )
41 40 imbi2d 
 |-  ( x = v -> ( ( D e. Fin -> E. w e. Word C ( S gsum x ) = ( S gsum w ) ) <-> ( D e. Fin -> E. w e. Word C ( S gsum v ) = ( S gsum w ) ) ) )
42 wrd0 
 |-  (/) e. Word C
43 42 a1i 
 |-  ( D e. Fin -> (/) e. Word C )
44 simpr 
 |-  ( ( D e. Fin /\ w = (/) ) -> w = (/) )
45 44 oveq2d 
 |-  ( ( D e. Fin /\ w = (/) ) -> ( S gsum w ) = ( S gsum (/) ) )
46 45 eqeq2d 
 |-  ( ( D e. Fin /\ w = (/) ) -> ( ( S gsum (/) ) = ( S gsum w ) <-> ( S gsum (/) ) = ( S gsum (/) ) ) )
47 eqidd 
 |-  ( D e. Fin -> ( S gsum (/) ) = ( S gsum (/) ) )
48 43 46 47 rspcedvd 
 |-  ( D e. Fin -> E. w e. Word C ( S gsum (/) ) = ( S gsum w ) )
49 ccatcl 
 |-  ( ( v e. Word C /\ c e. Word C ) -> ( v ++ c ) e. Word C )
50 49 ad5ant24 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> ( v ++ c ) e. Word C )
51 oveq2 
 |-  ( w = ( v ++ c ) -> ( S gsum w ) = ( S gsum ( v ++ c ) ) )
52 51 eqeq2d 
 |-  ( w = ( v ++ c ) -> ( ( S gsum ( u ++ <" i j "> ) ) = ( S gsum w ) <-> ( S gsum ( u ++ <" i j "> ) ) = ( S gsum ( v ++ c ) ) ) )
53 52 adantl 
 |-  ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) /\ w = ( v ++ c ) ) -> ( ( S gsum ( u ++ <" i j "> ) ) = ( S gsum w ) <-> ( S gsum ( u ++ <" i j "> ) ) = ( S gsum ( v ++ c ) ) ) )
54 simpllr 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> ( S gsum u ) = ( S gsum v ) )
55 simpllr 
 |-  ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) -> D e. Fin )
56 55 ad2antrr 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> D e. Fin )
57 3 symggrp 
 |-  ( D e. Fin -> S e. Grp )
58 grpmnd 
 |-  ( S e. Grp -> S e. Mnd )
59 56 57 58 3syl 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> S e. Mnd )
60 19 3 15 symgtrf 
 |-  ran ( pmTrsp ` D ) C_ ( Base ` S )
61 60 a1i 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> ran ( pmTrsp ` D ) C_ ( Base ` S ) )
62 simp-5r 
 |-  ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) -> i e. ran ( pmTrsp ` D ) )
63 62 ad2antrr 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> i e. ran ( pmTrsp ` D ) )
64 61 63 sseldd 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> i e. ( Base ` S ) )
65 simp-6r 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> j e. ran ( pmTrsp ` D ) )
66 61 65 sseldd 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> j e. ( Base ` S ) )
67 eqid 
 |-  ( +g ` S ) = ( +g ` S )
68 15 67 gsumws2 
 |-  ( ( S e. Mnd /\ i e. ( Base ` S ) /\ j e. ( Base ` S ) ) -> ( S gsum <" i j "> ) = ( i ( +g ` S ) j ) )
69 59 64 66 68 syl3anc 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> ( S gsum <" i j "> ) = ( i ( +g ` S ) j ) )
70 simpr 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> ( i ( +g ` S ) j ) = ( S gsum c ) )
71 69 70 eqtrd 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> ( S gsum <" i j "> ) = ( S gsum c ) )
72 54 71 oveq12d 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> ( ( S gsum u ) ( +g ` S ) ( S gsum <" i j "> ) ) = ( ( S gsum v ) ( +g ` S ) ( S gsum c ) ) )
73 sswrd 
 |-  ( ran ( pmTrsp ` D ) C_ ( Base ` S ) -> Word ran ( pmTrsp ` D ) C_ Word ( Base ` S ) )
74 61 73 syl 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> Word ran ( pmTrsp ` D ) C_ Word ( Base ` S ) )
75 simp-7l 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> u e. Word ran ( pmTrsp ` D ) )
76 74 75 sseldd 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> u e. Word ( Base ` S ) )
77 64 66 s2cld 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> <" i j "> e. Word ( Base ` S ) )
78 15 67 gsumccat 
 |-  ( ( S e. Mnd /\ u e. Word ( Base ` S ) /\ <" i j "> e. Word ( Base ` S ) ) -> ( S gsum ( u ++ <" i j "> ) ) = ( ( S gsum u ) ( +g ` S ) ( S gsum <" i j "> ) ) )
79 59 76 77 78 syl3anc 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> ( S gsum ( u ++ <" i j "> ) ) = ( ( S gsum u ) ( +g ` S ) ( S gsum <" i j "> ) ) )
80 5 imaeq1i 
 |-  ( M " ( `' # " { 3 } ) ) = ( ( toCyc ` D ) " ( `' # " { 3 } ) )
81 1 80 eqtri 
 |-  C = ( ( toCyc ` D ) " ( `' # " { 3 } ) )
82 81 2 cyc3evpm 
 |-  ( D e. Fin -> C C_ A )
83 3 15 evpmss 
 |-  ( pmEven ` D ) C_ ( Base ` S )
84 2 83 eqsstri 
 |-  A C_ ( Base ` S )
85 82 84 sstrdi 
 |-  ( D e. Fin -> C C_ ( Base ` S ) )
86 sswrd 
 |-  ( C C_ ( Base ` S ) -> Word C C_ Word ( Base ` S ) )
87 56 85 86 3syl 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> Word C C_ Word ( Base ` S ) )
88 simp-4r 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> v e. Word C )
89 87 88 sseldd 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> v e. Word ( Base ` S ) )
90 simplr 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> c e. Word C )
91 87 90 sseldd 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> c e. Word ( Base ` S ) )
92 15 67 gsumccat 
 |-  ( ( S e. Mnd /\ v e. Word ( Base ` S ) /\ c e. Word ( Base ` S ) ) -> ( S gsum ( v ++ c ) ) = ( ( S gsum v ) ( +g ` S ) ( S gsum c ) ) )
93 59 89 91 92 syl3anc 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> ( S gsum ( v ++ c ) ) = ( ( S gsum v ) ( +g ` S ) ( S gsum c ) ) )
94 72 79 93 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> ( S gsum ( u ++ <" i j "> ) ) = ( S gsum ( v ++ c ) ) )
95 50 53 94 rspcedvd 
 |-  ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ c e. Word C ) /\ ( i ( +g ` S ) j ) = ( S gsum c ) ) -> E. w e. Word C ( S gsum ( u ++ <" i j "> ) ) = ( S gsum w ) )
96 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) /\ g e. D ) /\ h e. D ) /\ ( g =/= h /\ j = ( M ` <" g h "> ) ) ) -> e e. D )
97 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) /\ g e. D ) /\ h e. D ) /\ ( g =/= h /\ j = ( M ` <" g h "> ) ) ) -> f e. D )
98 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) /\ g e. D ) /\ h e. D ) /\ ( g =/= h /\ j = ( M ` <" g h "> ) ) ) -> g e. D )
99 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) /\ g e. D ) /\ h e. D ) /\ ( g =/= h /\ j = ( M ` <" g h "> ) ) ) -> h e. D )
100 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) /\ g e. D ) /\ h e. D ) /\ ( g =/= h /\ j = ( M ` <" g h "> ) ) ) -> ( e =/= f /\ i = ( M ` <" e f "> ) ) )
101 100 simprd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) /\ g e. D ) /\ h e. D ) /\ ( g =/= h /\ j = ( M ` <" g h "> ) ) ) -> i = ( M ` <" e f "> ) )
102 simprr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) /\ g e. D ) /\ h e. D ) /\ ( g =/= h /\ j = ( M ` <" g h "> ) ) ) -> j = ( M ` <" g h "> ) )
103 55 ad6antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) /\ g e. D ) /\ h e. D ) /\ ( g =/= h /\ j = ( M ` <" g h "> ) ) ) -> D e. Fin )
104 100 simpld 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) /\ g e. D ) /\ h e. D ) /\ ( g =/= h /\ j = ( M ` <" g h "> ) ) ) -> e =/= f )
105 simprl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) /\ g e. D ) /\ h e. D ) /\ ( g =/= h /\ j = ( M ` <" g h "> ) ) ) -> g =/= h )
106 1 2 3 4 5 67 96 97 98 99 101 102 103 104 105 cyc3genpmlem 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) /\ g e. D ) /\ h e. D ) /\ ( g =/= h /\ j = ( M ` <" g h "> ) ) ) -> E. c e. Word C ( i ( +g ` S ) j ) = ( S gsum c ) )
107 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) -> D e. Fin )
108 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) -> j e. ran ( pmTrsp ` D ) )
109 19 5 trsp2cyc 
 |-  ( ( D e. Fin /\ j e. ran ( pmTrsp ` D ) ) -> E. g e. D E. h e. D ( g =/= h /\ j = ( M ` <" g h "> ) ) )
110 107 108 109 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) -> E. g e. D E. h e. D ( g =/= h /\ j = ( M ` <" g h "> ) ) )
111 106 110 r19.29vva 
 |-  ( ( ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) /\ e e. D ) /\ f e. D ) /\ ( e =/= f /\ i = ( M ` <" e f "> ) ) ) -> E. c e. Word C ( i ( +g ` S ) j ) = ( S gsum c ) )
112 19 5 trsp2cyc 
 |-  ( ( D e. Fin /\ i e. ran ( pmTrsp ` D ) ) -> E. e e. D E. f e. D ( e =/= f /\ i = ( M ` <" e f "> ) ) )
113 55 62 112 syl2anc 
 |-  ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) -> E. e e. D E. f e. D ( e =/= f /\ i = ( M ` <" e f "> ) ) )
114 111 113 r19.29vva 
 |-  ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) -> E. c e. Word C ( i ( +g ` S ) j ) = ( S gsum c ) )
115 95 114 r19.29a 
 |-  ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) -> E. w e. Word C ( S gsum ( u ++ <" i j "> ) ) = ( S gsum w ) )
116 115 adantl3r 
 |-  ( ( ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ ( D e. Fin -> E. w e. Word C ( S gsum u ) = ( S gsum w ) ) ) /\ D e. Fin ) /\ v e. Word C ) /\ ( S gsum u ) = ( S gsum v ) ) -> E. w e. Word C ( S gsum ( u ++ <" i j "> ) ) = ( S gsum w ) )
117 simpr 
 |-  ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ ( D e. Fin -> E. w e. Word C ( S gsum u ) = ( S gsum w ) ) ) /\ D e. Fin ) -> D e. Fin )
118 simplr 
 |-  ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ ( D e. Fin -> E. w e. Word C ( S gsum u ) = ( S gsum w ) ) ) /\ D e. Fin ) -> ( D e. Fin -> E. w e. Word C ( S gsum u ) = ( S gsum w ) ) )
119 117 118 mpd 
 |-  ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ ( D e. Fin -> E. w e. Word C ( S gsum u ) = ( S gsum w ) ) ) /\ D e. Fin ) -> E. w e. Word C ( S gsum u ) = ( S gsum w ) )
120 oveq2 
 |-  ( v = w -> ( S gsum v ) = ( S gsum w ) )
121 120 eqeq2d 
 |-  ( v = w -> ( ( S gsum u ) = ( S gsum v ) <-> ( S gsum u ) = ( S gsum w ) ) )
122 121 cbvrexvw 
 |-  ( E. v e. Word C ( S gsum u ) = ( S gsum v ) <-> E. w e. Word C ( S gsum u ) = ( S gsum w ) )
123 119 122 sylibr 
 |-  ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ ( D e. Fin -> E. w e. Word C ( S gsum u ) = ( S gsum w ) ) ) /\ D e. Fin ) -> E. v e. Word C ( S gsum u ) = ( S gsum v ) )
124 116 123 r19.29a 
 |-  ( ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ ( D e. Fin -> E. w e. Word C ( S gsum u ) = ( S gsum w ) ) ) /\ D e. Fin ) -> E. w e. Word C ( S gsum ( u ++ <" i j "> ) ) = ( S gsum w ) )
125 124 ex 
 |-  ( ( ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) ) /\ j e. ran ( pmTrsp ` D ) ) /\ ( D e. Fin -> E. w e. Word C ( S gsum u ) = ( S gsum w ) ) ) -> ( D e. Fin -> E. w e. Word C ( S gsum ( u ++ <" i j "> ) ) = ( S gsum w ) ) )
126 125 ex3 
 |-  ( ( u e. Word ran ( pmTrsp ` D ) /\ i e. ran ( pmTrsp ` D ) /\ j e. ran ( pmTrsp ` D ) ) -> ( ( D e. Fin -> E. w e. Word C ( S gsum u ) = ( S gsum w ) ) -> ( D e. Fin -> E. w e. Word C ( S gsum ( u ++ <" i j "> ) ) = ( S gsum w ) ) ) )
127 29 33 37 41 48 126 wrdt2ind 
 |-  ( ( v e. Word ran ( pmTrsp ` D ) /\ 2 || ( # ` v ) ) -> ( D e. Fin -> E. w e. Word C ( S gsum v ) = ( S gsum w ) ) )
128 127 imp 
 |-  ( ( ( v e. Word ran ( pmTrsp ` D ) /\ 2 || ( # ` v ) ) /\ D e. Fin ) -> E. w e. Word C ( S gsum v ) = ( S gsum w ) )
129 6 25 12 128 syl21anc 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> E. w e. Word C ( S gsum v ) = ( S gsum w ) )
130 10 eqeq1d 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> ( Q = ( S gsum w ) <-> ( S gsum v ) = ( S gsum w ) ) )
131 130 rexbidv 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> ( E. w e. Word C Q = ( S gsum w ) <-> E. w e. Word C ( S gsum v ) = ( S gsum w ) ) )
132 129 131 mpbird 
 |-  ( ( ( ( D e. Fin /\ Q e. A ) /\ v e. Word ran ( pmTrsp ` D ) ) /\ Q = ( S gsum v ) ) -> E. w e. Word C Q = ( S gsum w ) )
133 84 sseli 
 |-  ( Q e. A -> Q e. ( Base ` S ) )
134 3 15 19 psgnfitr 
 |-  ( D e. Fin -> ( Q e. ( Base ` S ) <-> E. v e. Word ran ( pmTrsp ` D ) Q = ( S gsum v ) ) )
135 134 biimpa 
 |-  ( ( D e. Fin /\ Q e. ( Base ` S ) ) -> E. v e. Word ran ( pmTrsp ` D ) Q = ( S gsum v ) )
136 133 135 sylan2 
 |-  ( ( D e. Fin /\ Q e. A ) -> E. v e. Word ran ( pmTrsp ` D ) Q = ( S gsum v ) )
137 132 136 r19.29a 
 |-  ( ( D e. Fin /\ Q e. A ) -> E. w e. Word C Q = ( S gsum w ) )
138 simpr 
 |-  ( ( ( D e. Fin /\ w e. Word C ) /\ Q = ( S gsum w ) ) -> Q = ( S gsum w ) )
139 3 altgnsg 
 |-  ( D e. Fin -> ( pmEven ` D ) e. ( NrmSGrp ` S ) )
140 2 139 eqeltrid 
 |-  ( D e. Fin -> A e. ( NrmSGrp ` S ) )
141 nsgsubg 
 |-  ( A e. ( NrmSGrp ` S ) -> A e. ( SubGrp ` S ) )
142 subgsubm 
 |-  ( A e. ( SubGrp ` S ) -> A e. ( SubMnd ` S ) )
143 140 141 142 3syl 
 |-  ( D e. Fin -> A e. ( SubMnd ` S ) )
144 143 adantr 
 |-  ( ( D e. Fin /\ w e. Word C ) -> A e. ( SubMnd ` S ) )
145 sswrd 
 |-  ( C C_ A -> Word C C_ Word A )
146 82 145 syl 
 |-  ( D e. Fin -> Word C C_ Word A )
147 146 sselda 
 |-  ( ( D e. Fin /\ w e. Word C ) -> w e. Word A )
148 gsumwsubmcl 
 |-  ( ( A e. ( SubMnd ` S ) /\ w e. Word A ) -> ( S gsum w ) e. A )
149 144 147 148 syl2anc 
 |-  ( ( D e. Fin /\ w e. Word C ) -> ( S gsum w ) e. A )
150 149 adantr 
 |-  ( ( ( D e. Fin /\ w e. Word C ) /\ Q = ( S gsum w ) ) -> ( S gsum w ) e. A )
151 138 150 eqeltrd 
 |-  ( ( ( D e. Fin /\ w e. Word C ) /\ Q = ( S gsum w ) ) -> Q e. A )
152 151 r19.29an 
 |-  ( ( D e. Fin /\ E. w e. Word C Q = ( S gsum w ) ) -> Q e. A )
153 137 152 impbida 
 |-  ( D e. Fin -> ( Q e. A <-> E. w e. Word C Q = ( S gsum w ) ) )