Metamath Proof Explorer

Theorem pgpfaclem3

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 ) ) )
Assertion pgpfaclem3 
|- ( 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 wrd0 
 |-  (/) e. Word C
9 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
10 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
11 10 dprd0 
 |-  ( G e. Grp -> ( G dom DProd (/) /\ ( G DProd (/) ) = { ( 0g ` G ) } ) )
12 3 9 11 3syl 
 |-  ( ph -> ( G dom DProd (/) /\ ( G DProd (/) ) = { ( 0g ` G ) } ) )
13 12 adantr 
 |-  ( ( ph /\ ( gEx ` ( G |`s U ) ) = 1 ) -> ( G dom DProd (/) /\ ( G DProd (/) ) = { ( 0g ` G ) } ) )
14 10 subg0cl 
 |-  ( U e. ( SubGrp ` G ) -> ( 0g ` G ) e. U )
15 6 14 syl 
 |-  ( ph -> ( 0g ` G ) e. U )
16 15 adantr 
 |-  ( ( ph /\ ( gEx ` ( G |`s U ) ) = 1 ) -> ( 0g ` G ) e. U )
17 eqid 
 |-  ( G |`s U ) = ( G |`s U )
18 17 subgbas 
 |-  ( U e. ( SubGrp ` G ) -> U = ( Base ` ( G |`s U ) ) )
19 6 18 syl 
 |-  ( ph -> U = ( Base ` ( G |`s U ) ) )
20 19 adantr 
 |-  ( ( ph /\ ( gEx ` ( G |`s U ) ) = 1 ) -> U = ( Base ` ( G |`s U ) ) )
21 17 subggrp 
 |-  ( U e. ( SubGrp ` G ) -> ( G |`s U ) e. Grp )
22 6 21 syl 
 |-  ( ph -> ( G |`s U ) e. Grp )
23 grpmnd 
 |-  ( ( G |`s U ) e. Grp -> ( G |`s U ) e. Mnd )
24 eqid 
 |-  ( Base ` ( G |`s U ) ) = ( Base ` ( G |`s U ) )
25 eqid 
 |-  ( gEx ` ( G |`s U ) ) = ( gEx ` ( G |`s U ) )
26 24 25 gex1 
 |-  ( ( G |`s U ) e. Mnd -> ( ( gEx ` ( G |`s U ) ) = 1 <-> ( Base ` ( G |`s U ) ) ~~ 1o ) )
27 22 23 26 3syl 
 |-  ( ph -> ( ( gEx ` ( G |`s U ) ) = 1 <-> ( Base ` ( G |`s U ) ) ~~ 1o ) )
28 27 biimpa 
 |-  ( ( ph /\ ( gEx ` ( G |`s U ) ) = 1 ) -> ( Base ` ( G |`s U ) ) ~~ 1o )
29 20 28 eqbrtrd 
 |-  ( ( ph /\ ( gEx ` ( G |`s U ) ) = 1 ) -> U ~~ 1o )
30 en1eqsn 
 |-  ( ( ( 0g ` G ) e. U /\ U ~~ 1o ) -> U = { ( 0g ` G ) } )
31 16 29 30 syl2anc 
 |-  ( ( ph /\ ( gEx ` ( G |`s U ) ) = 1 ) -> U = { ( 0g ` G ) } )
32 31 eqeq2d 
 |-  ( ( ph /\ ( gEx ` ( G |`s U ) ) = 1 ) -> ( ( G DProd (/) ) = U <-> ( G DProd (/) ) = { ( 0g ` G ) } ) )
33 32 anbi2d 
 |-  ( ( ph /\ ( gEx ` ( G |`s U ) ) = 1 ) -> ( ( G dom DProd (/) /\ ( G DProd (/) ) = U ) <-> ( G dom DProd (/) /\ ( G DProd (/) ) = { ( 0g ` G ) } ) ) )
34 13 33 mpbird 
 |-  ( ( ph /\ ( gEx ` ( G |`s U ) ) = 1 ) -> ( G dom DProd (/) /\ ( G DProd (/) ) = U ) )
35 breq2 
 |-  ( s = (/) -> ( G dom DProd s <-> G dom DProd (/) ) )
36 oveq2 
 |-  ( s = (/) -> ( G DProd s ) = ( G DProd (/) ) )
37 36 eqeq1d 
 |-  ( s = (/) -> ( ( G DProd s ) = U <-> ( G DProd (/) ) = U ) )
38 35 37 anbi12d 
 |-  ( s = (/) -> ( ( G dom DProd s /\ ( G DProd s ) = U ) <-> ( G dom DProd (/) /\ ( G DProd (/) ) = U ) ) )
39 38 rspcev 
 |-  ( ( (/) e. Word C /\ ( G dom DProd (/) /\ ( G DProd (/) ) = U ) ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )
40 8 34 39 sylancr 
 |-  ( ( ph /\ ( gEx ` ( G |`s U ) ) = 1 ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )
41 17 subgabl 
 |-  ( ( G e. Abel /\ U e. ( SubGrp ` G ) ) -> ( G |`s U ) e. Abel )
42 3 6 41 syl2anc 
 |-  ( ph -> ( G |`s U ) e. Abel )
43 1 subgss 
 |-  ( U e. ( SubGrp ` G ) -> U C_ B )
44 6 43 syl 
 |-  ( ph -> U C_ B )
45 5 44 ssfid 
 |-  ( ph -> U e. Fin )
46 19 45 eqeltrrd 
 |-  ( ph -> ( Base ` ( G |`s U ) ) e. Fin )
47 24 25 gexcl2 
 |-  ( ( ( G |`s U ) e. Grp /\ ( Base ` ( G |`s U ) ) e. Fin ) -> ( gEx ` ( G |`s U ) ) e. NN )
48 22 46 47 syl2anc 
 |-  ( ph -> ( gEx ` ( G |`s U ) ) e. NN )
