Theorem pgpfaclem2

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 )
Assertion	pgpfaclem2	|- ( 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	8	subsubg	|- ( U e. ( SubGrp ` G ) -> ( W e. ( SubGrp ` H ) <-> ( W e. ( SubGrp ` G ) /\ W C_ U ) ) )
21	6 20	syl	|- ( ph -> ( W e. ( SubGrp ` H ) <-> ( W e. ( SubGrp ` G ) /\ W C_ U ) ) )
22	17 21	mpbid	|- ( ph -> ( W e. ( SubGrp ` G ) /\ W C_ U ) )
23	22	simprd	|- ( ph -> W C_ U )
24	1	subgss	|- ( U e. ( SubGrp ` G ) -> U C_ B )
25	6 24	syl	|- ( ph -> U C_ B )
26	5 25	ssfid	|- ( ph -> U e. Fin )
27	26 23	ssfid	|- ( ph -> W e. Fin )
28		hashcl	|- ( W e. Fin -> ( # ` W ) e. NN0 )
29	27 28	syl	|- ( ph -> ( # ` W ) e. NN0 )
30	29	nn0red	|- ( ph -> ( # ` W ) e. RR )
31	12	fvexi	|- .0. e. _V
32		hashsng	|- ( .0. e. _V -> ( # ` { .0. } ) = 1 )
33	31 32	ax-mp	|- ( # ` { .0. } ) = 1
34		subgrcl	|- ( W e. ( SubGrp ` H ) -> H e. Grp )
35		eqid	|- ( Base ` H ) = ( Base ` H )
36	35	subgacs	|- ( H e. Grp -> ( SubGrp ` H ) e. ( ACS ` ( Base ` H ) ) )
37		acsmre	|- ( ( SubGrp ` H ) e. ( ACS ` ( Base ` H ) ) -> ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) )
38	17 34 36 37	4syl	|- ( ph -> ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) )
39	38 9	mrcssvd	|- ( ph -> ( K ` { X } ) C_ ( Base ` H ) )
40	8	subgbas	|- ( U e. ( SubGrp ` G ) -> U = ( Base ` H ) )
41	6 40	syl	|- ( ph -> U = ( Base ` H ) )
42	39 41	sseqtrrd	|- ( ph -> ( K ` { X } ) C_ U )
43	26 42	ssfid	|- ( ph -> ( K ` { X } ) e. Fin )
44	15 41	eleqtrd	|- ( ph -> X e. ( Base ` H ) )
45	9	mrcsncl	|- ( ( ( SubGrp ` H ) e. ( Moore ` ( Base ` H ) ) /\ X e. ( Base ` H ) ) -> ( K ` { X } ) e. ( SubGrp ` H ) )
46	38 44 45	syl2anc	|- ( ph -> ( K ` { X } ) e. ( SubGrp ` H ) )
47	12	subg0cl	|- ( ( K ` { X } ) e. ( SubGrp ` H ) -> .0. e. ( K ` { X } ) )
48	46 47	syl	|- ( ph -> .0. e. ( K ` { X } ) )
49	48	snssd	|- ( ph -> { .0. } C_ ( K ` { X } ) )
50	44	snssd	|- ( ph -> { X } C_ ( Base ` H ) )
51	38 9 50	mrcssidd	|- ( ph -> { X } C_ ( K ` { X } ) )
52		snssg	|- ( X e. U -> ( X e. ( K ` { X } ) <-> { X } C_ ( K ` { X } ) ) )
53	15 52	syl	|- ( ph -> ( X e. ( K ` { X } ) <-> { X } C_ ( K ` { X } ) ) )
54	51 53	mpbird	|- ( ph -> X e. ( K ` { X } ) )
55	16 14	eqnetrd	|- ( ph -> ( O ` X ) =/= 1 )
56	10 12	od1	|- ( H e. Grp -> ( O ` .0. ) = 1 )
57	17 34 56	3syl	|- ( ph -> ( O ` .0. ) = 1 )
58		elsni	|- ( X e. { .0. } -> X = .0. )
59	58	fveqeq2d	|- ( X e. { .0. } -> ( ( O ` X ) = 1 <-> ( O ` .0. ) = 1 ) )
60	57 59	syl5ibrcom	|- ( ph -> ( X e. { .0. } -> ( O ` X ) = 1 ) )
61	60	necon3ad	|- ( ph -> ( ( O ` X ) =/= 1 -> -. X e. { .0. } ) )
62	55 61	mpd	|- ( ph -> -. X e. { .0. } )
63	49 54 62	ssnelpssd	|- ( ph -> { .0. } C. ( K ` { X } ) )
64		php3	|- ( ( ( K ` { X } ) e. Fin /\ { .0. } C. ( K ` { X } ) ) -> { .0. } ~< ( K ` { X } ) )
65	43 63 64	syl2anc	|- ( ph -> { .0. } ~< ( K ` { X } ) )
66		snfi	|- { .0. } e. Fin
67		hashsdom	|- ( ( { .0. } e. Fin /\ ( K ` { X } ) e. Fin ) -> ( ( # ` { .0. } ) < ( # ` ( K ` { X } ) ) <-> { .0. } ~< ( K ` { X } ) ) )
68	66 43 67	sylancr	|- ( ph -> ( ( # ` { .0. } ) < ( # ` ( K ` { X } ) ) <-> { .0. } ~< ( K ` { X } ) ) )
69	65 68	mpbird	|- ( ph -> ( # ` { .0. } ) < ( # ` ( K ` { X } ) ) )
70	33 69	eqbrtrrid	|- ( ph -> 1 < ( # ` ( K ` { X } ) ) )
71		1red	|- ( ph -> 1 e. RR )
72		hashcl	|- ( ( K ` { X } ) e. Fin -> ( # ` ( K ` { X } ) ) e. NN0 )
73	43 72	syl	|- ( ph -> ( # ` ( K ` { X } ) ) e. NN0 )
74	73	nn0red	|- ( ph -> ( # ` ( K ` { X } ) ) e. RR )
75	12	subg0cl	|- ( W e. ( SubGrp ` H ) -> .0. e. W )
76		ne0i	|- ( .0. e. W -> W =/= (/) )
77	17 75 76	3syl	|- ( ph -> W =/= (/) )
78		hashnncl	|- ( W e. Fin -> ( ( # ` W ) e. NN <-> W =/= (/) ) )
79	27 78	syl	|- ( ph -> ( ( # ` W ) e. NN <-> W =/= (/) ) )
80	77 79	mpbird	|- ( ph -> ( # ` W ) e. NN )
81	80	nngt0d	|- ( ph -> 0 < ( # ` W ) )
82		ltmul1	|- ( ( 1 e. RR /\ ( # ` ( K ` { X } ) ) e. RR /\ ( ( # ` W ) e. RR /\ 0 < ( # ` W ) ) ) -> ( 1 < ( # ` ( K ` { X } ) ) <-> ( 1 x. ( # ` W ) ) < ( ( # ` ( K ` { X } ) ) x. ( # ` W ) ) ) )
83	71 74 30 81 82	syl112anc	|- ( ph -> ( 1 < ( # ` ( K ` { X } ) ) <-> ( 1 x. ( # ` W ) ) < ( ( # ` ( K ` { X } ) ) x. ( # ` W ) ) ) )
84	70 83	mpbid	|- ( ph -> ( 1 x. ( # ` W ) ) < ( ( # ` ( K ` { X } ) ) x. ( # ` W ) ) )
85	30	recnd	|- ( ph -> ( # ` W ) e. CC )
86	85	mullidd	|- ( ph -> ( 1 x. ( # ` W ) ) = ( # ` W ) )
87		eqid	|- ( Cntz ` H ) = ( Cntz ` H )
88	8	subgabl	|- ( ( G e. Abel /\ U e. ( SubGrp ` G ) ) -> H e. Abel )
89	3 6 88	syl2anc	|- ( ph -> H e. Abel )
90	87 89 46 17	ablcntzd	|- ( ph -> ( K ` { X } ) C_ ( ( Cntz ` H ) ` W ) )
91	13 12 87 46 17 18 90 43 27	lsmhash	|- ( ph -> ( # ` ( ( K ` { X } ) .(+) W ) ) = ( ( # ` ( K ` { X } ) ) x. ( # ` W ) ) )
92	19	fveq2d	|- ( ph -> ( # ` ( ( K ` { X } ) .(+) W ) ) = ( # ` U ) )
93	91 92	eqtr3d	|- ( ph -> ( ( # ` ( K ` { X } ) ) x. ( # ` W ) ) = ( # ` U ) )
94	84 86 93	3brtr3d	|- ( ph -> ( # ` W ) < ( # ` U ) )
95	30 94	ltned	|- ( ph -> ( # ` W ) =/= ( # ` U ) )
96		fveq2	|- ( W = U -> ( # ` W ) = ( # ` U ) )
97	96	necon3i	|- ( ( # ` W ) =/= ( # ` U ) -> W =/= U )
98	95 97	syl	|- ( ph -> W =/= U )
99		df-pss	|- ( W C. U <-> ( W C_ U /\ W =/= U ) )
100	23 98 99	sylanbrc	|- ( ph -> W C. U )
101		psseq1	|- ( t = W -> ( t C. U <-> W C. U ) )
102		eqeq2	|- ( t = W -> ( ( G DProd s ) = t <-> ( G DProd s ) = W ) )
103	102	anbi2d	|- ( t = W -> ( ( G dom DProd s /\ ( G DProd s ) = t ) <-> ( G dom DProd s /\ ( G DProd s ) = W ) ) )
104	103	rexbidv	|- ( t = W -> ( E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) <-> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = W ) ) )
105	101 104	imbi12d	|- ( t = W -> ( ( t C. U -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) <-> ( W C. U -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = W ) ) ) )
106	22	simpld	|- ( ph -> W e. ( SubGrp ` G ) )
107	105 7 106	rspcdva	|- ( ph -> ( W C. U -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = W ) ) )
108	100 107	mpd	|- ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = W ) )
109		breq2	|- ( s = a -> ( G dom DProd s <-> G dom DProd a ) )
110		oveq2	|- ( s = a -> ( G DProd s ) = ( G DProd a ) )
111	110	eqeq1d	|- ( s = a -> ( ( G DProd s ) = W <-> ( G DProd a ) = W ) )
112	109 111	anbi12d	|- ( s = a -> ( ( G dom DProd s /\ ( G DProd s ) = W ) <-> ( G dom DProd a /\ ( G DProd a ) = W ) ) )
113	112	cbvrexvw	|- ( E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = W ) <-> E. a e. Word C ( G dom DProd a /\ ( G DProd a ) = W ) )
114	108 113	sylib	|- ( ph -> E. a e. Word C ( G dom DProd a /\ ( G DProd a ) = W ) )
115	3	adantr	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> G e. Abel )
116	4	adantr	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> P pGrp G )
117	5	adantr	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> B e. Fin )
118	6	adantr	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> U e. ( SubGrp ` G ) )
119	7	adantr	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> A. t e. ( SubGrp ` G ) ( t C. U -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = t ) ) )
120	14	adantr	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> E =/= 1 )
121	15	adantr	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> X e. U )
122	16	adantr	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> ( O ` X ) = E )
123	17	adantr	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> W e. ( SubGrp ` H ) )
124	18	adantr	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> ( ( K ` { X } ) i^i W ) = { .0. } )
125	19	adantr	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> ( ( K ` { X } ) .(+) W ) = U )
126		simprl	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> a e. Word C )
127		simprrl	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> G dom DProd a )
128		simprrr	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> ( G DProd a ) = W )
129		eqid	|- ( a ++ <" ( K ` { X } ) "> ) = ( a ++ <" ( K ` { X } ) "> )
130	1 2 115 116 117 118 119 8 9 10 11 12 13 120 121 122 123 124 125 126 127 128 129	pgpfaclem1	|- ( ( ph /\ ( a e. Word C /\ ( G dom DProd a /\ ( G DProd a ) = W ) ) ) -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )
131	114 130	rexlimddv	|- ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = U ) )