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

Metamath Proof Explorer

Theorem pgpfaclem1

Description: Lemma for pgpfac . (Contributed by Mario Carneiro, 27-Apr-2016) (Revised by Mario Carneiro, 3-May-2016)

Ref Expression
Hypotheses pgpfac.b 
|- B = ( Base ` G )
pgpfac.c 
|- C = { r e. ( SubGrp ` G ) | ( G |`s r ) e. ( CycGrp i^i ran pGrp ) }
pgpfac.g 
|- ( ph -> G e. Abel )
pgpfac.p 
|- ( ph -> P pGrp G )
pgpfac.f 
|- ( ph -> B e. Fin )
pgpfac.u 
|- ( ph -> U e. ( SubGrp ` G ) )
pgpfac.a 
|- ( ph -> A. t e. ( SubGrp ` G ) ( t C. U -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) )
pgpfac.h 
|- H = ( G |`s U )
pgpfac.k 
|- K = ( mrCls ` ( SubGrp ` H ) )
pgpfac.o 
|- O = ( od ` H )
pgpfac.e 
|- E = ( gEx ` H )
pgpfac.0 
|- .0. = ( 0g ` H )
pgpfac.l 
|- .(+) = ( LSSum ` H )
pgpfac.1 
|- ( ph -> E =/= 1 )
pgpfac.x 
|- ( ph -> X e. U )
pgpfac.oe 
|- ( ph -> ( O ` X ) = E )
pgpfac.w 
|- ( ph -> W e. ( SubGrp ` H ) )
pgpfac.i 
|- ( ph -> ( ( K ` { X } ) i^i W ) = { .0. } )
pgpfac.s 
|- ( ph -> ( ( K ` { X } ) .(+) W ) = U )
pgpfac.2 
|- ( ph -> S e. Word C )
pgpfac.4 
|- ( ph -> G dom DProd S )
pgpfac.5 
|- ( ph -> ( G DProd S ) = W )
pgpfac.t 
|- T = ( S ++ <" ( K ` { X } ) "> )
Assertion pgpfaclem1 
|- ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )

Proof

Step Hyp Ref Expression
1 pgpfac.b 
 |-  B = ( Base ` G )
2 pgpfac.c 
 |-  C = { r e. ( SubGrp ` G ) | ( G |`s r ) e. ( CycGrp i^i ran pGrp ) }
3 pgpfac.g 
 |-  ( ph -> G e. Abel )
4 pgpfac.p 
 |-  ( ph -> P pGrp G )
5 pgpfac.f 
 |-  ( ph -> B e. Fin )
6 pgpfac.u 
 |-  ( ph -> U e. ( SubGrp ` G ) )
7 pgpfac.a 
 |-  ( ph -> A. t e. ( SubGrp ` G ) ( t C. U -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) )
8 pgpfac.h 
 |-  H = ( G |`s U )
9 pgpfac.k 
 |-  K = ( mrCls ` ( SubGrp ` H ) )
10 pgpfac.o 
 |-  O = ( od ` H )
11 pgpfac.e 
 |-  E = ( gEx ` H )
12 pgpfac.0 
 |-  .0. = ( 0g ` H )
13 pgpfac.l 
 |-  .(+) = ( LSSum ` H )
14 pgpfac.1 
 |-  ( ph -> E =/= 1 )
15 pgpfac.x 
 |-  ( ph -> X e. U )
16 pgpfac.oe 
 |-  ( ph -> ( O ` X ) = E )
17 pgpfac.w 
 |-  ( ph -> W e. ( SubGrp ` H ) )
18 pgpfac.i 
 |-  ( ph -> ( ( K ` { X } ) i^i W ) = { .0. } )
19 pgpfac.s 
 |-  ( ph -> ( ( K ` { X } ) .(+) W ) = U )
20 pgpfac.2 
 |-  ( ph -> S e. Word C )
21 pgpfac.4 
 |-  ( ph -> G dom DProd S )
