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

Metamath Proof Explorer

Theorem pgpfac1lem3

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 )
pgpfac1.m 
|- ( ph -> M e. ZZ )
pgpfac1.mw 
|- ( ph -> ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) e. W )
pgpfac1.d 
|- D = ( C ( +g ` G ) ( ( M / P ) .x. A ) )
Assertion pgpfac1lem3 
|- ( ph -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) )

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 pgpfac1.m 
 |-  ( ph -> M e. ZZ )
21 pgpfac1.mw 
 |-  ( ph -> ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) e. W )
22 pgpfac1.d 
 |-  D = ( C ( +g ` G ) ( ( M / P ) .x. A ) )
23 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
24 9 23 syl 
 |-  ( ph -> G e. Grp )
25 3 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` B ) )
26 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` B ) -> ( SubGrp ` G ) e. ( Moore ` B ) )
27 24 25 26 3syl 
 |-  ( ph -> ( SubGrp ` G ) e. ( Moore ` B ) )
28 3 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ B )
29 12 28 syl 
 |-  ( ph -> U C_ B )
30 18 eldifad 
 |-  ( ph -> C e. U )
31 29 13 sseldd 
 |-  ( ph -> A e. B )
32 1 mrcsncl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` B ) /\ A e. B ) -> ( K ` { A } ) e. ( SubGrp ` G ) )
33 27 31 32 syl2anc 
 |-  ( ph -> ( K ` { A } ) e. ( SubGrp ` G ) )
34 2 33 eqeltrid 
 |-  ( ph -> S e. ( SubGrp ` G ) )
35 7 lsmub1 
 |-  ( ( S e. ( SubGrp ` G ) /\ W e. ( SubGrp ` G ) ) -> S C_ ( S .(+) W ) )
36 34 14 35 syl2anc 
 |-  ( ph -> S C_ ( S .(+) W ) )
37 36 16 sstrd 
 |-  ( ph -> S C_ U )
38 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 pgpfac1lem3a 
 |-  ( ph -> ( P || E /\ P || M ) )
39 38 simprd 
 |-  ( ph -> P || M )
40 pgpprm 
 |-  ( P pGrp G -> P e. Prime )
41 8 40 syl 
 |-  ( ph -> P e. Prime )
42 prmz 
 |-  ( P e. Prime -> P e. ZZ )
43 41 42 syl 
 |-  ( ph -> P e. ZZ )
44 prmnn 
 |-  ( P e. Prime -> P e. NN )
45 41 44 syl 
 |-  ( ph -> P e. NN )
46 45 nnne0d 
 |-  ( ph -> P =/= 0 )
47 dvdsval2 
 |-  ( ( P e. ZZ /\ P =/= 0 /\ M e. ZZ ) -> ( P || M <-> ( M / P ) e. ZZ ) )
48 43 46 20 47 syl3anc 
 |-  ( ph -> ( P || M <-> ( M / P ) e. ZZ ) )
49 39 48 mpbid 
 |-  ( ph -> ( M / P ) e. ZZ )
50 31 snssd 
 |-  ( ph -> { A } C_ B )
51 27 1 50 mrcssidd 
 |-  ( ph -> { A } C_ ( K ` { A } ) )
52 51 2 sseqtrrdi 
 |-  ( ph -> { A } C_ S )
53 snssg 
 |-  ( A e. U -> ( A e. S <-> { A } C_ S ) )
54 13 53 syl 
 |-  ( ph -> ( A e. S <-> { A } C_ S ) )
55 52 54 mpbird 
 |-  ( ph -> A e. S )
56 19 subgmulgcl 
 |-  ( ( S e. ( SubGrp ` G ) /\ ( M / P ) e. ZZ /\ A e. S ) -> ( ( M / P ) .x. A ) e. S )
57 34 49 55 56 syl3anc 
 |-  ( ph -> ( ( M / P ) .x. A ) e. S )
58 37 57 sseldd 
 |-  ( ph -> ( ( M / P ) .x. A ) e. U )
59 eqid 
 |-  ( +g ` G ) = ( +g ` G )
