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 syl5eq
 |-  ( 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 syl5eq
 |-  ( 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 syl5eq
 |-  ( 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 addid2d
 |-  ( 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 ) )