This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pgpfac1lem2

Description: Lemma for pgpfac1 . (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses pgpfac1.k 
|- K = ( mrCls ` ( SubGrp ` G ) )
pgpfac1.s 
|- S = ( K ` { A } )
pgpfac1.b 
|- B = ( Base ` G )
pgpfac1.o 
|- O = ( od ` G )
pgpfac1.e 
|- E = ( gEx ` G )
pgpfac1.z 
|- .0. = ( 0g ` G )
pgpfac1.l 
|- .(+) = ( LSSum ` G )
pgpfac1.p 
|- ( ph -> P pGrp G )
pgpfac1.g 
|- ( ph -> G e. Abel )
pgpfac1.n 
|- ( ph -> B e. Fin )
pgpfac1.oe 
|- ( ph -> ( O ` A ) = E )
pgpfac1.u 
|- ( ph -> U e. ( SubGrp ` G ) )
pgpfac1.au 
|- ( ph -> A e. U )
pgpfac1.w 
|- ( ph -> W e. ( SubGrp ` G ) )
pgpfac1.i 
|- ( ph -> ( S i^i W ) = { .0. } )
pgpfac1.ss 
|- ( ph -> ( S .(+) W ) C_ U )
pgpfac1.2 
|- ( ph -> A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. ( S .(+) W ) C. w ) )
pgpfac1.c 
|- ( ph -> C e. ( U \ ( S .(+) W ) ) )
pgpfac1.mg 
|- .x. = ( .g ` G )
Assertion pgpfac1lem2 
|- ( ph -> ( P .x. C ) e. ( S .(+) W ) )

Proof

Step Hyp Ref Expression
1 pgpfac1.k 
 |-  K = ( mrCls ` ( SubGrp ` G ) )
2 pgpfac1.s 
 |-  S = ( K ` { A } )
3 pgpfac1.b 
 |-  B = ( Base ` G )
4 pgpfac1.o 
 |-  O = ( od ` G )
5 pgpfac1.e 
 |-  E = ( gEx ` G )
6 pgpfac1.z 
 |-  .0. = ( 0g ` G )
7 pgpfac1.l 
 |-  .(+) = ( LSSum ` G )
8 pgpfac1.p 
 |-  ( ph -> P pGrp G )
9 pgpfac1.g 
 |-  ( ph -> G e. Abel )
10 pgpfac1.n 
 |-  ( ph -> B e. Fin )
11 pgpfac1.oe 
 |-  ( ph -> ( O ` A ) = E )
12 pgpfac1.u 
 |-  ( ph -> U e. ( SubGrp ` G ) )
13 pgpfac1.au 
 |-  ( ph -> A e. U )
14 pgpfac1.w 
 |-  ( ph -> W e. ( SubGrp ` G ) )
15 pgpfac1.i 
 |-  ( ph -> ( S i^i W ) = { .0. } )
16 pgpfac1.ss 
 |-  ( ph -> ( S .(+) W ) C_ U )
17 pgpfac1.2 
 |-  ( ph -> A. w e. ( SubGrp ` G ) ( ( w C. U /\ A e. w ) -> -. ( S .(+) W ) C. w ) )
18 pgpfac1.c 
 |-  ( ph -> C e. ( U \ ( S .(+) W ) ) )
19 pgpfac1.mg 
 |-  .x. = ( .g ` G )
20 18 eldifbd 
 |-  ( ph -> -. C e. ( S .(+) W ) )
21 18 eldifad 
 |-  ( ph -> C e. U )
22 21 adantr 
 |-  ( ( ph /\ -. ( P .x. C ) e. ( S .(+) W ) ) -> C e. U )
23 pgpprm 
 |-  ( P pGrp G -> P e. Prime )
24 8 23 syl 
 |-  ( ph -> P e. Prime )
25 prmz 
 |-  ( P e. Prime -> P e. ZZ )
26 24 25 syl 
 |-  ( ph -> P e. ZZ )
27 19 subgmulgcl 
 |-  ( ( U e. ( SubGrp ` G ) /\ P e. ZZ /\ C e. U ) -> ( P .x. C ) e. U )