60 59 subgcl 
 |-  ( ( U e. ( SubGrp ` G ) /\ C e. U /\ ( ( M / P ) .x. A ) e. U ) -> ( C ( +g ` G ) ( ( M / P ) .x. A ) ) e. U )
61 12 30 58 60 syl3anc 
 |-  ( ph -> ( C ( +g ` G ) ( ( M / P ) .x. A ) ) e. U )
62 22 61 eqeltrid 
 |-  ( ph -> D e. U )
63 29 62 sseldd 
 |-  ( ph -> D e. B )
64 1 mrcsncl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` B ) /\ D e. B ) -> ( K ` { D } ) e. ( SubGrp ` G ) )
65 27 63 64 syl2anc 
 |-  ( ph -> ( K ` { D } ) e. ( SubGrp ` G ) )
66 7 lsmsubg2 
 |-  ( ( G e. Abel /\ W e. ( SubGrp ` G ) /\ ( K ` { D } ) e. ( SubGrp ` G ) ) -> ( W .(+) ( K ` { D } ) ) e. ( SubGrp ` G ) )
67 9 14 65 66 syl3anc 
 |-  ( ph -> ( W .(+) ( K ` { D } ) ) e. ( SubGrp ` G ) )
68 eqid 
 |-  ( -g ` G ) = ( -g ` G )
69 68 7 14 65 lsmelvalm 
 |-  ( ph -> ( x e. ( W .(+) ( K ` { D } ) ) <-> E. w e. W E. y e. ( K ` { D } ) x = ( w ( -g ` G ) y ) ) )
70 eqid 
 |-  ( n e. ZZ |-> ( n .x. D ) ) = ( n e. ZZ |-> ( n .x. D ) )
71 3 19 70 1 cycsubg2 
 |-  ( ( G e. Grp /\ D e. B ) -> ( K ` { D } ) = ran ( n e. ZZ |-> ( n .x. D ) ) )
72 24 63 71 syl2anc 
 |-  ( ph -> ( K ` { D } ) = ran ( n e. ZZ |-> ( n .x. D ) ) )
73 72 rexeqdv 
 |-  ( ph -> ( E. y e. ( K ` { D } ) x = ( w ( -g ` G ) y ) <-> E. y e. ran ( n e. ZZ |-> ( n .x. D ) ) x = ( w ( -g ` G ) y ) ) )
74 ovex 
 |-  ( n .x. D ) e. _V
75 74 rgenw 
 |-  A. n e. ZZ ( n .x. D ) e. _V
76 oveq2 
 |-  ( y = ( n .x. D ) -> ( w ( -g ` G ) y ) = ( w ( -g ` G ) ( n .x. D ) ) )
77 76 eqeq2d 
 |-  ( y = ( n .x. D ) -> ( x = ( w ( -g ` G ) y ) <-> x = ( w ( -g ` G ) ( n .x. D ) ) ) )
78 70 77 rexrnmptw 
 |-  ( A. n e. ZZ ( n .x. D ) e. _V -> ( E. y e. ran ( n e. ZZ |-> ( n .x. D ) ) x = ( w ( -g ` G ) y ) <-> E. n e. ZZ x = ( w ( -g ` G ) ( n .x. D ) ) ) )
79 75 78 ax-mp 
 |-  ( E. y e. ran ( n e. ZZ |-> ( n .x. D ) ) x = ( w ( -g ` G ) y ) <-> E. n e. ZZ x = ( w ( -g ` G ) ( n .x. D ) ) )
80 73 79 bitrdi 
 |-  ( ph -> ( E. y e. ( K ` { D } ) x = ( w ( -g ` G ) y ) <-> E. n e. ZZ x = ( w ( -g ` G ) ( n .x. D ) ) ) )
81 80 rexbidv 
 |-  ( ph -> ( E. w e. W E. y e. ( K ` { D } ) x = ( w ( -g ` G ) y ) <-> E. w e. W E. n e. ZZ x = ( w ( -g ` G ) ( n .x. D ) ) ) )
82 69 81 bitrd 
 |-  ( ph -> ( x e. ( W .(+) ( K ` { D } ) ) <-> E. w e. W E. n e. ZZ x = ( w ( -g ` G ) ( n .x. D ) ) ) )
83 82 adantr 
 |-  ( ( ph /\ x e. S ) -> ( x e. ( W .(+) ( K ` { D } ) ) <-> E. w e. W E. n e. ZZ x = ( w ( -g ` G ) ( n .x. D ) ) ) )
84 simpr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> x = ( w ( -g ` G ) ( n .x. D ) ) )
85 14 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> W e. ( SubGrp ` G ) )
86 simplrl 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> w e. W )
87 simplrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> n e. ZZ )
88 87 zcnd 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> n e. CC )
89 45 nncnd 
 |-  ( ph -> P e. CC )
90 89 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> P e. CC )
91 46 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> P =/= 0 )
92 88 90 91 divcan1d 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( ( n / P ) x. P ) = n )
93 92 oveq1d 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( ( ( n / P ) x. P ) .x. D ) = ( n .x. D ) )
94 24 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> G e. Grp )
95 18 eldifbd 
 |-  ( ph -> -. C e. ( S .(+) W ) )
96 7 lsmsubg2 
 |-  ( ( G e. Abel /\ S e. ( SubGrp ` G ) /\ W e. ( SubGrp ` G ) ) -> ( S .(+) W ) e. ( SubGrp ` G ) )
97 9 34 14 96 syl3anc 
 |-  ( ph -> ( S .(+) W ) e. ( SubGrp ` G ) )
98 36 57 sseldd 
 |-  ( ph -> ( ( M / P ) .x. A ) e. ( S .(+) W ) )
99 68 subgsubcl 
 |-  ( ( ( S .(+) W ) e. ( SubGrp ` G ) /\ D e. ( S .(+) W ) /\ ( ( M / P ) .x. A ) e. ( S .(+) W ) ) -> ( D ( -g ` G ) ( ( M / P ) .x. A ) ) e. ( S .(+) W ) )
100 99 3expia 
 |-  ( ( ( S .(+) W ) e. ( SubGrp ` G ) /\ D e. ( S .(+) W ) ) -> ( ( ( M / P ) .x. A ) e. ( S .(+) W ) -> ( D ( -g ` G ) ( ( M / P ) .x. A ) ) e. ( S .(+) W ) ) )
101 100 impancom 
 |-  ( ( ( S .(+) W ) e. ( SubGrp ` G ) /\ ( ( M / P ) .x. A ) e. ( S .(+) W ) ) -> ( D e. ( S .(+) W ) -> ( D ( -g ` G ) ( ( M / P ) .x. A ) ) e. ( S .(+) W ) ) )
102 97 98 101 syl2anc 
 |-  ( ph -> ( D e. ( S .(+) W ) -> ( D ( -g ` G ) ( ( M / P ) .x. A ) ) e. ( S .(+) W ) ) )
103 22 oveq1i 
 |-  ( D ( -g ` G ) ( ( M / P ) .x. A ) ) = ( ( C ( +g ` G ) ( ( M / P ) .x. A ) ) ( -g ` G ) ( ( M / P ) .x. A ) )
104 29 30 sseldd 
 |-  ( ph -> C e. B )
105 3 subgss 
 |-  ( S e. ( SubGrp ` G ) -> S C_ B )
106 34 105 syl 
 |-  ( ph -> S C_ B )
107 106 57 sseldd 
 |-  ( ph -> ( ( M / P ) .x. A ) e. B )
