MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pgpfaclem2 Structured version   Visualization version   GIF version

Theorem pgpfaclem2 19993
Description: Lemma for pgpfac 19995. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
Hypotheses
Ref Expression
pgpfac.b 𝐡 = (Baseβ€˜πΊ)
pgpfac.c 𝐢 = {π‘Ÿ ∈ (SubGrpβ€˜πΊ) ∣ (𝐺 β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )}
pgpfac.g (πœ‘ β†’ 𝐺 ∈ Abel)
pgpfac.p (πœ‘ β†’ 𝑃 pGrp 𝐺)
pgpfac.f (πœ‘ β†’ 𝐡 ∈ Fin)
pgpfac.u (πœ‘ β†’ π‘ˆ ∈ (SubGrpβ€˜πΊ))
pgpfac.a (πœ‘ β†’ βˆ€π‘‘ ∈ (SubGrpβ€˜πΊ)(𝑑 ⊊ π‘ˆ β†’ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑑)))
pgpfac.h 𝐻 = (𝐺 β†Ύs π‘ˆ)
pgpfac.k 𝐾 = (mrClsβ€˜(SubGrpβ€˜π»))
pgpfac.o 𝑂 = (odβ€˜π»)
pgpfac.e 𝐸 = (gExβ€˜π»)
pgpfac.0 0 = (0gβ€˜π»)
pgpfac.l βŠ• = (LSSumβ€˜π»)
pgpfac.1 (πœ‘ β†’ 𝐸 β‰  1)
pgpfac.x (πœ‘ β†’ 𝑋 ∈ π‘ˆ)
pgpfac.oe (πœ‘ β†’ (π‘‚β€˜π‘‹) = 𝐸)
pgpfac.w (πœ‘ β†’ π‘Š ∈ (SubGrpβ€˜π»))
pgpfac.i (πœ‘ β†’ ((πΎβ€˜{𝑋}) ∩ π‘Š) = { 0 })
pgpfac.s (πœ‘ β†’ ((πΎβ€˜{𝑋}) βŠ• π‘Š) = π‘ˆ)
Assertion
Ref Expression
pgpfaclem2 (πœ‘ β†’ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = π‘ˆ))
Distinct variable groups:   𝑑,𝑠,𝐢   𝑠,π‘Ÿ,𝑑,𝐺   𝐾,π‘Ÿ,𝑠   πœ‘,𝑑   𝐡,𝑠,𝑑   π‘ˆ,π‘Ÿ,𝑠,𝑑   π‘Š,𝑠,𝑑   𝑋,π‘Ÿ,𝑠
Allowed substitution hints:   πœ‘(𝑠,π‘Ÿ)   𝐡(π‘Ÿ)   𝐢(π‘Ÿ)   𝑃(𝑑,𝑠,π‘Ÿ)   βŠ• (𝑑,𝑠,π‘Ÿ)   𝐸(𝑑,𝑠,π‘Ÿ)   𝐻(𝑑,𝑠,π‘Ÿ)   𝐾(𝑑)   𝑂(𝑑,𝑠,π‘Ÿ)   π‘Š(π‘Ÿ)   𝑋(𝑑)   0 (𝑑,𝑠,π‘Ÿ)