28 12 26 21 27 syl3anc 
 |-  ( ph -> ( P .x. C ) e. U )
29 28 adantr 
 |-  ( ( ph /\ -. ( P .x. C ) e. ( S .(+) W ) ) -> ( P .x. C ) e. U )
30 simpr 
 |-  ( ( ph /\ -. ( P .x. C ) e. ( S .(+) W ) ) -> -. ( P .x. C ) e. ( S .(+) W ) )
31 29 30 eldifd 
 |-  ( ( ph /\ -. ( P .x. C ) e. ( S .(+) W ) ) -> ( P .x. C ) e. ( U \ ( S .(+) W ) ) )
32 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pgpfac1lem1 
 |-  ( ( ph /\ ( P .x. C ) e. ( U \ ( S .(+) W ) ) ) -> ( ( S .(+) W ) .(+) ( K ` { ( P .x. C ) } ) ) = U )
33 31 32 syldan 
 |-  ( ( ph /\ -. ( P .x. C ) e. ( S .(+) W ) ) -> ( ( S .(+) W ) .(+) ( K ` { ( P .x. C ) } ) ) = U )
34 22 33 eleqtrrd 
 |-  ( ( ph /\ -. ( P .x. C ) e. ( S .(+) W ) ) -> C e. ( ( S .(+) W ) .(+) ( K ` { ( P .x. C ) } ) ) )
35 34 ex 
 |-  ( ph -> ( -. ( P .x. C ) e. ( S .(+) W ) -> C e. ( ( S .(+) W ) .(+) ( K ` { ( P .x. C ) } ) ) ) )
36 eqid 
 |-  ( -g ` G ) = ( -g ` G )
37 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
38 9 37 syl 
 |-  ( ph -> G e. Grp )
39 3 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` B ) )
40 38 39 syl 
 |-  ( ph -> ( SubGrp ` G ) e. ( ACS ` B ) )
41 40 acsmred 
 |-  ( ph -> ( SubGrp ` G ) e. ( Moore ` B ) )
42 3 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ B )
43 12 42 syl 
 |-  ( ph -> U C_ B )
44 43 13 sseldd 
 |-  ( ph -> A e. B )
45 1 mrcsncl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` B ) /\ A e. B ) -> ( K ` { A } ) e. ( SubGrp ` G ) )
46 41 44 45 syl2anc 
 |-  ( ph -> ( K ` { A } ) e. ( SubGrp ` G ) )
47 2 46 eqeltrid 
 |-  ( ph -> S e. ( SubGrp ` G ) )
48 7 lsmsubg2 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) /\ W e. ( SubGrp ` G ) ) -> ( S .(+) W ) e. ( SubGrp ` G ) )
49 9 47 14 48 syl3anc 
 |-  ( ph -> ( S .(+) W ) e. ( SubGrp ` G ) )
50 43 28 sseldd 
 |-  ( ph -> ( P .x. C ) e. B )
51 1 mrcsncl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` B ) /\ ( P .x. C ) e. B ) -> ( K ` { ( P .x. C ) } ) e. ( SubGrp ` G ) )
52 41 50 51 syl2anc 
 |-  ( ph -> ( K ` { ( P .x. C ) } ) e. ( SubGrp ` G ) )
53 36 7 49 52 lsmelvalm 
 |-  ( ph -> ( C e. ( ( S .(+) W ) .(+) ( K ` { ( P .x. C ) } ) ) <-> E. s e. ( S .(+) W ) E. t e. ( K ` { ( P .x. C ) } ) C = ( s ( -g ` G ) t ) ) )
54 eqid 
 |-  ( k e. ZZ |-> ( k .x. ( P .x. C ) ) ) = ( k e. ZZ |-> ( k .x. ( P .x. C ) ) )
55 3 19 54 1 cycsubg2 
 |-  ( ( G e. Grp /\ ( P .x. C ) e. B ) -> ( K ` { ( P .x. C ) } ) = ran ( k e. ZZ |-> ( k .x. ( P .x. C ) ) ) )
56 38 50 55 syl2anc 
 |-  ( ph -> ( K ` { ( P .x. C ) } ) = ran ( k e. ZZ |-> ( k .x. ( P .x. C ) ) ) )