108 3 59 68 grppncan 
 |-  ( ( G e. Grp /\ C e. B /\ ( ( M / P ) .x. A ) e. B ) -> ( ( C ( +g ` G ) ( ( M / P ) .x. A ) ) ( -g ` G ) ( ( M / P ) .x. A ) ) = C )
109 24 104 107 108 syl3anc 
 |-  ( ph -> ( ( C ( +g ` G ) ( ( M / P ) .x. A ) ) ( -g ` G ) ( ( M / P ) .x. A ) ) = C )
110 103 109 eqtrid 
 |-  ( ph -> ( D ( -g ` G ) ( ( M / P ) .x. A ) ) = C )
111 110 eleq1d 
 |-  ( ph -> ( ( D ( -g ` G ) ( ( M / P ) .x. A ) ) e. ( S .(+) W ) <-> C e. ( S .(+) W ) ) )
112 102 111 sylibd 
 |-  ( ph -> ( D e. ( S .(+) W ) -> C e. ( S .(+) W ) ) )
113 95 112 mtod 
 |-  ( ph -> -. D e. ( S .(+) W ) )
114 113 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> -. D e. ( S .(+) W ) )
115 41 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> P e. Prime )
116 coprm 
 |-  ( ( P e. Prime /\ n e. ZZ ) -> ( -. P || n <-> ( P gcd n ) = 1 ) )
117 115 87 116 syl2anc 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( -. P || n <-> ( P gcd n ) = 1 ) )
118 43 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> P e. ZZ )
119 bezout 
 |-  ( ( P e. ZZ /\ n e. ZZ ) -> E. a e. ZZ E. b e. ZZ ( P gcd n ) = ( ( P x. a ) + ( n x. b ) ) )
120 118 87 119 syl2anc 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> E. a e. ZZ E. b e. ZZ ( P gcd n ) = ( ( P x. a ) + ( n x. b ) ) )
121 eqeq1 
 |-  ( ( P gcd n ) = 1 -> ( ( P gcd n ) = ( ( P x. a ) + ( n x. b ) ) <-> 1 = ( ( P x. a ) + ( n x. b ) ) ) )
122 121 2rexbidv 
 |-  ( ( P gcd n ) = 1 -> ( E. a e. ZZ E. b e. ZZ ( P gcd n ) = ( ( P x. a ) + ( n x. b ) ) <-> E. a e. ZZ E. b e. ZZ 1 = ( ( P x. a ) + ( n x. b ) ) ) )
123 120 122 syl5ibcom 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( ( P gcd n ) = 1 -> E. a e. ZZ E. b e. ZZ 1 = ( ( P x. a ) + ( n x. b ) ) ) )
124 94 adantr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> G e. Grp )
125 118 adantr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> P e. ZZ )
126 simprl 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ZZ )
127 125 126 zmulcld 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( P x. a ) e. ZZ )
128 87 adantr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> n e. ZZ )
129 simprr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. ZZ )
130 128 129 zmulcld 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( n x. b ) e. ZZ )
131 63 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> D e. B )
132 131 adantr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> D e. B )
133 3 19 59 mulgdir 
 |-  ( ( G e. Grp /\ ( ( P x. a ) e. ZZ /\ ( n x. b ) e. ZZ /\ D e. B ) ) -> ( ( ( P x. a ) + ( n x. b ) ) .x. D ) = ( ( ( P x. a ) .x. D ) ( +g ` G ) ( ( n x. b ) .x. D ) ) )
134 124 127 130 132 133 syl13anc 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( P x. a ) + ( n x. b ) ) .x. D ) = ( ( ( P x. a ) .x. D ) ( +g ` G ) ( ( n x. b ) .x. D ) ) )
135 97 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( S .(+) W ) e. ( SubGrp ` G ) )
136 135 adantr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( S .(+) W ) e. ( SubGrp ` G ) )
137 90 adantr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> P e. CC )
138 zcn 
 |-  ( a e. ZZ -> a e. CC )
139 138 ad2antrl 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. CC )
140 137 139 mulcomd 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( P x. a ) = ( a x. P ) )
141 140 oveq1d 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( P x. a ) .x. D ) = ( ( a x. P ) .x. D ) )
142 3 19 mulgass 
 |-  ( ( G e. Grp /\ ( a e. ZZ /\ P e. ZZ /\ D e. B ) ) -> ( ( a x. P ) .x. D ) = ( a .x. ( P .x. D ) ) )