22 pgpfac.5 
 |-  ( ph -> ( G DProd S ) = W )
23 pgpfac.t 
 |-  T = ( S ++ <" ( K ` { X } ) "> )
24 8 subggrp 
 |-  ( U e. ( SubGrp ` G ) -> H e. Grp )
25 6 24 syl 
 |-  ( ph -> H e. Grp )
26 eqid 
 |-  ( Base ` H ) = ( Base ` H )
27 26 subgacs 
 |-  ( H e. Grp -> ( SubGrp ` H ) e. ( ACS ` ( Base ` H ) ) )
28 25 27 syl 
 |-  ( ph -> ( SubGrp ` H ) e. ( ACS ` ( Base ` H ) ) )
29 28 acsmred 
 |-  ( ph -> ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) )
30 8 subgbas 
 |-  ( U e. ( SubGrp ` G ) -> U = ( Base ` H ) )
31 6 30 syl 
 |-  ( ph -> U = ( Base ` H ) )
32 15 31 eleqtrd 
 |-  ( ph -> X e. ( Base ` H ) )
33 9 mrcsncl 
 |-  ( ( ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) /\ X e. ( Base ` H ) ) -> ( K ` { X } ) e. ( SubGrp ` H ) )
34 29 32 33 syl2anc 
 |-  ( ph -> ( K ` { X } ) e. ( SubGrp ` H ) )
35 8 subsubg 
 |-  ( U e. ( SubGrp ` G ) -> ( ( K ` { X } ) e. ( SubGrp ` H ) <-> ( ( K ` { X } ) e. ( SubGrp ` G ) /\ ( K ` { X } ) C_ U ) ) )
36 6 35 syl 
 |-  ( ph -> ( ( K ` { X } ) e. ( SubGrp ` H ) <-> ( ( K ` { X } ) e. ( SubGrp ` G ) /\ ( K ` { X } ) C_ U ) ) )
37 34 36 mpbid 
 |-  ( ph -> ( ( K ` { X } ) e. ( SubGrp ` G ) /\ ( K ` { X } ) C_ U ) )
38 37 simpld 
 |-  ( ph -> ( K ` { X } ) e. ( SubGrp ` G ) )
39 8 oveq1i 
 |-  ( H |`s ( K ` { X } ) ) = ( ( G |`s U ) |`s ( K ` { X } ) )
40 37 simprd 
 |-  ( ph -> ( K ` { X } ) C_ U )
41 ressabs 
 |-  ( ( U e. ( SubGrp ` G ) /\ ( K ` { X } ) C_ U ) -> ( ( G |`s U ) |`s ( K ` { X } ) ) = ( G |`s ( K ` { X } ) ) )
42 6 40 41 syl2anc 
 |-  ( ph -> ( ( G |`s U ) |`s ( K ` { X } ) ) = ( G |`s ( K ` { X } ) ) )
43 39 42 eqtrid 
 |-  ( ph -> ( H |`s ( K ` { X } ) ) = ( G |`s ( K ` { X } ) ) )
