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

Metamath Proof Explorer

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