143 124 126 125 132 142 syl13anc 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a x. P ) .x. D ) = ( a .x. ( P .x. D ) ) )
144 141 143 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( P x. a ) .x. D ) = ( a .x. ( P .x. D ) ) )
145 7 lsmub2 
 |-  ( ( S e. ( SubGrp ` G ) /\ W e. ( SubGrp ` G ) ) -> W C_ ( S .(+) W ) )
146 34 14 145 syl2anc 
 |-  ( ph -> W C_ ( S .(+) W ) )
147 22 oveq2i 
 |-  ( P .x. D ) = ( P .x. ( C ( +g ` G ) ( ( M / P ) .x. A ) ) )
148 3 19 59 mulgdi 
 |-  ( ( G e. Abel /\ ( P e. ZZ /\ C e. B /\ ( ( M / P ) .x. A ) e. B ) ) -> ( P .x. ( C ( +g ` G ) ( ( M / P ) .x. A ) ) ) = ( ( P .x. C ) ( +g ` G ) ( P .x. ( ( M / P ) .x. A ) ) ) )
149 9 43 104 107 148 syl13anc 
 |-  ( ph -> ( P .x. ( C ( +g ` G ) ( ( M / P ) .x. A ) ) ) = ( ( P .x. C ) ( +g ` G ) ( P .x. ( ( M / P ) .x. A ) ) ) )
150 147 149 eqtrid 
 |-  ( ph -> ( P .x. D ) = ( ( P .x. C ) ( +g ` G ) ( P .x. ( ( M / P ) .x. A ) ) ) )
151 3 19 mulgass 
 |-  ( ( G e. Grp /\ ( P e. ZZ /\ ( M / P ) e. ZZ /\ A e. B ) ) -> ( ( P x. ( M / P ) ) .x. A ) = ( P .x. ( ( M / P ) .x. A ) ) )
152 24 43 49 31 151 syl13anc 
 |-  ( ph -> ( ( P x. ( M / P ) ) .x. A ) = ( P .x. ( ( M / P ) .x. A ) ) )
153 20 zcnd 
 |-  ( ph -> M e. CC )
154 153 89 46 divcan2d 
 |-  ( ph -> ( P x. ( M / P ) ) = M )
155 154 oveq1d 
 |-  ( ph -> ( ( P x. ( M / P ) ) .x. A ) = ( M .x. A ) )
156 152 155 eqtr3d 
 |-  ( ph -> ( P .x. ( ( M / P ) .x. A ) ) = ( M .x. A ) )
157 156 oveq2d 
 |-  ( ph -> ( ( P .x. C ) ( +g ` G ) ( P .x. ( ( M / P ) .x. A ) ) ) = ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) )
158 150 157 eqtrd 
 |-  ( ph -> ( P .x. D ) = ( ( P .x. C ) ( +g ` G ) ( M .x. A ) ) )
159 158 21 eqeltrd 
 |-  ( ph -> ( P .x. D ) e. W )
160 146 159 sseldd 
 |-  ( ph -> ( P .x. D ) e. ( S .(+) W ) )
161 160 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( P .x. D ) e. ( S .(+) W ) )
162 161 adantr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( P .x. D ) e. ( S .(+) W ) )
163 19 subgmulgcl 
 |-  ( ( ( S .(+) W ) e. ( SubGrp ` G ) /\ a e. ZZ /\ ( P .x. D ) e. ( S .(+) W ) ) -> ( a .x. ( P .x. D ) ) e. ( S .(+) W ) )
164 136 126 162 163 syl3anc 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a .x. ( P .x. D ) ) e. ( S .(+) W ) )
165 144 164 eqeltrd 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( P x. a ) .x. D ) e. ( S .(+) W ) )
166 88 adantr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> n e. CC )
167 zcn 
 |-  ( b e. ZZ -> b e. CC )
168 167 ad2antll 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. CC )
169 166 168 mulcomd 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( n x. b ) = ( b x. n ) )
170 169 oveq1d 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( n x. b ) .x. D ) = ( ( b x. n ) .x. D ) )
171 3 19 mulgass 
 |-  ( ( G e. Grp /\ ( b e. ZZ /\ n e. ZZ /\ D e. B ) ) -> ( ( b x. n ) .x. D ) = ( b .x. ( n .x. D ) ) )
172 124 129 128 132 171 syl13anc 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( b x. n ) .x. D ) = ( b .x. ( n .x. D ) ) )
173 170 172 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( n x. b ) .x. D ) = ( b .x. ( n .x. D ) ) )
174 84 oveq2d 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( w ( -g ` G ) x ) = ( w ( -g ` G ) ( w ( -g ` G ) ( n .x. D ) ) ) )
175 9 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> G e. Abel )
176 3 subgss 
 |-  ( W e. ( SubGrp ` G ) -> W C_ B )
177 85 176 syl 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> W C_ B )
178 177 86 sseldd 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> w e. B )
179 3 19 mulgcl 
 |-  ( ( G e. Grp /\ n e. ZZ /\ D e. B ) -> ( n .x. D ) e. B )
180 94 87 131 179 syl3anc 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( n .x. D ) e. B )
181 3 68 175 178 180 ablnncan 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( w ( -g ` G ) ( w ( -g ` G ) ( n .x. D ) ) ) = ( n .x. D ) )
182 174 181 eqtrd 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( w ( -g ` G ) x ) = ( n .x. D ) )
183 146 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> W C_ ( S .(+) W ) )
184 183 86 sseldd 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> w e. ( S .(+) W ) )
185 36 sselda 
 |-  ( ( ph /\ x e. S ) -> x e. ( S .(+) W ) )
186 185 ad2antrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> x e. ( S .(+) W ) )
187 68 subgsubcl 
 |-  ( ( ( S .(+) W ) e. ( SubGrp ` G ) /\ w e. ( S .(+) W ) /\ x e. ( S .(+) W ) ) -> ( w ( -g ` G ) x ) e. ( S .(+) W ) )
188 135 184 186 187 syl3anc 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( w ( -g ` G ) x ) e. ( S .(+) W ) )
189 182 188 eqeltrrd 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( n .x. D ) e. ( S .(+) W ) )
190 189 adantr 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( n .x. D ) e. ( S .(+) W ) )
191 19 subgmulgcl 
 |-  ( ( ( S .(+) W ) e. ( SubGrp ` G ) /\ b e. ZZ /\ ( n .x. D ) e. ( S .(+) W ) ) -> ( b .x. ( n .x. D ) ) e. ( S .(+) W ) )
192 136 129 190 191 syl3anc 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( b .x. ( n .x. D ) ) e. ( S .(+) W ) )
193 173 192 eqeltrd 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( n x. b ) .x. D ) e. ( S .(+) W ) )
194 59 subgcl 
 |-  ( ( ( S .(+) W ) e. ( SubGrp ` G ) /\ ( ( P x. a ) .x. D ) e. ( S .(+) W ) /\ ( ( n x. b ) .x. D ) e. ( S .(+) W ) ) -> ( ( ( P x. a ) .x. D ) ( +g ` G ) ( ( n x. b ) .x. D ) ) e. ( S .(+) W ) )