44 26 9 cycsubgcyg2 
 |-  ( ( H e. Grp /\ X e. ( Base ` H ) ) -> ( H |`s ( K ` { X } ) ) e. CycGrp )
45 25 32 44 syl2anc 
 |-  ( ph -> ( H |`s ( K ` { X } ) ) e. CycGrp )
46 43 45 eqeltrrd 
 |-  ( ph -> ( G |`s ( K ` { X } ) ) e. CycGrp )
47 pgpprm 
 |-  ( P pGrp G -> P e. Prime )
48 4 47 syl 
 |-  ( ph -> P e. Prime )
49 subgpgp 
 |-  ( ( P pGrp G /\ ( K ` { X } ) e. ( SubGrp ` G ) ) -> P pGrp ( G |`s ( K ` { X } ) ) )
50 4 38 49 syl2anc 
 |-  ( ph -> P pGrp ( G |`s ( K ` { X } ) ) )
51 brelrng 
 |-  ( ( P e. Prime /\ ( G |`s ( K ` { X } ) ) e. CycGrp /\ P pGrp ( G |`s ( K ` { X } ) ) ) -> ( G |`s ( K ` { X } ) ) e. ran pGrp )
52 48 46 50 51 syl3anc 
 |-  ( ph -> ( G |`s ( K ` { X } ) ) e. ran pGrp )
53 46 52 elind 
 |-  ( ph -> ( G |`s ( K ` { X } ) ) e. ( CycGrp i^i ran pGrp ) )
54 oveq2 
 |-  ( r = ( K ` { X } ) -> ( G |`s r ) = ( G |`s ( K ` { X } ) ) )
55 54 eleq1d 
 |-  ( r = ( K ` { X } ) -> ( ( G |`s r ) e. ( CycGrp i^i ran pGrp ) <-> ( G |`s ( K ` { X } ) ) e. ( CycGrp i^i ran pGrp ) ) )
56 55 2 elrab2 
 |-  ( ( K ` { X } ) e. C <-> ( ( K ` { X } ) e. ( SubGrp ` G ) /\ ( G |`s ( K ` { X } ) ) e. ( CycGrp i^i ran pGrp ) ) )
57 38 53 56 sylanbrc 
 |-  ( ph -> ( K ` { X } ) e. C )
58 23 20 57 cats1cld 
 |-  ( ph -> T e. Word C )
59 wrdf 
 |-  ( T e. Word C -> T : ( 0 ..^ ( # ` T ) ) --> C )
60 58 59 syl 
 |-  ( ph -> T : ( 0 ..^ ( # ` T ) ) --> C )
61 2 ssrab3 
 |-  C C_ ( SubGrp ` G )
62 fss 
 |-  ( ( T : ( 0 ..^ ( # ` T ) ) --> C /\ C C_ ( SubGrp ` G ) ) -> T : ( 0 ..^ ( # ` T ) ) --> ( SubGrp ` G ) )
63 60 61 62 sylancl 
 |-  ( ph -> T : ( 0 ..^ ( # ` T ) ) --> ( SubGrp ` G ) )
64 lencl 
 |-  ( S e. Word C -> ( # ` S ) e. NN0 )
65 20 64 syl 
 |-  ( ph -> ( # ` S ) e. NN0 )
66 65 nn0zd 
 |-  ( ph -> ( # ` S ) e. ZZ )
67 fzosn 
 |-  ( ( # ` S ) e. ZZ -> ( ( # ` S ) ..^ ( ( # ` S ) + 1 ) ) = { ( # ` S ) } )
68 66 67 syl 
 |-  ( ph -> ( ( # ` S ) ..^ ( ( # ` S ) + 1 ) ) = { ( # ` S ) } )
69 68 ineq2d 
 |-  ( ph -> ( ( 0 ..^ ( # ` S ) ) i^i ( ( # ` S ) ..^ ( ( # ` S ) + 1 ) ) ) = ( ( 0 ..^ ( # ` S ) ) i^i { ( # ` S ) } ) )
70 fzodisj 
 |-  ( ( 0 ..^ ( # ` S ) ) i^i ( ( # ` S ) ..^ ( ( # ` S ) + 1 ) ) ) = (/)
71 69 70 eqtr3di 
 |-  ( ph -> ( ( 0 ..^ ( # ` S ) ) i^i { ( # ` S ) } ) = (/) )
72 23 fveq2i 
 |-  ( # ` T ) = ( # ` ( S ++ <" ( K ` { X } ) "> ) )
73 57 s1cld 
 |-  ( ph -> <" ( K ` { X } ) "> e. Word C )
74 ccatlen 
 |-  ( ( S e. Word C /\ <" ( K ` { X } ) "> e. Word C ) -> ( # ` ( S ++ <" ( K ` { X } ) "> ) ) = ( ( # ` S ) + ( # ` <" ( K ` { X } ) "> ) ) )
75 20 73 74 syl2anc 
 |-  ( ph -> ( # ` ( S ++ <" ( K ` { X } ) "> ) ) = ( ( # ` S ) + ( # ` <" ( K ` { X } ) "> ) ) )
76 72 75 eqtrid 
 |-  ( ph -> ( # ` T ) = ( ( # ` S ) + ( # ` <" ( K ` { X } ) "> ) ) )
77 s1len 
 |-  ( # ` <" ( K ` { X } ) "> ) = 1
78 77 oveq2i 
 |-  ( ( # ` S ) + ( # ` <" ( K ` { X } ) "> ) ) = ( ( # ` S ) + 1 )
79 76 78 eqtrdi 
 |-  ( ph -> ( # ` T ) = ( ( # ` S ) + 1 ) )
80 79 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` T ) ) = ( 0 ..^ ( ( # ` S ) + 1 ) ) )
81 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
82 65 81 eleqtrdi 
 |-  ( ph -> ( # ` S ) e. ( ZZ>= ` 0 ) )
83 fzosplitsn 
 |-  ( ( # ` S ) e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( ( # ` S ) + 1 ) ) = ( ( 0 ..^ ( # ` S ) ) u. { ( # ` S ) } ) )
84 82 83 syl 
 |-  ( ph -> ( 0 ..^ ( ( # ` S ) + 1 ) ) = ( ( 0 ..^ ( # ` S ) ) u. { ( # ` S ) } ) )
85 80 84 eqtrd 
 |-  ( ph -> ( 0 ..^ ( # ` T ) ) = ( ( 0 ..^ ( # ` S ) ) u. { ( # ` S ) } ) )
86 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
87 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
88 cats1un 
 |-  ( ( S e. Word C /\ ( K ` { X } ) e. C ) -> ( S ++ <" ( K ` { X } ) "> ) = ( S u. { <. ( # ` S ) , ( K ` { X } ) >. } ) )
89 20 57 88 syl2anc 
 |-  ( ph -> ( S ++ <" ( K ` { X } ) "> ) = ( S u. { <. ( # ` S ) , ( K ` { X } ) >. } ) )
90 23 89 eqtrid 
 |-  ( ph -> T = ( S u. { <. ( # ` S ) , ( K ` { X } ) >. } ) )
91 90 reseq1d 
 |-  ( ph -> ( T |` ( 0 ..^ ( # ` S ) ) ) = ( ( S u. { <. ( # ` S ) , ( K ` { X } ) >. } ) |` ( 0 ..^ ( # ` S ) ) ) )
92 wrdfn 
 |-  ( S e. Word C -> S Fn ( 0 ..^ ( # ` S ) ) )
93 20 92 syl 
 |-  ( ph -> S Fn ( 0 ..^ ( # ` S ) ) )
94 fzonel 
 |-  -. ( # ` S ) e. ( 0 ..^ ( # ` S ) )
95 fsnunres 
 |-  ( ( S Fn ( 0 ..^ ( # ` S ) ) /\ -. ( # ` S ) e. ( 0 ..^ ( # ` S ) ) ) -> ( ( S u. { <. ( # ` S ) , ( K ` { X } ) >. } ) |` ( 0 ..^ ( # ` S ) ) ) = S )
96 93 94 95 sylancl 
 |-  ( ph -> ( ( S u. { <. ( # ` S ) , ( K ` { X } ) >. } ) |` ( 0 ..^ ( # ` S ) ) ) = S )
97 91 96 eqtrd 
 |-  ( ph -> ( T |` ( 0 ..^ ( # ` S ) ) ) = S )
98 21 97 breqtrrd 
 |-  ( ph -> G dom DProd ( T |` ( 0 ..^ ( # ` S ) ) ) )
99 fvex 
 |-  ( # ` S ) e. _V
100 dprdsn 
 |-  ( ( ( # ` S ) e. _V /\ ( K ` { X } ) e. ( SubGrp ` G ) ) -> ( G dom DProd { <. ( # ` S ) , ( K ` { X } ) >. } /\ ( G DProd { <. ( # ` S ) , ( K ` { X } ) >. } ) = ( K ` { X } ) ) )
101 99 38 100 sylancr 
 |-  ( ph -> ( G dom DProd { <. ( # ` S ) , ( K ` { X } ) >. } /\ ( G DProd { <. ( # ` S ) , ( K ` { X } ) >. } ) = ( K ` { X } ) ) )
102 101 simpld 
 |-  ( ph -> G dom DProd { <. ( # ` S ) , ( K ` { X } ) >. } )
103 wrdfn 
 |-  ( T e. Word C -> T Fn ( 0 ..^ ( # ` T ) ) )
104 58 103 syl 
 |-  ( ph -> T Fn ( 0 ..^ ( # ` T ) ) )
105 ssun2 
 |-  { ( # ` S ) } C_ ( ( 0 ..^ ( # ` S ) ) u. { ( # ` S ) } )
106 99 snss 
 |-  ( ( # ` S ) e. ( ( 0 ..^ ( # ` S ) ) u. { ( # ` S ) } ) <-> { ( # ` S ) } C_ ( ( 0 ..^ ( # ` S ) ) u. { ( # ` S ) } ) )
107 105 106 mpbir 
 |-  ( # ` S ) e. ( ( 0 ..^ ( # ` S ) ) u. { ( # ` S ) } )
108 107 85 eleqtrrid 
 |-  ( ph -> ( # ` S ) e. ( 0 ..^ ( # ` T ) ) )
109 fnressn 
 |-  ( ( T Fn ( 0 ..^ ( # ` T ) ) /\ ( # ` S ) e. ( 0 ..^ ( # ` T ) ) ) -> ( T |` { ( # ` S ) } ) = { <. ( # ` S ) , ( T ` ( # ` S ) ) >. } )
110 104 108 109 syl2anc 
 |-  ( ph -> ( T |` { ( # ` S ) } ) = { <. ( # ` S ) , ( T ` ( # ` S ) ) >. } )
111 23 fveq1i 
 |-  ( T ` ( # ` S ) ) = ( ( S ++ <" ( K ` { X } ) "> ) ` ( # ` S ) )
112 65 nn0cnd 
 |-  ( ph -> ( # ` S ) e. CC )
113 112 addlidd 
 |-  ( ph -> ( 0 + ( # ` S ) ) = ( # ` S ) )
114 113 fveq2d 
 |-  ( ph -> ( ( S ++ <" ( K ` { X } ) "> ) ` ( 0 + ( # ` S ) ) ) = ( ( S ++ <" ( K ` { X } ) "> ) ` ( # ` S ) ) )
115 111 114 eqtr4id 
 |-  ( ph -> ( T ` ( # ` S ) ) = ( ( S ++ <" ( K ` { X } ) "> ) ` ( 0 + ( # ` S ) ) ) )
116 1nn 
 |-  1 e. NN
117 77 116 eqeltri 
 |-  ( # ` <" ( K ` { X } ) "> ) e. NN
118 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` <" ( K ` { X } ) "> ) ) <-> ( # ` <" ( K ` { X } ) "> ) e. NN )
119 117 118 mpbir 
 |-  0 e. ( 0 ..^ ( # ` <" ( K ` { X } ) "> ) )
120 119 a1i 
 |-  ( ph -> 0 e. ( 0 ..^ ( # ` <" ( K ` { X } ) "> ) ) )
121 ccatval3 
 |-  ( ( S e. Word C /\ <" ( K ` { X } ) "> e. Word C /\ 0 e. ( 0 ..^ ( # ` <" ( K ` { X } ) "> ) ) ) -> ( ( S ++ <" ( K ` { X } ) "> ) ` ( 0 + ( # ` S ) ) ) = ( <" ( K ` { X } ) "> ` 0 ) )
122 20 73 120 121 syl3anc 
 |-  ( ph -> ( ( S ++ <" ( K ` { X } ) "> ) ` ( 0 + ( # ` S ) ) ) = ( <" ( K ` { X } ) "> ` 0 ) )
123 fvex 
 |-  ( K ` { X } ) e. _V
124 s1fv 
 |-  ( ( K ` { X } ) e. _V -> ( <" ( K ` { X } ) "> ` 0 ) = ( K ` { X } ) )
125 123 124 mp1i 
 |-  ( ph -> ( <" ( K ` { X } ) "> ` 0 ) = ( K ` { X } ) )
126 115 122 125 3eqtrd 
 |-  ( ph -> ( T ` ( # ` S ) ) = ( K ` { X } ) )
127 126 opeq2d 
 |-  ( ph -> <. ( # ` S ) , ( T ` ( # ` S ) ) >. = <. ( # ` S ) , ( K ` { X } ) >. )
128 127 sneqd 
 |-  ( ph -> { <. ( # ` S ) , ( T ` ( # ` S ) ) >. } = { <. ( # ` S ) , ( K ` { X } ) >. } )
129 110 128 eqtrd 
 |-  ( ph -> ( T |` { ( # ` S ) } ) = { <. ( # ` S ) , ( K ` { X } ) >. } )
130 102 129 breqtrrd 
 |-  ( ph -> G dom DProd ( T |` { ( # ` S ) } ) )
131 dprdsubg 
 |-  ( G dom DProd ( T |` ( 0 ..^ ( # ` S ) ) ) -> ( G DProd ( T |` ( 0 ..^ ( # ` S ) ) ) ) e. ( SubGrp ` G ) )
132 98 131 syl 
 |-  ( ph -> ( G DProd ( T |` ( 0 ..^ ( # ` S ) ) ) ) e. ( SubGrp ` G ) )
133 dprdsubg 
 |-  ( G dom DProd ( T |` { ( # ` S ) } ) -> ( G DProd ( T |` { ( # ` S ) } ) ) e. ( SubGrp ` G ) )
134 130 133 syl 
 |-  ( ph -> ( G DProd ( T |` { ( # ` S ) } ) ) e. ( SubGrp ` G ) )
135 86 3 132 134 ablcntzd 
 |-  ( ph -> ( G DProd ( T |` ( 0 ..^ ( # ` S ) ) ) ) C_ ( ( Cntz ` G ) ` ( G DProd ( T |` { ( # ` S ) } ) ) ) )
136 97 oveq2d 
 |-  ( ph -> ( G DProd ( T |` ( 0 ..^ ( # ` S ) ) ) ) = ( G DProd S ) )
137 136 22 eqtrd 
 |-  ( ph -> ( G DProd ( T |` ( 0 ..^ ( # ` S ) ) ) ) = W )
138 129 oveq2d 
 |-  ( ph -> ( G DProd ( T |` { ( # ` S ) } ) ) = ( G DProd { <. ( # ` S ) , ( K ` { X } ) >. } ) )
139 101 simprd 
 |-  ( ph -> ( G DProd { <. ( # ` S ) , ( K ` { X } ) >. } ) = ( K ` { X } ) )
140 138 139 eqtrd 
 |-  ( ph -> ( G DProd ( T |` { ( # ` S ) } ) ) = ( K ` { X } ) )
141 137 140 ineq12d 
 |-  ( ph -> ( ( G DProd ( T |` ( 0 ..^ ( # ` S ) ) ) ) i^i ( G DProd ( T |` { ( # ` S ) } ) ) ) = ( W i^i ( K ` { X } ) ) )
142 incom 
 |-  ( W i^i ( K ` { X } ) ) = ( ( K ` { X } ) i^i W )
143 141 142 eqtrdi 
 |-  ( ph -> ( ( G DProd ( T |` ( 0 ..^ ( # ` S ) ) ) ) i^i ( G DProd ( T |` { ( # ` S ) } ) ) ) = ( ( K ` { X } ) i^i W ) )
144 8 87 subg0 
 |-  ( U e. ( SubGrp ` G ) -> ( 0g ` G ) = ( 0g ` H ) )
145 6 144 syl 
 |-  ( ph -> ( 0g ` G ) = ( 0g ` H ) )
146 145 12 eqtr4di 
 |-  ( ph -> ( 0g ` G ) = .0. )
147 146 sneqd 
 |-  ( ph -> { ( 0g ` G ) } = { .0. } )
148 18 143 147 3eqtr4d 
 |-  ( ph -> ( ( G DProd ( T |` ( 0 ..^ ( # ` S ) ) ) ) i^i ( G DProd ( T |` { ( # ` S ) } ) ) ) = { ( 0g ` G ) } )
149 63 71 85 86 87 98 130 135 148 dmdprdsplit2 
 |-  ( ph -> G dom DProd T )
150 eqid 
 |-  ( LSSum ` G ) = ( LSSum ` G )
151 63 71 85 150 149 dprdsplit 
 |-  ( ph -> ( G DProd T ) = ( ( G DProd ( T |` ( 0 ..^ ( # ` S ) ) ) ) ( LSSum ` G ) ( G DProd ( T |` { ( # ` S ) } ) ) ) )
152 137 140 oveq12d 
 |-  ( ph -> ( ( G DProd ( T |` ( 0 ..^ ( # ` S ) ) ) ) ( LSSum ` G ) ( G DProd ( T |` { ( # ` S ) } ) ) ) = ( W ( LSSum ` G ) ( K ` { X } ) ) )
153 137 132 eqeltrrd 
 |-  ( ph -> W e. ( SubGrp ` G ) )
154 150 lsmcom 
 |-  ( ( G e. Abel /\ W e. ( SubGrp ` G ) /\ ( K ` { X } ) e. ( SubGrp ` G ) ) -> ( W ( LSSum ` G ) ( K ` { X } ) ) = ( ( K ` { X } ) ( LSSum ` G ) W ) )
155 3 153 38 154 syl3anc 
 |-  ( ph -> ( W ( LSSum ` G ) ( K ` { X } ) ) = ( ( K ` { X } ) ( LSSum ` G ) W ) )
156 151 152 155 3eqtrd 
 |-  ( ph -> ( G DProd T ) = ( ( K ` { X } ) ( LSSum ` G ) W ) )
157 26 subgss 
 |-  ( W e. ( SubGrp ` H ) -> W C_ ( Base ` H ) )
158 17 157 syl 
 |-  ( ph -> W C_ ( Base ` H ) )
159 158 31 sseqtrrd 
 |-  ( ph -> W C_ U )
160 8 150 13 subglsm 
 |-  ( ( U e. ( SubGrp ` G ) /\ ( K ` { X } ) C_ U /\ W C_ U ) -> ( ( K ` { X } ) ( LSSum ` G ) W ) = ( ( K ` { X } ) .(+) W ) )
161 6 40 159 160 syl3anc 
 |-  ( ph -> ( ( K ` { X } ) ( LSSum ` G ) W ) = ( ( K ` { X } ) .(+) W ) )
162 156 161 19 3eqtrd 
 |-  ( ph -> ( G DProd T ) = U )
163 breq2 
 |-  ( s = T -> ( G dom DProd s <-> G dom DProd T ) )
164 oveq2 
 |-  ( s = T -> ( G DProd s ) = ( G DProd T ) )
165 164 eqeq1d 
 |-  ( s = T -> ( ( G DProd s ) = U <-> ( G DProd T ) = U ) )
166 163 165 anbi12d 
 |-  ( s = T -> ( ( G dom DProd s /\ ( G DProd s ) = U ) <-> ( G dom DProd T /\ ( G DProd T ) = U ) ) )
167 166 rspcev 
 |-  ( ( T e. Word C /\ ( G dom DProd T /\ ( G DProd T ) = U ) ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )
168 58 149 162 167 syl12anc 
 |-  ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )