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 syl5bb
 |-  ( 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 ) )