195 136 165 193 194 syl3anc 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( P x. a ) .x. D ) ( +g ` G ) ( ( n x. b ) .x. D ) ) e. ( S .(+) W ) )
196 134 195 eqeltrd 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( P x. a ) + ( n x. b ) ) .x. D ) e. ( S .(+) W ) )
197 oveq1 
 |-  ( 1 = ( ( P x. a ) + ( n x. b ) ) -> ( 1 .x. D ) = ( ( ( P x. a ) + ( n x. b ) ) .x. D ) )
198 197 eleq1d 
 |-  ( 1 = ( ( P x. a ) + ( n x. b ) ) -> ( ( 1 .x. D ) e. ( S .(+) W ) <-> ( ( ( P x. a ) + ( n x. b ) ) .x. D ) e. ( S .(+) W ) ) )
199 196 198 syl5ibrcom 
 |-  ( ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( 1 = ( ( P x. a ) + ( n x. b ) ) -> ( 1 .x. D ) e. ( S .(+) W ) ) )
200 199 rexlimdvva 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( E. a e. ZZ E. b e. ZZ 1 = ( ( P x. a ) + ( n x. b ) ) -> ( 1 .x. D ) e. ( S .(+) W ) ) )
201 123 200 syld 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( ( P gcd n ) = 1 -> ( 1 .x. D ) e. ( S .(+) W ) ) )
202 3 19 mulg1 
 |-  ( D e. B -> ( 1 .x. D ) = D )
203 131 202 syl 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( 1 .x. D ) = D )
204 203 eleq1d 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( ( 1 .x. D ) e. ( S .(+) W ) <-> D e. ( S .(+) W ) ) )
205 201 204 sylibd 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( ( P gcd n ) = 1 -> D e. ( S .(+) W ) ) )
206 117 205 sylbid 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( -. P || n -> D e. ( S .(+) W ) ) )
207 114 206 mt3d 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> P || n )
208 dvdsval2 
 |-  ( ( P e. ZZ /\ P =/= 0 /\ n e. ZZ ) -> ( P || n <-> ( n / P ) e. ZZ ) )
209 118 91 87 208 syl3anc 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( P || n <-> ( n / P ) e. ZZ ) )
210 207 209 mpbid 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( n / P ) e. ZZ )
211 3 19 mulgass 
 |-  ( ( G e. Grp /\ ( ( n / P ) e. ZZ /\ P e. ZZ /\ D e. B ) ) -> ( ( ( n / P ) x. P ) .x. D ) = ( ( n / P ) .x. ( P .x. D ) ) )
212 94 210 118 131 211 syl13anc 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( ( ( n / P ) x. P ) .x. D ) = ( ( n / P ) .x. ( P .x. D ) ) )
213 93 212 eqtr3d 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( n .x. D ) = ( ( n / P ) .x. ( P .x. D ) ) )
214 159 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( P .x. D ) e. W )
215 19 subgmulgcl 
 |-  ( ( W e. ( SubGrp ` G ) /\ ( n / P ) e. ZZ /\ ( P .x. D ) e. W ) -> ( ( n / P ) .x. ( P .x. D ) ) e. W )
216 85 210 214 215 syl3anc 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( ( n / P ) .x. ( P .x. D ) ) e. W )
217 213 216 eqeltrd 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( n .x. D ) e. W )
218 68 subgsubcl 
 |-  ( ( W e. ( SubGrp ` G ) /\ w e. W /\ ( n .x. D ) e. W ) -> ( w ( -g ` G ) ( n .x. D ) ) e. W )
219 85 86 217 218 syl3anc 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> ( w ( -g ` G ) ( n .x. D ) ) e. W )
220 84 219 eqeltrd 
 |-  ( ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) /\ x = ( w ( -g ` G ) ( n .x. D ) ) ) -> x e. W )
221 220 ex 
 |-  ( ( ( ph /\ x e. S ) /\ ( w e. W /\ n e. ZZ ) ) -> ( x = ( w ( -g ` G ) ( n .x. D ) ) -> x e. W ) )
222 221 rexlimdvva 
 |-  ( ( ph /\ x e. S ) -> ( E. w e. W E. n e. ZZ x = ( w ( -g ` G ) ( n .x. D ) ) -> x e. W ) )
223 83 222 sylbid 
 |-  ( ( ph /\ x e. S ) -> ( x e. ( W .(+) ( K ` { D } ) ) -> x e. W ) )
224 223 imdistanda 
 |-  ( ph -> ( ( x e. S /\ x e. ( W .(+) ( K ` { D } ) ) ) -> ( x e. S /\ x e. W ) ) )
225 elin 
 |-  ( x e. ( S i^i ( W .(+) ( K ` { D } ) ) ) <-> ( x e. S /\ x e. ( W .(+) ( K ` { D } ) ) ) )
226 elin 
 |-  ( x e. ( S i^i W ) <-> ( x e. S /\ x e. W ) )