Proof of Theorem pgpfaclem2
Dummy variable π‘Ž is distinct from all other variables.
StepHypRef Expression
1 pgpfac.w . . . . . . 7 (πœ‘ β†’ π‘Š ∈ (SubGrpβ€˜π»))
2 pgpfac.u . . . . . . . 8 (πœ‘ β†’ π‘ˆ ∈ (SubGrpβ€˜πΊ))
3 pgpfac.h . . . . . . . . 9 𝐻 = (𝐺 β†Ύs π‘ˆ)
43subsubg 19065 . . . . . . . 8 (π‘ˆ ∈ (SubGrpβ€˜πΊ) β†’ (π‘Š ∈ (SubGrpβ€˜π») ↔ (π‘Š ∈ (SubGrpβ€˜πΊ) ∧ π‘Š βŠ† π‘ˆ)))
52, 4syl 17 . . . . . . 7 (πœ‘ β†’ (π‘Š ∈ (SubGrpβ€˜π») ↔ (π‘Š ∈ (SubGrpβ€˜πΊ) ∧ π‘Š βŠ† π‘ˆ)))
61, 5mpbid 231 . . . . . 6 (πœ‘ β†’ (π‘Š ∈ (SubGrpβ€˜πΊ) ∧ π‘Š βŠ† π‘ˆ))
76simprd 494 . . . . 5 (πœ‘ β†’ π‘Š βŠ† π‘ˆ)
8 pgpfac.f . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ Fin)
9 pgpfac.b . . . . . . . . . . . . 13 𝐡 = (Baseβ€˜πΊ)
109subgss 19043 . . . . . . . . . . . 12 (π‘ˆ ∈ (SubGrpβ€˜πΊ) β†’ π‘ˆ βŠ† 𝐡)
112, 10syl 17 . . . . . . . . . . 11 (πœ‘ β†’ π‘ˆ βŠ† 𝐡)
128, 11ssfid 9269 . . . . . . . . . 10 (πœ‘ β†’ π‘ˆ ∈ Fin)
1312, 7ssfid 9269 . . . . . . . . 9 (πœ‘ β†’ π‘Š ∈ Fin)
14 hashcl 14320 . . . . . . . . 9 (π‘Š ∈ Fin β†’ (β™―β€˜π‘Š) ∈ β„•0)
1513, 14syl 17 . . . . . . . 8 (πœ‘ β†’ (β™―β€˜π‘Š) ∈ β„•0)
1615nn0red 12537 . . . . . . 7 (πœ‘ β†’ (β™―β€˜π‘Š) ∈ ℝ)
17 pgpfac.0 . . . . . . . . . . . 12 0 = (0gβ€˜π»)
1817fvexi 6904 . . . . . . . . . . 11 0 ∈ V
19 hashsng 14333 . . . . . . . . . . 11 ( 0 ∈ V β†’ (β™―β€˜{ 0 }) = 1)
2018, 19ax-mp 5 . . . . . . . . . 10 (β™―β€˜{ 0 }) = 1
21 subgrcl 19047 . . . . . . . . . . . . . . . 16 (π‘Š ∈ (SubGrpβ€˜π») β†’ 𝐻 ∈ Grp)
22 eqid 2730 . . . . . . . . . . . . . . . . 17 (Baseβ€˜π») = (Baseβ€˜π»)
2322subgacs 19077 . . . . . . . . . . . . . . . 16 (𝐻 ∈ Grp β†’ (SubGrpβ€˜π») ∈ (ACSβ€˜(Baseβ€˜π»)))
24 acsmre 17600 . . . . . . . . . . . . . . . 16 ((SubGrpβ€˜π») ∈ (ACSβ€˜(Baseβ€˜π»)) β†’ (SubGrpβ€˜π») ∈ (Mooreβ€˜(Baseβ€˜π»)))
251, 21, 23, 244syl 19 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (SubGrpβ€˜π») ∈ (Mooreβ€˜(Baseβ€˜π»)))
26 pgpfac.k . . . . . . . . . . . . . . 15 𝐾 = (mrClsβ€˜(SubGrpβ€˜π»))
2725, 26mrcssvd 17571 . . . . . . . . . . . . . 14 (πœ‘ β†’ (πΎβ€˜{𝑋}) βŠ† (Baseβ€˜π»))
283subgbas 19046 . . . . . . . . . . . . . . 15 (π‘ˆ ∈ (SubGrpβ€˜πΊ) β†’ π‘ˆ = (Baseβ€˜π»))
292, 28syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ π‘ˆ = (Baseβ€˜π»))
3027, 29sseqtrrd 4022 . . . . . . . . . . . . 13 (πœ‘ β†’ (πΎβ€˜{𝑋}) βŠ† π‘ˆ)
3112, 30ssfid 9269 . . . . . . . . . . . 12 (πœ‘ β†’ (πΎβ€˜{𝑋}) ∈ Fin)
32 pgpfac.x . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑋 ∈ π‘ˆ)
3332, 29eleqtrd 2833 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑋 ∈ (Baseβ€˜π»))
3426mrcsncl 17560 . . . . . . . . . . . . . . . 16 (((SubGrpβ€˜π») ∈ (Mooreβ€˜(Baseβ€˜π»)) ∧ 𝑋 ∈ (Baseβ€˜π»)) β†’ (πΎβ€˜{𝑋}) ∈ (SubGrpβ€˜π»))
3525, 33, 34syl2anc 582 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (πΎβ€˜{𝑋}) ∈ (SubGrpβ€˜π»))
3617subg0cl 19050 . . . . . . . . . . . . . . 15 ((πΎβ€˜{𝑋}) ∈ (SubGrpβ€˜π») β†’ 0 ∈ (πΎβ€˜{𝑋}))
3735, 36syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 ∈ (πΎβ€˜{𝑋}))
3837snssd 4811 . . . . . . . . . . . . 13 (πœ‘ β†’ { 0 } βŠ† (πΎβ€˜{𝑋}))
3933snssd 4811 . . . . . . . . . . . . . . 15 (πœ‘ β†’ {𝑋} βŠ† (Baseβ€˜π»))
4025, 26, 39mrcssidd 17573 . . . . . . . . . . . . . 14 (πœ‘ β†’ {𝑋} βŠ† (πΎβ€˜{𝑋}))
41 snssg 4786 . . . . . . . . . . . . . . 15 (𝑋 ∈ π‘ˆ β†’ (𝑋 ∈ (πΎβ€˜{𝑋}) ↔ {𝑋} βŠ† (πΎβ€˜{𝑋})))
4232, 41syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑋 ∈ (πΎβ€˜{𝑋}) ↔ {𝑋} βŠ† (πΎβ€˜{𝑋})))
4340, 42mpbird 256 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑋 ∈ (πΎβ€˜{𝑋}))
44 pgpfac.oe . . . . . . . . . . . . . . 15 (πœ‘ β†’ (π‘‚β€˜π‘‹) = 𝐸)
45 pgpfac.1 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐸 β‰  1)
4644, 45eqnetrd 3006 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘‚β€˜π‘‹) β‰  1)
47 pgpfac.o . . . . . . . . . . . . . . . . . 18 𝑂 = (odβ€˜π»)
4847, 17od1 19468 . . . . . . . . . . . . . . . . 17 (𝐻 ∈ Grp β†’ (π‘‚β€˜ 0 ) = 1)
491, 21, 483syl 18 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (π‘‚β€˜ 0 ) = 1)
50 elsni 4644 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ { 0 } β†’ 𝑋 = 0 )
5150fveqeq2d 6898 . . . . . . . . . . . . . . . 16 (𝑋 ∈ { 0 } β†’ ((π‘‚β€˜π‘‹) = 1 ↔ (π‘‚β€˜ 0 ) = 1))
5249, 51syl5ibrcom 246 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑋 ∈ { 0 } β†’ (π‘‚β€˜π‘‹) = 1))
5352necon3ad 2951 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘‚β€˜π‘‹) β‰  1 β†’ Β¬ 𝑋 ∈ { 0 }))
5446, 53mpd 15 . . . . . . . . . . . . 13 (πœ‘ β†’ Β¬ 𝑋 ∈ { 0 })
5538, 43, 54ssnelpssd 4111 . . . . . . . . . . . 12 (πœ‘ β†’ { 0 } ⊊ (πΎβ€˜{𝑋}))
56 php3 9214 . . . . . . . . . . . 12 (((πΎβ€˜{𝑋}) ∈ Fin ∧ { 0 } ⊊ (πΎβ€˜{𝑋})) β†’ { 0 } β‰Ί (πΎβ€˜{𝑋}))
5731, 55, 56syl2anc 582 . . . . . . . . . . 11 (πœ‘ β†’ { 0 } β‰Ί (πΎβ€˜{𝑋}))
58 snfi 9046 . . . . . . . . . . . 12 { 0 } ∈ Fin
59 hashsdom 14345 . . . . . . . . . . . 12 (({ 0 } ∈ Fin ∧ (πΎβ€˜{𝑋}) ∈ Fin) β†’ ((β™―β€˜{ 0 }) < (β™―β€˜(πΎβ€˜{𝑋})) ↔ { 0 } β‰Ί (πΎβ€˜{𝑋})))
6058, 31, 59sylancr 585 . . . . . . . . . . 11 (πœ‘ β†’ ((β™―β€˜{ 0 }) < (β™―β€˜(πΎβ€˜{𝑋})) ↔ { 0 } β‰Ί (πΎβ€˜{𝑋})))
6157, 60mpbird 256 . . . . . . . . . 10 (πœ‘ β†’ (β™―β€˜{ 0 }) < (β™―β€˜(πΎβ€˜{𝑋})))
6220, 61eqbrtrrid 5183 . . . . . . . . 9 (πœ‘ β†’ 1 < (β™―β€˜(πΎβ€˜{𝑋})))
63 1red 11219 . . . . . . . . . 10 (πœ‘ β†’ 1 ∈ ℝ)
64 hashcl 14320 . . . . . . . . . . . 12 ((πΎβ€˜{𝑋}) ∈ Fin β†’ (β™―β€˜(πΎβ€˜{𝑋})) ∈ β„•0)
6531, 64syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜(πΎβ€˜{𝑋})) ∈ β„•0)
6665nn0red 12537 . . . . . . . . . 10 (πœ‘ β†’ (β™―β€˜(πΎβ€˜{𝑋})) ∈ ℝ)
6717subg0cl 19050 . . . . . . . . . . . . 13 (π‘Š ∈ (SubGrpβ€˜π») β†’ 0 ∈ π‘Š)
68 ne0i 4333 . . . . . . . . . . . . 13 ( 0 ∈ π‘Š β†’ π‘Š β‰  βˆ…)
691, 67, 683syl 18 . . . . . . . . . . . 12 (πœ‘ β†’ π‘Š β‰  βˆ…)
70 hashnncl 14330 . . . . . . . . . . . . 13 (π‘Š ∈ Fin β†’ ((β™―β€˜π‘Š) ∈ β„• ↔ π‘Š β‰  βˆ…))
7113, 70syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ ((β™―β€˜π‘Š) ∈ β„• ↔ π‘Š β‰  βˆ…))
7269, 71mpbird 256 . . . . . . . . . . 11 (πœ‘ β†’ (β™―β€˜π‘Š) ∈ β„•)
7372nngt0d 12265 . . . . . . . . . 10 (πœ‘ β†’ 0 < (β™―β€˜π‘Š))
74 ltmul1 12068 . . . . . . . . . 10 ((1 ∈ ℝ ∧ (β™―β€˜(πΎβ€˜{𝑋})) ∈ ℝ ∧ ((β™―β€˜π‘Š) ∈ ℝ ∧ 0 < (β™―β€˜π‘Š))) β†’ (1 < (β™―β€˜(πΎβ€˜{𝑋})) ↔ (1 Β· (β™―β€˜π‘Š)) < ((β™―β€˜(πΎβ€˜{𝑋})) Β· (β™―β€˜π‘Š))))
7563, 66, 16, 73, 74syl112anc 1372 . . . . . . . . 9 (πœ‘ β†’ (1 < (β™―β€˜(πΎβ€˜{𝑋})) ↔ (1 Β· (β™―β€˜π‘Š)) < ((β™―β€˜(πΎβ€˜{𝑋})) Β· (β™―β€˜π‘Š))))
7662, 75mpbid 231 . . . . . . . 8 (πœ‘ β†’ (1 Β· (β™―β€˜π‘Š)) < ((β™―β€˜(πΎβ€˜{𝑋})) Β· (β™―β€˜π‘Š)))
7716recnd 11246 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜π‘Š) ∈ β„‚)
7877mullidd 11236 . . . . . . . 8 (πœ‘ β†’ (1 Β· (β™―β€˜π‘Š)) = (β™―β€˜π‘Š))
79 pgpfac.l . . . . . . . . . 10 βŠ• = (LSSumβ€˜π»)
80 eqid 2730 . . . . . . . . . 10 (Cntzβ€˜π») = (Cntzβ€˜π»)
81 pgpfac.i . . . . . . . . . 10 (πœ‘ β†’ ((πΎβ€˜{𝑋}) ∩ π‘Š) = { 0 })
82 pgpfac.g . . . . . . . . . . . 12 (πœ‘ β†’ 𝐺 ∈ Abel)
833subgabl 19745 . . . . . . . . . . . 12 ((𝐺 ∈ Abel ∧ π‘ˆ ∈ (SubGrpβ€˜πΊ)) β†’ 𝐻 ∈ Abel)
8482, 2, 83syl2anc 582 . . . . . . . . . . 11 (πœ‘ β†’ 𝐻 ∈ Abel)
8580, 84, 35, 1ablcntzd 19766 . . . . . . . . . 10 (πœ‘ β†’ (πΎβ€˜{𝑋}) βŠ† ((Cntzβ€˜π»)β€˜π‘Š))
8679, 17, 80, 35, 1, 81, 85, 31, 13lsmhash 19614 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜((πΎβ€˜{𝑋}) βŠ• π‘Š)) = ((β™―β€˜(πΎβ€˜{𝑋})) Β· (β™―β€˜π‘Š)))
87 pgpfac.s . . . . . . . . . 10 (πœ‘ β†’ ((πΎβ€˜{𝑋}) βŠ• π‘Š) = π‘ˆ)
8887fveq2d 6894 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜((πΎβ€˜{𝑋}) βŠ• π‘Š)) = (β™―β€˜π‘ˆ))
8986, 88eqtr3d 2772 . . . . . . . 8 (πœ‘ β†’ ((β™―β€˜(πΎβ€˜{𝑋})) Β· (β™―β€˜π‘Š)) = (β™―β€˜π‘ˆ))
9076, 78, 893brtr3d 5178 . . . . . . 7 (πœ‘ β†’ (β™―β€˜π‘Š) < (β™―β€˜π‘ˆ))
9116, 90ltned 11354 . . . . . 6 (πœ‘ β†’ (β™―β€˜π‘Š) β‰  (β™―β€˜π‘ˆ))
92 fveq2 6890 . . . . . . 7 (π‘Š = π‘ˆ β†’ (β™―β€˜π‘Š) = (β™―β€˜π‘ˆ))
9392necon3i 2971 . . . . . 6 ((β™―β€˜π‘Š) β‰  (β™―β€˜π‘ˆ) β†’ π‘Š β‰  π‘ˆ)
9491, 93syl 17 . . . . 5 (πœ‘ β†’ π‘Š β‰  π‘ˆ)
95 df-pss 3966 . . . . 5 (π‘Š ⊊ π‘ˆ ↔ (π‘Š βŠ† π‘ˆ ∧ π‘Š β‰  π‘ˆ))
967, 94, 95sylanbrc 581 . . . 4 (πœ‘ β†’ π‘Š ⊊ π‘ˆ)
97 psseq1 4086 . . . . . 6 (𝑑 = π‘Š β†’ (𝑑 ⊊ π‘ˆ ↔ π‘Š ⊊ π‘ˆ))
98 eqeq2 2742 . . . . . . . 8 (𝑑 = π‘Š β†’ ((𝐺 DProd 𝑠) = 𝑑 ↔ (𝐺 DProd 𝑠) = π‘Š))
9998anbi2d 627 . . . . . . 7 (𝑑 = π‘Š β†’ ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑑) ↔ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = π‘Š)))
10099rexbidv 3176 . . . . . 6 (𝑑 = π‘Š β†’ (βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑑) ↔ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = π‘Š)))
10197, 100imbi12d 343 . . . . 5 (𝑑 = π‘Š β†’ ((𝑑 ⊊ π‘ˆ β†’ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑑)) ↔ (π‘Š ⊊ π‘ˆ β†’ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = π‘Š))))
102 pgpfac.a . . . . 5 (πœ‘ β†’ βˆ€π‘‘ ∈ (SubGrpβ€˜πΊ)(𝑑 ⊊ π‘ˆ β†’ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑑)))
1036simpld 493 . . . . 5 (πœ‘ β†’ π‘Š ∈ (SubGrpβ€˜πΊ))
104101, 102, 103rspcdva 3612 . . . 4 (πœ‘ β†’ (π‘Š ⊊ π‘ˆ β†’ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = π‘Š)))
10596, 104mpd 15 . . 3 (πœ‘ β†’ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = π‘Š))
106 breq2 5151 . . . . 5 (𝑠 = π‘Ž β†’ (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd π‘Ž))
107 oveq2 7419 . . . . . 6 (𝑠 = π‘Ž β†’ (𝐺 DProd 𝑠) = (𝐺 DProd π‘Ž))
108107eqeq1d 2732 . . . . 5 (𝑠 = π‘Ž β†’ ((𝐺 DProd 𝑠) = π‘Š ↔ (𝐺 DProd π‘Ž) = π‘Š))
109106, 108anbi12d 629 . . . 4 (𝑠 = π‘Ž β†’ ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = π‘Š) ↔ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š)))
110109cbvrexvw 3233 . . 3 (βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = π‘Š) ↔ βˆƒπ‘Ž ∈ Word 𝐢(𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))
111105, 110sylib 217 . 2 (πœ‘ β†’ βˆƒπ‘Ž ∈ Word 𝐢(𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))
112 pgpfac.c . . 3 𝐢 = {π‘Ÿ ∈ (SubGrpβ€˜πΊ) ∣ (𝐺 β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )}
11382adantr 479 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ 𝐺 ∈ Abel)
114 pgpfac.p . . . 4 (πœ‘ β†’ 𝑃 pGrp 𝐺)
115114adantr 479 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ 𝑃 pGrp 𝐺)
1168adantr 479 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ 𝐡 ∈ Fin)
1172adantr 479 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ π‘ˆ ∈ (SubGrpβ€˜πΊ))
118102adantr 479 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ βˆ€π‘‘ ∈ (SubGrpβ€˜πΊ)(𝑑 ⊊ π‘ˆ β†’ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑑)))
119 pgpfac.e . . 3 𝐸 = (gExβ€˜π»)
12045adantr 479 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ 𝐸 β‰  1)
12132adantr 479 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ 𝑋 ∈ π‘ˆ)
12244adantr 479 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ (π‘‚β€˜π‘‹) = 𝐸)
1231adantr 479 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ π‘Š ∈ (SubGrpβ€˜π»))
12481adantr 479 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ ((πΎβ€˜{𝑋}) ∩ π‘Š) = { 0 })
12587adantr 479 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ ((πΎβ€˜{𝑋}) βŠ• π‘Š) = π‘ˆ)
126 simprl 767 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ π‘Ž ∈ Word 𝐢)
127 simprrl 777 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ 𝐺dom DProd π‘Ž)
128 simprrr 778 . . 3 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ (𝐺 DProd π‘Ž) = π‘Š)
129 eqid 2730 . . 3 (π‘Ž ++ βŸ¨β€œ(πΎβ€˜{𝑋})β€βŸ©) = (π‘Ž ++ βŸ¨β€œ(πΎβ€˜{𝑋})β€βŸ©)
1309, 112, 113, 115, 116, 117, 118, 3, 26, 47, 119, 17, 79, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129pgpfaclem1 19992 . 2 ((πœ‘ ∧ (π‘Ž ∈ Word 𝐢 ∧ (𝐺dom DProd π‘Ž ∧ (𝐺 DProd π‘Ž) = π‘Š))) β†’ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = π‘ˆ))
131111, 130rexlimddv 3159 1 (πœ‘ β†’ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = π‘ˆ))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  {crab 3430  Vcvv 3472   ∩ cin 3946   βŠ† wss 3947   ⊊ wpss 3948  βˆ…c0 4321  {csn 4627   class class class wbr 5147  dom cdm 5675  ran crn 5676  β€˜cfv 6542  (class class class)co 7411   β‰Ί csdm 8940  Fincfn 8941  β„cr 11111  0cc0 11112  1c1 11113   Β· cmul 11117   < clt 11252  β„•cn 12216  β„•0cn0 12476  β™―chash 14294  Word cword 14468   ++ cconcat 14524  βŸ¨β€œcs1 14549  Basecbs 17148   β†Ύs cress 17177  0gc0g 17389  Moorecmre 17530  mrClscmrc 17531  ACScacs 17533  Grpcgrp 18855  SubGrpcsubg 19036  Cntzccntz 19220  odcod 19433  gExcgex 19434   pGrp cpgp 19435  LSSumclsm 19543  Abelcabl 19690  CycGrpccyg 19786   DProd cdprd 19904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-tpos 8213  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-n0 12477  df-xnn0 12549  df-z 12563  df-uz 12827  df-fz 13489  df-fzo 13632  df-seq 13971  df-hash 14295  df-word 14469  df-concat 14525  df-s1 14550  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-0g 17391  df-gsum 17392  df-mre 17534  df-mrc 17535  df-acs 17537  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-mhm 18705  df-submnd 18706  df-grp 18858  df-minusg 18859  df-sbg 18860  df-mulg 18987  df-subg 19039  df-ghm 19128  df-gim 19173  df-cntz 19222  df-oppg 19251  df-od 19437  df-pgp 19439  df-lsm 19545  df-pj1 19546  df-cmn 19691  df-abl 19692  df-cyg 19787  df-dprd 19906
This theorem is referenced by:  pgpfaclem3  19994
  Copyright terms: Public domain W3C validator