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