227 224 225 226 3imtr4g 
 |-  ( ph -> ( x e. ( S i^i ( W .(+) ( K ` { D } ) ) ) -> x e. ( S i^i W ) ) )
228 227 ssrdv 
 |-  ( ph -> ( S i^i ( W .(+) ( K ` { D } ) ) ) C_ ( S i^i W ) )
229 228 15 sseqtrd 
 |-  ( ph -> ( S i^i ( W .(+) ( K ` { D } ) ) ) C_ { .0. } )
230 6 subg0cl 
 |-  ( S e. ( SubGrp ` G ) -> .0. e. S )
231 34 230 syl 
 |-  ( ph -> .0. e. S )
232 6 subg0cl 
 |-  ( ( W .(+) ( K ` { D } ) ) e. ( SubGrp ` G ) -> .0. e. ( W .(+) ( K ` { D } ) ) )
233 67 232 syl 
 |-  ( ph -> .0. e. ( W .(+) ( K ` { D } ) ) )
234 231 233 elind 
 |-  ( ph -> .0. e. ( S i^i ( W .(+) ( K ` { D } ) ) ) )
235 234 snssd 
 |-  ( ph -> { .0. } C_ ( S i^i ( W .(+) ( K ` { D } ) ) ) )
236 229 235 eqssd 
 |-  ( ph -> ( S i^i ( W .(+) ( K ` { D } ) ) ) = { .0. } )
237 7 lsmass 
 |-  ( ( S e. ( SubGrp ` G ) /\ W e. ( SubGrp ` G ) /\ ( K ` { D } ) e. ( SubGrp ` G ) ) -> ( ( S .(+) W ) .(+) ( K ` { D } ) ) = ( S .(+) ( W .(+) ( K ` { D } ) ) ) )
238 34 14 65 237 syl3anc 
 |-  ( ph -> ( ( S .(+) W ) .(+) ( K ` { D } ) ) = ( S .(+) ( W .(+) ( K ` { D } ) ) ) )
239 62 113 eldifd 
 |-  ( ph -> D e. ( U \ ( S .(+) W ) ) )
240 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pgpfac1lem1 
 |-  ( ( ph /\ D e. ( U \ ( S .(+) W ) ) ) -> ( ( S .(+) W ) .(+) ( K ` { D } ) ) = U )
241 239 240 mpdan 
 |-  ( ph -> ( ( S .(+) W ) .(+) ( K ` { D } ) ) = U )
242 238 241 eqtr3d 
 |-  ( ph -> ( S .(+) ( W .(+) ( K ` { D } ) ) ) = U )
243 ineq2 
 |-  ( t = ( W .(+) ( K ` { D } ) ) -> ( S i^i t ) = ( S i^i ( W .(+) ( K ` { D } ) ) ) )
244 243 eqeq1d 
 |-  ( t = ( W .(+) ( K ` { D } ) ) -> ( ( S i^i t ) = { .0. } <-> ( S i^i ( W .(+) ( K ` { D } ) ) ) = { .0. } ) )
245 oveq2 
 |-  ( t = ( W .(+) ( K ` { D } ) ) -> ( S .(+) t ) = ( S .(+) ( W .(+) ( K ` { D } ) ) ) )
246 245 eqeq1d 
 |-  ( t = ( W .(+) ( K ` { D } ) ) -> ( ( S .(+) t ) = U <-> ( S .(+) ( W .(+) ( K ` { D } ) ) ) = U ) )
247 244 246 anbi12d 
 |-  ( t = ( W .(+) ( K ` { D } ) ) -> ( ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) <-> ( ( S i^i ( W .(+) ( K ` { D } ) ) ) = { .0. } /\ ( S .(+) ( W .(+) ( K ` { D } ) ) ) = U ) ) )
248 247 rspcev 
 |-  ( ( ( W .(+) ( K ` { D } ) ) e. ( SubGrp ` G ) /\ ( ( S i^i ( W .(+) ( K ` { D } ) ) ) = { .0. } /\ ( S .(+) ( W .(+) ( K ` { D } ) ) ) = U ) ) -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) )
249 67 236 242 248 syl12anc 
 |-  ( ph -> E. t e. ( SubGrp ` G ) ( ( S i^i t ) = { .0. } /\ ( S .(+) t ) = U ) )