57 56 rexeqdv 
 |-  ( ph -> ( E. t e. ( K ` { ( P .x. C ) } ) C = ( s ( -g ` G ) t ) <-> E. t e. ran ( k e. ZZ |-> ( k .x. ( P .x. C ) ) ) C = ( s ( -g ` G ) t ) ) )
58 ovex 
 |-  ( k .x. ( P .x. C ) ) e. _V
59 58 rgenw 
 |-  A. k e. ZZ ( k .x. ( P .x. C ) ) e. _V
60 oveq2 
 |-  ( t = ( k .x. ( P .x. C ) ) -> ( s ( -g ` G ) t ) = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) )
61 60 eqeq2d 
 |-  ( t = ( k .x. ( P .x. C ) ) -> ( C = ( s ( -g ` G ) t ) <-> C = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) ) )
62 54 61 rexrnmptw 
 |-  ( A. k e. ZZ ( k .x. ( P .x. C ) ) e. _V -> ( E. t e. ran ( k e. ZZ |-> ( k .x. ( P .x. C ) ) ) C = ( s ( -g ` G ) t ) <-> E. k e. ZZ C = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) ) )
63 59 62 mp1i 
 |-  ( ph -> ( E. t e. ran ( k e. ZZ |-> ( k .x. ( P .x. C ) ) ) C = ( s ( -g ` G ) t ) <-> E. k e. ZZ C = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) ) )
64 57 63 bitrd 
 |-  ( ph -> ( E. t e. ( K ` { ( P .x. C ) } ) C = ( s ( -g ` G ) t ) <-> E. k e. ZZ C = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) ) )
65 64 rexbidv 
 |-  ( ph -> ( E. s e. ( S .(+) W ) E. t e. ( K ` { ( P .x. C ) } ) C = ( s ( -g ` G ) t ) <-> E. s e. ( S .(+) W ) E. k e. ZZ C = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) ) )
66 rexcom 
 |-  ( E. s e. ( S .(+) W ) E. k e. ZZ C = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) <-> E. k e. ZZ E. s e. ( S .(+) W ) C = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) )
67 38 ad2antrr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> G e. Grp )
68 16 43 sstrd 
 |-  ( ph -> ( S .(+) W ) C_ B )
69 68 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> ( S .(+) W ) C_ B )
70 69 sselda 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> s e. B )
71 simplr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> k e. ZZ )
72 50 ad2antrr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> ( P .x. C ) e. B )
73 3 19 mulgcl 
 |-  ( ( G e. Grp /\ k e. ZZ /\ ( P .x. C ) e. B ) -> ( k .x. ( P .x. C ) ) e. B )
74 67 71 72 73 syl3anc 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> ( k .x. ( P .x. C ) ) e. B )
75 43 21 sseldd 
 |-  ( ph -> C e. B )
76 75 ad2antrr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> C e. B )
77 eqid 
 |-  ( +g ` G ) = ( +g ` G )
78 3 77 36 grpsubadd 
 |-  ( ( G e. Grp /\ ( s e. B /\ ( k .x. ( P .x. C ) ) e. B /\ C e. B ) ) -> ( ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) = C <-> ( C ( +g ` G ) ( k .x. ( P .x. C ) ) ) = s ) )
79 67 70 74 76 78 syl13anc 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> ( ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) = C <-> ( C ( +g ` G ) ( k .x. ( P .x. C ) ) ) = s ) )
80 1zzd 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> 1 e. ZZ )
81 26 ad2antrr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> P e. ZZ )
82 71 81 zmulcld 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> ( k x. P ) e. ZZ )
83 3 19 77 mulgdir 
 |-  ( ( G e. Grp /\ ( 1 e. ZZ /\ ( k x. P ) e. ZZ /\ C e. B ) ) -> ( ( 1 + ( k x. P ) ) .x. C ) = ( ( 1 .x. C ) ( +g ` G ) ( ( k x. P ) .x. C ) ) )
84 67 80 82 76 83 syl13anc 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> ( ( 1 + ( k x. P ) ) .x. C ) = ( ( 1 .x. C ) ( +g ` G ) ( ( k x. P ) .x. C ) ) )
85 3 19 mulg1 
 |-  ( C e. B -> ( 1 .x. C ) = C )
86 76 85 syl 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> ( 1 .x. C ) = C )
87 3 19 mulgass 
 |-  ( ( G e. Grp /\ ( k e. ZZ /\ P e. ZZ /\ C e. B ) ) -> ( ( k x. P ) .x. C ) = ( k .x. ( P .x. C ) ) )
88 67 71 81 76 87 syl13anc 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> ( ( k x. P ) .x. C ) = ( k .x. ( P .x. C ) ) )
89 86 88 oveq12d 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> ( ( 1 .x. C ) ( +g ` G ) ( ( k x. P ) .x. C ) ) = ( C ( +g ` G ) ( k .x. ( P .x. C ) ) ) )
90 84 89 eqtrd 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> ( ( 1 + ( k x. P ) ) .x. C ) = ( C ( +g ` G ) ( k .x. ( P .x. C ) ) ) )
91 90 eqeq1d 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> ( ( ( 1 + ( k x. P ) ) .x. C ) = s <-> ( C ( +g ` G ) ( k .x. ( P .x. C ) ) ) = s ) )
92 79 91 bitr4d 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> ( ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) = C <-> ( ( 1 + ( k x. P ) ) .x. C ) = s ) )
93 eqcom 
 |-  ( C = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) <-> ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) = C )
94 eqcom 
 |-  ( s = ( ( 1 + ( k x. P ) ) .x. C ) <-> ( ( 1 + ( k x. P ) ) .x. C ) = s )
95 92 93 94 3bitr4g 
 |-  ( ( ( ph /\ k e. ZZ ) /\ s e. ( S .(+) W ) ) -> ( C = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) <-> s = ( ( 1 + ( k x. P ) ) .x. C ) ) )
96 95 rexbidva 
 |-  ( ( ph /\ k e. ZZ ) -> ( E. s e. ( S .(+) W ) C = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) <-> E. s e. ( S .(+) W ) s = ( ( 1 + ( k x. P ) ) .x. C ) ) )
97 risset 
 |-  ( ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) <-> E. s e. ( S .(+) W ) s = ( ( 1 + ( k x. P ) ) .x. C ) )
98 96 97 bitr4di 
 |-  ( ( ph /\ k e. ZZ ) -> ( E. s e. ( S .(+) W ) C = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) <-> ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) ) )
99 98 rexbidva 
 |-  ( ph -> ( E. k e. ZZ E. s e. ( S .(+) W ) C = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) <-> E. k e. ZZ ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) ) )
100 66 99 bitrid 
 |-  ( ph -> ( E. s e. ( S .(+) W ) E. k e. ZZ C = ( s ( -g ` G ) ( k .x. ( P .x. C ) ) ) <-> E. k e. ZZ ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) ) )