49 eqid 
 |-  ( od ` ( G |`s U ) ) = ( od ` ( G |`s U ) )
50 24 25 49 gexex 
 |-  ( ( ( G |`s U ) e. Abel /\ ( gEx ` ( G |`s U ) ) e. NN ) -> E. x e. ( Base ` ( G |`s U ) ) ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) )
51 42 48 50 syl2anc 
 |-  ( ph -> E. x e. ( Base ` ( G |`s U ) ) ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) )
52 51 adantr 
 |-  ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) -> E. x e. ( Base ` ( G |`s U ) ) ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) )
53 eqid 
 |-  ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) = ( mrCls ` ( SubGrp ` ( G |`s U ) ) )
54 eqid 
 |-  ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) = ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } )
55 eqid 
 |-  ( 0g ` ( G |`s U ) ) = ( 0g ` ( G |`s U ) )
56 eqid 
 |-  ( LSSum ` ( G |`s U ) ) = ( LSSum ` ( G |`s U ) )
57 subgpgp 
 |-  ( ( P pGrp G /\ U e. ( SubGrp ` G ) ) -> P pGrp ( G |`s U ) )
58 4 6 57 syl2anc 
 |-  ( ph -> P pGrp ( G |`s U ) )
59 58 ad2antrr 
 |-  ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) -> P pGrp ( G |`s U ) )
60 42 ad2antrr 
 |-  ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) -> ( G |`s U ) e. Abel )
61 46 ad2antrr 
 |-  ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) -> ( Base ` ( G |`s U ) ) e. Fin )
62 simprr 
 |-  ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) -> ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) )
63 simprl 
 |-  ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) -> x e. ( Base ` ( G |`s U ) ) )
64 53 54 24 49 25 55 56 59 60 61 62 63 pgpfac1 
 |-  ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) -> E. w e. ( SubGrp ` ( G |`s U ) ) ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) )
65 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> G e. Abel )
66 4 ad3antrrr 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> P pGrp G )
67 5 ad3antrrr 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> B e. Fin )
68 6 ad3antrrr 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> U e. ( SubGrp ` G ) )
69 7 ad3antrrr 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> A. t e. ( SubGrp ` G ) ( t C. U -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) )
70 simpllr 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> ( gEx ` ( G |`s U ) ) =/= 1 )
71 simplrl 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> x e. ( Base ` ( G |`s U ) ) )
72 68 18 syl 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> U = ( Base ` ( G |`s U ) ) )
73 71 72 eleqtrrd 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> x e. U )
74 simplrr 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) )
75 simprl 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> w e. ( SubGrp ` ( G |`s U ) ) )
76 simprrl 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } )
77 simprrr 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) )
78 77 72 eqtr4d 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = U )
79 1 2 65 66 67 68 69 17 53 49 25 55 56 70 73 74 75 76 78 pgpfaclem2 
 |-  ( ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) /\ ( w e. ( SubGrp ` ( G |`s U ) ) /\ ( ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) i^i w ) = { ( 0g ` ( G |`s U ) ) } /\ ( ( ( mrCls ` ( SubGrp ` ( G |`s U ) ) ) ` { x } ) ( LSSum ` ( G |`s U ) ) w ) = ( Base ` ( G |`s U ) ) ) ) ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )
80 64 79 rexlimddv 
 |-  ( ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) /\ ( x e. ( Base ` ( G |`s U ) ) /\ ( ( od ` ( G |`s U ) ) ` x ) = ( gEx ` ( G |`s U ) ) ) ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )
81 52 80 rexlimddv 
 |-  ( ( ph /\ ( gEx ` ( G |`s U ) ) =/= 1 ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )
82 40 81 pm2.61dane 
 |-  ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )