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

Theorem pgpfaclem2 19875
Description: Lemma for pgpfac 19877. (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 18965 . . . . . . . 8 (𝑈 ∈ (SubGrp‘𝐺) → (𝑊 ∈ (SubGrp‘𝐻) ↔ (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊𝑈)))
52, 4syl 17 . . . . . . 7 (𝜑 → (𝑊 ∈ (SubGrp‘𝐻) ↔ (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊𝑈)))
61, 5mpbid 231 . . . . . 6 (𝜑 → (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊𝑈))
76simprd 496 . . . . 5 (𝜑𝑊𝑈)
8 pgpfac.f . . . . . . . . . . 11 (𝜑𝐵 ∈ Fin)
9 pgpfac.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝐺)
109subgss 18943 . . . . . . . . . . . 12 (𝑈 ∈ (SubGrp‘𝐺) → 𝑈𝐵)
112, 10syl 17 . . . . . . . . . . 11 (𝜑𝑈𝐵)
128, 11ssfid 9218 . . . . . . . . . 10 (𝜑𝑈 ∈ Fin)
1312, 7ssfid 9218 . . . . . . . . 9 (𝜑𝑊 ∈ Fin)
14 hashcl 14266 . . . . . . . . 9 (𝑊 ∈ Fin → (♯‘𝑊) ∈ ℕ0)
1513, 14syl 17 . . . . . . . 8 (𝜑 → (♯‘𝑊) ∈ ℕ0)
1615nn0red 12483 . . . . . . 7 (𝜑 → (♯‘𝑊) ∈ ℝ)
17 pgpfac.0 . . . . . . . . . . . 12 0 = (0g𝐻)
1817fvexi 6861 . . . . . . . . . . 11 0 ∈ V
19 hashsng 14279 . . . . . . . . . . 11 ( 0 ∈ V → (♯‘{ 0 }) = 1)
2018, 19ax-mp 5 . . . . . . . . . 10 (♯‘{ 0 }) = 1
21 subgrcl 18947 . . . . . . . . . . . . . . . 16 (𝑊 ∈ (SubGrp‘𝐻) → 𝐻 ∈ Grp)
22 eqid 2731 . . . . . . . . . . . . . . . . 17 (Base‘𝐻) = (Base‘𝐻)
2322subgacs 18977 . . . . . . . . . . . . . . . 16 (𝐻 ∈ Grp → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
24 acsmre 17546 . . . . . . . . . . . . . . . 16 ((SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)) → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
251, 21, 23, 244syl 19 . . . . . . . . . . . . . . 15 (𝜑 → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
26 pgpfac.k . . . . . . . . . . . . . . 15 𝐾 = (mrCls‘(SubGrp‘𝐻))
2725, 26mrcssvd 17517 . . . . . . . . . . . . . 14 (𝜑 → (𝐾‘{𝑋}) ⊆ (Base‘𝐻))
283subgbas 18946 . . . . . . . . . . . . . . 15 (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻))
292, 28syl 17 . . . . . . . . . . . . . 14 (𝜑𝑈 = (Base‘𝐻))
3027, 29sseqtrrd 3988 . . . . . . . . . . . . 13 (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈)
3112, 30ssfid 9218 . . . . . . . . . . . 12 (𝜑 → (𝐾‘{𝑋}) ∈ Fin)
32 pgpfac.x . . . . . . . . . . . . . . . . 17 (𝜑𝑋𝑈)
3332, 29eleqtrd 2834 . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ (Base‘𝐻))
3426mrcsncl 17506 . . . . . . . . . . . . . . . 16 (((SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
3525, 33, 34syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
3617subg0cl 18950 . . . . . . . . . . . . . . 15 ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) → 0 ∈ (𝐾‘{𝑋}))
3735, 36syl 17 . . . . . . . . . . . . . 14 (𝜑0 ∈ (𝐾‘{𝑋}))
3837snssd 4774 . . . . . . . . . . . . 13 (𝜑 → { 0 } ⊆ (𝐾‘{𝑋}))
3933snssd 4774 . . . . . . . . . . . . . . 15 (𝜑 → {𝑋} ⊆ (Base‘𝐻))
4025, 26, 39mrcssidd 17519 . . . . . . . . . . . . . 14 (𝜑 → {𝑋} ⊆ (𝐾‘{𝑋}))
41 snssg 4749 . . . . . . . . . . . . . . 15 (𝑋𝑈 → (𝑋 ∈ (𝐾‘{𝑋}) ↔ {𝑋} ⊆ (𝐾‘{𝑋})))
4232, 41syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 ∈ (𝐾‘{𝑋}) ↔ {𝑋} ⊆ (𝐾‘{𝑋})))
4340, 42mpbird 256 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ (𝐾‘{𝑋}))
44 pgpfac.oe . . . . . . . . . . . . . . 15 (𝜑 → (𝑂𝑋) = 𝐸)
45 pgpfac.1 . . . . . . . . . . . . . . 15 (𝜑𝐸 ≠ 1)
4644, 45eqnetrd 3007 . . . . . . . . . . . . . 14 (𝜑 → (𝑂𝑋) ≠ 1)
47 pgpfac.o . . . . . . . . . . . . . . . . . 18 𝑂 = (od‘𝐻)
4847, 17od1 19355 . . . . . . . . . . . . . . . . 17 (𝐻 ∈ Grp → (𝑂0 ) = 1)
491, 21, 483syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑂0 ) = 1)
50 elsni 4608 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ { 0 } → 𝑋 = 0 )
5150fveqeq2d 6855 . . . . . . . . . . . . . . . 16 (𝑋 ∈ { 0 } → ((𝑂𝑋) = 1 ↔ (𝑂0 ) = 1))
5249, 51syl5ibrcom 246 . . . . . . . . . . . . . . 15 (𝜑 → (𝑋 ∈ { 0 } → (𝑂𝑋) = 1))
5352necon3ad 2952 . . . . . . . . . . . . . 14 (𝜑 → ((𝑂𝑋) ≠ 1 → ¬ 𝑋 ∈ { 0 }))
5446, 53mpd 15 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝑋 ∈ { 0 })
5538, 43, 54ssnelpssd 4077 . . . . . . . . . . . 12 (𝜑 → { 0 } ⊊ (𝐾‘{𝑋}))
56 php3 9163 . . . . . . . . . . . 12 (((𝐾‘{𝑋}) ∈ Fin ∧ { 0 } ⊊ (𝐾‘{𝑋})) → { 0 } ≺ (𝐾‘{𝑋}))
5731, 55, 56syl2anc 584 . . . . . . . . . . 11 (𝜑 → { 0 } ≺ (𝐾‘{𝑋}))
58 snfi 8995 . . . . . . . . . . . 12 { 0 } ∈ Fin
59 hashsdom 14291 . . . . . . . . . . . 12 (({ 0 } ∈ Fin ∧ (𝐾‘{𝑋}) ∈ Fin) → ((♯‘{ 0 }) < (♯‘(𝐾‘{𝑋})) ↔ { 0 } ≺ (𝐾‘{𝑋})))
6058, 31, 59sylancr 587 . . . . . . . . . . 11 (𝜑 → ((♯‘{ 0 }) < (♯‘(𝐾‘{𝑋})) ↔ { 0 } ≺ (𝐾‘{𝑋})))
6157, 60mpbird 256 . . . . . . . . . 10 (𝜑 → (♯‘{ 0 }) < (♯‘(𝐾‘{𝑋})))
6220, 61eqbrtrrid 5146 . . . . . . . . 9 (𝜑 → 1 < (♯‘(𝐾‘{𝑋})))
63 1red 11165 . . . . . . . . . 10 (𝜑 → 1 ∈ ℝ)
64 hashcl 14266 . . . . . . . . . . . 12 ((𝐾‘{𝑋}) ∈ Fin → (♯‘(𝐾‘{𝑋})) ∈ ℕ0)
6531, 64syl 17 . . . . . . . . . . 11 (𝜑 → (♯‘(𝐾‘{𝑋})) ∈ ℕ0)
6665nn0red 12483 . . . . . . . . . 10 (𝜑 → (♯‘(𝐾‘{𝑋})) ∈ ℝ)
6717subg0cl 18950 . . . . . . . . . . . . 13 (𝑊 ∈ (SubGrp‘𝐻) → 0𝑊)
68 ne0i 4299 . . . . . . . . . . . . 13 ( 0𝑊𝑊 ≠ ∅)
691, 67, 683syl 18 . . . . . . . . . . . 12 (𝜑𝑊 ≠ ∅)
70 hashnncl 14276 . . . . . . . . . . . . 13 (𝑊 ∈ Fin → ((♯‘𝑊) ∈ ℕ ↔ 𝑊 ≠ ∅))
7113, 70syl 17 . . . . . . . . . . . 12 (𝜑 → ((♯‘𝑊) ∈ ℕ ↔ 𝑊 ≠ ∅))
7269, 71mpbird 256 . . . . . . . . . . 11 (𝜑 → (♯‘𝑊) ∈ ℕ)
7372nngt0d 12211 . . . . . . . . . 10 (𝜑 → 0 < (♯‘𝑊))
74 ltmul1 12014 . . . . . . . . . 10 ((1 ∈ ℝ ∧ (♯‘(𝐾‘{𝑋})) ∈ ℝ ∧ ((♯‘𝑊) ∈ ℝ ∧ 0 < (♯‘𝑊))) → (1 < (♯‘(𝐾‘{𝑋})) ↔ (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊))))
7563, 66, 16, 73, 74syl112anc 1374 . . . . . . . . 9 (𝜑 → (1 < (♯‘(𝐾‘{𝑋})) ↔ (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊))))
7662, 75mpbid 231 . . . . . . . 8 (𝜑 → (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)))
7716recnd 11192 . . . . . . . . 9 (𝜑 → (♯‘𝑊) ∈ ℂ)
7877mullidd 11182 . . . . . . . 8 (𝜑 → (1 · (♯‘𝑊)) = (♯‘𝑊))
79 pgpfac.l . . . . . . . . . 10 = (LSSum‘𝐻)
80 eqid 2731 . . . . . . . . . 10 (Cntz‘𝐻) = (Cntz‘𝐻)
81 pgpfac.i . . . . . . . . . 10 (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })
82 pgpfac.g . . . . . . . . . . . 12 (𝜑𝐺 ∈ Abel)
833subgabl 19628 . . . . . . . . . . . 12 ((𝐺 ∈ Abel ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Abel)
8482, 2, 83syl2anc 584 . . . . . . . . . . 11 (𝜑𝐻 ∈ Abel)
8580, 84, 35, 1ablcntzd 19649 . . . . . . . . . 10 (𝜑 → (𝐾‘{𝑋}) ⊆ ((Cntz‘𝐻)‘𝑊))
8679, 17, 80, 35, 1, 81, 85, 31, 13lsmhash 19501 . . . . . . . . 9 (𝜑 → (♯‘((𝐾‘{𝑋}) 𝑊)) = ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)))
87 pgpfac.s . . . . . . . . . 10 (𝜑 → ((𝐾‘{𝑋}) 𝑊) = 𝑈)
8887fveq2d 6851 . . . . . . . . 9 (𝜑 → (♯‘((𝐾‘{𝑋}) 𝑊)) = (♯‘𝑈))
8986, 88eqtr3d 2773 . . . . . . . 8 (𝜑 → ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)) = (♯‘𝑈))
9076, 78, 893brtr3d 5141 . . . . . . 7 (𝜑 → (♯‘𝑊) < (♯‘𝑈))
9116, 90ltned 11300 . . . . . 6 (𝜑 → (♯‘𝑊) ≠ (♯‘𝑈))
92 fveq2 6847 . . . . . . 7 (𝑊 = 𝑈 → (♯‘𝑊) = (♯‘𝑈))
9392necon3i 2972 . . . . . 6 ((♯‘𝑊) ≠ (♯‘𝑈) → 𝑊𝑈)
9491, 93syl 17 . . . . 5 (𝜑𝑊𝑈)
95 df-pss 3932 . . . . 5 (𝑊𝑈 ↔ (𝑊𝑈𝑊𝑈))
967, 94, 95sylanbrc 583 . . . 4 (𝜑𝑊𝑈)
97 psseq1 4052 . . . . . 6 (𝑡 = 𝑊 → (𝑡𝑈𝑊𝑈))
98 eqeq2 2743 . . . . . . . 8 (𝑡 = 𝑊 → ((𝐺 DProd 𝑠) = 𝑡 ↔ (𝐺 DProd 𝑠) = 𝑊))
9998anbi2d 629 . . . . . . 7 (𝑡 = 𝑊 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡) ↔ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))
10099rexbidv 3171 . . . . . 6 (𝑡 = 𝑊 → (∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡) ↔ ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))
10197, 100imbi12d 344 . . . . 5 (𝑡 = 𝑊 → ((𝑡𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)) ↔ (𝑊𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊))))
102 pgpfac.a . . . . 5 (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)))
1036simpld 495 . . . . 5 (𝜑𝑊 ∈ (SubGrp‘𝐺))
104101, 102, 103rspcdva 3583 . . . 4 (𝜑 → (𝑊𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))
10596, 104mpd 15 . . 3 (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊))
106 breq2 5114 . . . . 5 (𝑠 = 𝑎 → (𝐺dom DProd 𝑠𝐺dom DProd 𝑎))
107 oveq2 7370 . . . . . 6 (𝑠 = 𝑎 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑎))
108107eqeq1d 2733 . . . . 5 (𝑠 = 𝑎 → ((𝐺 DProd 𝑠) = 𝑊 ↔ (𝐺 DProd 𝑎) = 𝑊))
109106, 108anbi12d 631 . . . 4 (𝑠 = 𝑎 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊) ↔ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊)))
110109cbvrexvw 3224 . . 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 481 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐺 ∈ Abel)
114 pgpfac.p . . . 4 (𝜑𝑃 pGrp 𝐺)
115114adantr 481 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑃 pGrp 𝐺)
1168adantr 481 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐵 ∈ Fin)
1172adantr 481 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑈 ∈ (SubGrp‘𝐺))
118102adantr 481 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)))
119 pgpfac.e . . 3 𝐸 = (gEx‘𝐻)
12045adantr 481 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐸 ≠ 1)
12132adantr 481 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑋𝑈)
12244adantr 481 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → (𝑂𝑋) = 𝐸)
1231adantr 481 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑊 ∈ (SubGrp‘𝐻))
12481adantr 481 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })
12587adantr 481 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ((𝐾‘{𝑋}) 𝑊) = 𝑈)
126 simprl 769 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑎 ∈ Word 𝐶)
127 simprrl 779 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐺dom DProd 𝑎)
128 simprrr 780 . . 3 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → (𝐺 DProd 𝑎) = 𝑊)
129 eqid 2731 . . 3 (𝑎 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑎 ++ ⟨“(𝐾‘{𝑋})”⟩)
1309, 112, 113, 115, 116, 117, 118, 3, 26, 47, 119, 17, 79, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129pgpfaclem1 19874 . 2 ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
131111, 130rexlimddv 3154 1 (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2939  wral 3060  wrex 3069  {crab 3405  Vcvv 3446  cin 3912  wss 3913  wpss 3914  c0 4287  {csn 4591   class class class wbr 5110  dom cdm 5638  ran crn 5639  cfv 6501  (class class class)co 7362  csdm 8889  Fincfn 8890  cr 11059  0cc0 11060  1c1 11061   · cmul 11065   < clt 11198  cn 12162  0cn0 12422  chash 14240  Word cword 14414   ++ cconcat 14470  ⟨“cs1 14495  Basecbs 17094  s cress 17123  0gc0g 17335  Moorecmre 17476  mrClscmrc 17477  ACScacs 17479  Grpcgrp 18762  SubGrpcsubg 18936  Cntzccntz 19109  odcod 19320  gExcgex 19321   pGrp cpgp 19322  LSSumclsm 19430  Abelcabl 19577  CycGrpccyg 19668   DProd cdprd 19786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11116  ax-resscn 11117  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-mulcom 11124  ax-addass 11125  ax-mulass 11126  ax-distr 11127  ax-i2m1 11128  ax-1ne0 11129  ax-1rid 11130  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133  ax-pre-lttri 11134  ax-pre-lttrn 11135  ax-pre-ltadd 11136  ax-pre-mulgt0 11137
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-tpos 8162  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-er 8655  df-map 8774  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-sup 9387  df-inf 9388  df-oi 9455  df-dju 9846  df-card 9884  df-pnf 11200  df-mnf 11201  df-xr 11202  df-ltxr 11203  df-le 11204  df-sub 11396  df-neg 11397  df-nn 12163  df-2 12225  df-n0 12423  df-xnn0 12495  df-z 12509  df-uz 12773  df-fz 13435  df-fzo 13578  df-seq 13917  df-hash 14241  df-word 14415  df-concat 14471  df-s1 14496  df-sets 17047  df-slot 17065  df-ndx 17077  df-base 17095  df-ress 17124  df-plusg 17160  df-0g 17337  df-gsum 17338  df-mre 17480  df-mrc 17481  df-acs 17483  df-mgm 18511  df-sgrp 18560  df-mnd 18571  df-mhm 18615  df-submnd 18616  df-grp 18765  df-minusg 18766  df-sbg 18767  df-mulg 18887  df-subg 18939  df-ghm 19020  df-gim 19063  df-cntz 19111  df-oppg 19138  df-od 19324  df-pgp 19326  df-lsm 19432  df-pj1 19433  df-cmn 19578  df-abl 19579  df-cyg 19669  df-dprd 19788
This theorem is referenced by:  pgpfaclem3  19876
  Copyright terms: Public domain W3C validator