101 53 65 100 3bitrd 
 |-  ( ph -> ( C e. ( ( S .(+) W ) .(+) ( K ` { ( P .x. C ) } ) ) <-> E. k e. ZZ ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) ) )
102 35 101 sylibd 
 |-  ( ph -> ( -. ( P .x. C ) e. ( S .(+) W ) -> E. k e. ZZ ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) ) )
103 38 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> G e. Grp )
104 75 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> C e. B )
105 1z 
 |-  1 e. ZZ
106 id 
 |-  ( k e. ZZ -> k e. ZZ )
107 zmulcl 
 |-  ( ( k e. ZZ /\ P e. ZZ ) -> ( k x. P ) e. ZZ )
108 106 26 107 syl2anr 
 |-  ( ( ph /\ k e. ZZ ) -> ( k x. P ) e. ZZ )
109 zaddcl 
 |-  ( ( 1 e. ZZ /\ ( k x. P ) e. ZZ ) -> ( 1 + ( k x. P ) ) e. ZZ )
110 105 108 109 sylancr 
 |-  ( ( ph /\ k e. ZZ ) -> ( 1 + ( k x. P ) ) e. ZZ )
111 3 4 odcl 
 |-  ( C e. B -> ( O ` C ) e. NN0 )
112 104 111 syl 
 |-  ( ( ph /\ k e. ZZ ) -> ( O ` C ) e. NN0 )
113 112 nn0zd 
 |-  ( ( ph /\ k e. ZZ ) -> ( O ` C ) e. ZZ )
114 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
115 10 114 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
116 115 nn0zd 
 |-  ( ph -> ( # ` B ) e. ZZ )
117 116 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> ( # ` B ) e. ZZ )
118 110 117 gcdcomd 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( 1 + ( k x. P ) ) gcd ( # ` B ) ) = ( ( # ` B ) gcd ( 1 + ( k x. P ) ) ) )
119 3 pgphash 
 |-  ( ( P pGrp G /\ B e. Fin ) -> ( # ` B ) = ( P ^ ( P pCnt ( # ` B ) ) ) )
120 8 10 119 syl2anc 
 |-  ( ph -> ( # ` B ) = ( P ^ ( P pCnt ( # ` B ) ) ) )
121 120 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> ( # ` B ) = ( P ^ ( P pCnt ( # ` B ) ) ) )
122 121 oveq1d 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( # ` B ) gcd ( 1 + ( k x. P ) ) ) = ( ( P ^ ( P pCnt ( # ` B ) ) ) gcd ( 1 + ( k x. P ) ) ) )
123 simpr 
 |-  ( ( ph /\ k e. ZZ ) -> k e. ZZ )
124 26 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> P e. ZZ )
125 1zzd 
 |-  ( ( ph /\ k e. ZZ ) -> 1 e. ZZ )
126 gcdaddm 
 |-  ( ( k e. ZZ /\ P e. ZZ /\ 1 e. ZZ ) -> ( P gcd 1 ) = ( P gcd ( 1 + ( k x. P ) ) ) )
127 123 124 125 126 syl3anc 
 |-  ( ( ph /\ k e. ZZ ) -> ( P gcd 1 ) = ( P gcd ( 1 + ( k x. P ) ) ) )
128 gcd1 
 |-  ( P e. ZZ -> ( P gcd 1 ) = 1 )
129 124 128 syl 
 |-  ( ( ph /\ k e. ZZ ) -> ( P gcd 1 ) = 1 )
130 127 129 eqtr3d 
 |-  ( ( ph /\ k e. ZZ ) -> ( P gcd ( 1 + ( k x. P ) ) ) = 1 )
131 3 grpbn0 
 |-  ( G e. Grp -> B =/= (/) )
132 38 131 syl 
 |-  ( ph -> B =/= (/) )
133 hashnncl 
 |-  ( B e. Fin -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
134 10 133 syl 
 |-  ( ph -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
135 132 134 mpbird 
 |-  ( ph -> ( # ` B ) e. NN )
136 24 135 pccld 
 |-  ( ph -> ( P pCnt ( # ` B ) ) e. NN0 )
137 136 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> ( P pCnt ( # ` B ) ) e. NN0 )
138 rpexp1i 
 |-  ( ( P e. ZZ /\ ( 1 + ( k x. P ) ) e. ZZ /\ ( P pCnt ( # ` B ) ) e. NN0 ) -> ( ( P gcd ( 1 + ( k x. P ) ) ) = 1 -> ( ( P ^ ( P pCnt ( # ` B ) ) ) gcd ( 1 + ( k x. P ) ) ) = 1 ) )
139 124 110 137 138 syl3anc 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( P gcd ( 1 + ( k x. P ) ) ) = 1 -> ( ( P ^ ( P pCnt ( # ` B ) ) ) gcd ( 1 + ( k x. P ) ) ) = 1 ) )
140 130 139 mpd 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( P ^ ( P pCnt ( # ` B ) ) ) gcd ( 1 + ( k x. P ) ) ) = 1 )
141 118 122 140 3eqtrd 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( 1 + ( k x. P ) ) gcd ( # ` B ) ) = 1 )
142 3 4 oddvds2 
 |-  ( ( G e. Grp /\ B e. Fin /\ C e. B ) -> ( O ` C ) || ( # ` B ) )
143 38 10 75 142 syl3anc 
 |-  ( ph -> ( O ` C ) || ( # ` B ) )
144 143 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> ( O ` C ) || ( # ` B ) )
145 rpdvds 
 |-  ( ( ( ( 1 + ( k x. P ) ) e. ZZ /\ ( O ` C ) e. ZZ /\ ( # ` B ) e. ZZ ) /\ ( ( ( 1 + ( k x. P ) ) gcd ( # ` B ) ) = 1 /\ ( O ` C ) || ( # ` B ) ) ) -> ( ( 1 + ( k x. P ) ) gcd ( O ` C ) ) = 1 )
146 110 113 117 141 144 145 syl32anc 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( 1 + ( k x. P ) ) gcd ( O ` C ) ) = 1 )
147 3 4 19 odbezout 
 |-  ( ( ( G e. Grp /\ C e. B /\ ( 1 + ( k x. P ) ) e. ZZ ) /\ ( ( 1 + ( k x. P ) ) gcd ( O ` C ) ) = 1 ) -> E. a e. ZZ ( a .x. ( ( 1 + ( k x. P ) ) .x. C ) ) = C )
148 103 104 110 146 147 syl31anc 
 |-  ( ( ph /\ k e. ZZ ) -> E. a e. ZZ ( a .x. ( ( 1 + ( k x. P ) ) .x. C ) ) = C )
149 49 ad2antrr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ a e. ZZ ) -> ( S .(+) W ) e. ( SubGrp ` G ) )
150 simpr 
 |-  ( ( ( ph /\ k e. ZZ ) /\ a e. ZZ ) -> a e. ZZ )
151 19 subgmulgcl 
 |-  ( ( ( S .(+) W ) e. ( SubGrp ` G ) /\ a e. ZZ /\ ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) ) -> ( a .x. ( ( 1 + ( k x. P ) ) .x. C ) ) e. ( S .(+) W ) )
152 151 3expia 
 |-  ( ( ( S .(+) W ) e. ( SubGrp ` G ) /\ a e. ZZ ) -> ( ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) -> ( a .x. ( ( 1 + ( k x. P ) ) .x. C ) ) e. ( S .(+) W ) ) )
153 149 150 152 syl2anc 
 |-  ( ( ( ph /\ k e. ZZ ) /\ a e. ZZ ) -> ( ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) -> ( a .x. ( ( 1 + ( k x. P ) ) .x. C ) ) e. ( S .(+) W ) ) )
154 eleq1 
 |-  ( ( a .x. ( ( 1 + ( k x. P ) ) .x. C ) ) = C -> ( ( a .x. ( ( 1 + ( k x. P ) ) .x. C ) ) e. ( S .(+) W ) <-> C e. ( S .(+) W ) ) )
155 154 imbi2d 
 |-  ( ( a .x. ( ( 1 + ( k x. P ) ) .x. C ) ) = C -> ( ( ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) -> ( a .x. ( ( 1 + ( k x. P ) ) .x. C ) ) e. ( S .(+) W ) ) <-> ( ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) -> C e. ( S .(+) W ) ) ) )
156 153 155 syl5ibcom 
 |-  ( ( ( ph /\ k e. ZZ ) /\ a e. ZZ ) -> ( ( a .x. ( ( 1 + ( k x. P ) ) .x. C ) ) = C -> ( ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) -> C e. ( S .(+) W ) ) ) )
157 156 rexlimdva 
 |-  ( ( ph /\ k e. ZZ ) -> ( E. a e. ZZ ( a .x. ( ( 1 + ( k x. P ) ) .x. C ) ) = C -> ( ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) -> C e. ( S .(+) W ) ) ) )
158 148 157 mpd 
 |-  ( ( ph /\ k e. ZZ ) -> ( ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) -> C e. ( S .(+) W ) ) )
159 158 rexlimdva 
 |-  ( ph -> ( E. k e. ZZ ( ( 1 + ( k x. P ) ) .x. C ) e. ( S .(+) W ) -> C e. ( S .(+) W ) ) )
160 102 159 syld 
 |-  ( ph -> ( -. ( P .x. C ) e. ( S .(+) W ) -> C e. ( S .(+) W ) ) )
161 20 160 mt3d 
 |-  ( ph -> ( P .x. C ) e. ( S .(+) W ) )