pgpfaclem2 - Metamath Proof Explorer

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

Theorem pgpfaclem2 20217

Description: Lemma for pgpfac 20219. (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 = (0_g‘𝐻)
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.

Step	Hyp	Ref	Expression
1		pgpfac.w	. . . . . . 7 ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻))
2		pgpfac.u	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))
3		pgpfac.h	. . . . . . . . 9 ⊢ 𝐻 = (𝐺 ↾_s 𝑈)
4	3	subsubg 19279	. . . . . . . 8 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝑊 ∈ (SubGrp‘𝐻) ↔ (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊 ⊆ 𝑈)))
5	2, 4	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑊 ∈ (SubGrp‘𝐻) ↔ (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊 ⊆ 𝑈)))
6	1, 5	mpbid 235	. . . . . 6 ⊢ (𝜑 → (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊 ⊆ 𝑈))
7	6	simprd 501	. . . . 5 ⊢ (𝜑 → 𝑊 ⊆ 𝑈)
8		pgpfac.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ Fin)
9		pgpfac.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝐺)
10	9	subgss 19256	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ 𝐵)
11	2, 10	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ⊆ 𝐵)
12	8, 11	ssfid 9243	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ Fin)
13	12, 7	ssfid 9243	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ Fin)
14		hashcl 14424	. . . . . . . . 9 ⊢ (𝑊 ∈ Fin → (♯‘𝑊) ∈ ℕ₀)
15	13, 14	syl 18	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑊) ∈ ℕ₀)
16	15	nn0red 12594	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑊) ∈ ℝ)
17		pgpfac.0	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘𝐻)
18	17	fvexi 6896	. . . . . . . . . . 11 ⊢ 0 ∈ V
19		hashsng 14437	. . . . . . . . . . 11 ⊢ ( 0 ∈ V → (♯‘{ 0 }) = 1)
20	18, 19	ax-mp 5	. . . . . . . . . 10 ⊢ (♯‘{ 0 }) = 1
21		subgrcl 19260	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ (SubGrp‘𝐻) → 𝐻 ∈ Grp)
22		eqid 2762	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝐻) = (Base‘𝐻)
23	22	subgacs 19290	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ Grp → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
24		acsmre 17746	. . . . . . . . . . . . . . . 16 ⊢ ((SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)) → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
25	1, 21, 23, 24	4syl 20	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
26		pgpfac.k	. . . . . . . . . . . . . . 15 ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻))
27	25, 26	mrcssvd 17717	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ (Base‘𝐻))
28	3	subgbas 19259	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻))
29	2, 28	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 = (Base‘𝐻))
30	27, 29	sseqtrrd 3971	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈)
31	12, 30	ssfid 9243	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ Fin)
32		pgpfac.x	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
33	32, 29	eleqtrd 2864	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻))
34	26	mrcsncl 17706	. . . . . . . . . . . . . . . 16 ⊢ (((SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
35	25, 33, 34	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
36	17	subg0cl 19263	. . . . . . . . . . . . . . 15 ⊢ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) → 0 ∈ (𝐾‘{𝑋}))
37	35, 36	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (𝐾‘{𝑋}))
38	37	snssd 4750	. . . . . . . . . . . . 13 ⊢ (𝜑 → { 0 } ⊆ (𝐾‘{𝑋}))
39	33	snssd 4750	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑋} ⊆ (Base‘𝐻))
40	25, 26, 39	mrcssidd 17719	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑋} ⊆ (𝐾‘{𝑋}))
41		snssg 4747	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝑈 → (𝑋 ∈ (𝐾‘{𝑋}) ↔ {𝑋} ⊆ (𝐾‘{𝑋})))
42	32, 41	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∈ (𝐾‘{𝑋}) ↔ {𝑋} ⊆ (𝐾‘{𝑋})))
43	40, 42	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ (𝐾‘{𝑋}))
44		pgpfac.oe	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑂‘𝑋) = 𝐸)
45		pgpfac.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 ≠ 1)
46	44, 45	eqnetrd 3024	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑂‘𝑋) ≠ 1)
47		pgpfac.o	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑂 = (od‘𝐻)
48	47, 17	od1 19692	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻 ∈ Grp → (𝑂‘ 0 ) = 1)
49	1, 21, 48	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑂‘ 0 ) = 1)
50		elsni 4604	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ { 0 } → 𝑋 = 0 )
51	50	fveqeq2d 6890	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ { 0 } → ((𝑂‘𝑋) = 1 ↔ (𝑂‘ 0 ) = 1))
52	49, 51	syl5ibrcom 250	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∈ { 0 } → (𝑂‘𝑋) = 1))
53	52	necon3ad 2970	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑂‘𝑋) ≠ 1 → ¬ 𝑋 ∈ { 0 }))
54	46, 53	mpd 16	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑋 ∈ { 0 })
55	38, 43, 54	ssnelpssd 4067	. . . . . . . . . . . 12 ⊢ (𝜑 → { 0 } ⊊ (𝐾‘{𝑋}))
56		php3 9207	. . . . . . . . . . . 12 ⊢ (((𝐾‘{𝑋}) ∈ Fin ∧ { 0 } ⊊ (𝐾‘{𝑋})) → { 0 } ≺ (𝐾‘{𝑋}))
57	31, 55, 56	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → { 0 } ≺ (𝐾‘{𝑋}))
58		snfi 9054	. . . . . . . . . . . 12 ⊢ { 0 } ∈ Fin
59		hashsdom 14449	. . . . . . . . . . . 12 ⊢ (({ 0 } ∈ Fin ∧ (𝐾‘{𝑋}) ∈ Fin) → ((♯‘{ 0 }) < (♯‘(𝐾‘{𝑋})) ↔ { 0 } ≺ (𝐾‘{𝑋})))
60	58, 31, 59	sylancr 599	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘{ 0 }) < (♯‘(𝐾‘{𝑋})) ↔ { 0 } ≺ (𝐾‘{𝑋})))
61	57, 60	mpbird 260	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘{ 0 }) < (♯‘(𝐾‘{𝑋})))
62	20, 61	eqbrtrrid 5145	. . . . . . . . 9 ⊢ (𝜑 → 1 < (♯‘(𝐾‘{𝑋})))
63		1red 11237	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℝ)
64		hashcl 14424	. . . . . . . . . . . 12 ⊢ ((𝐾‘{𝑋}) ∈ Fin → (♯‘(𝐾‘{𝑋})) ∈ ℕ₀)
65	31, 64	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(𝐾‘{𝑋})) ∈ ℕ₀)
66	65	nn0red 12594	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(𝐾‘{𝑋})) ∈ ℝ)
67	17	subg0cl 19263	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ (SubGrp‘𝐻) → 0 ∈ 𝑊)
68		ne0i 4290	. . . . . . . . . . . . 13 ⊢ ( 0 ∈ 𝑊 → 𝑊 ≠ ∅)
69	1, 67, 68	3syl 19	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 ≠ ∅)
70		hashnncl 14434	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ Fin → ((♯‘𝑊) ∈ ℕ ↔ 𝑊 ≠ ∅))
71	13, 70	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝑊) ∈ ℕ ↔ 𝑊 ≠ ∅))
72	69, 71	mpbird 260	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑊) ∈ ℕ)
73	72	nngt0d 12313	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (♯‘𝑊))
74		ltmul1 12093	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ (♯‘(𝐾‘{𝑋})) ∈ ℝ ∧ ((♯‘𝑊) ∈ ℝ ∧ 0 < (♯‘𝑊))) → (1 < (♯‘(𝐾‘{𝑋})) ↔ (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊))))
75	63, 66, 16, 73, 74	syl112anc 1401	. . . . . . . . 9 ⊢ (𝜑 → (1 < (♯‘(𝐾‘{𝑋})) ↔ (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊))))
76	62, 75	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)))
77	16	recnd 11265	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝑊) ∈ ℂ)
78	77	mullidd 11255	. . . . . . . 8 ⊢ (𝜑 → (1 · (♯‘𝑊)) = (♯‘𝑊))
79		pgpfac.l	. . . . . . . . . 10 ⊢ ⊕ = (LSSum‘𝐻)
80		eqid 2762	. . . . . . . . . 10 ⊢ (Cntz‘𝐻) = (Cntz‘𝐻)
81		pgpfac.i	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })
82		pgpfac.g	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 ∈ Abel)
83	3	subgabl 19969	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Abel ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Abel)
84	82, 2, 83	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ Abel)
85	80, 84, 35, 1	ablcntzd 19990	. . . . . . . . . 10 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ ((Cntz‘𝐻)‘𝑊))
86	79, 17, 80, 35, 1, 81, 85, 31, 13	lsmhash 19838	. . . . . . . . 9 ⊢ (𝜑 → (♯‘((𝐾‘{𝑋}) ⊕ 𝑊)) = ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)))
87		pgpfac.s	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈)
88	87	fveq2d 6886	. . . . . . . . 9 ⊢ (𝜑 → (♯‘((𝐾‘{𝑋}) ⊕ 𝑊)) = (♯‘𝑈))
89	86, 88	eqtr3d 2799	. . . . . . . 8 ⊢ (𝜑 → ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)) = (♯‘𝑈))
90	76, 78, 89	3brtr3d 5140	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑊) < (♯‘𝑈))
91	16, 90	ltned 11374	. . . . . 6 ⊢ (𝜑 → (♯‘𝑊) ≠ (♯‘𝑈))
92		fveq2 6882	. . . . . . 7 ⊢ (𝑊 = 𝑈 → (♯‘𝑊) = (♯‘𝑈))
93	92	necon3i 2989	. . . . . 6 ⊢ ((♯‘𝑊) ≠ (♯‘𝑈) → 𝑊 ≠ 𝑈)
94	91, 93	syl 18	. . . . 5 ⊢ (𝜑 → 𝑊 ≠ 𝑈)
95		df-pss 3922	. . . . 5 ⊢ (𝑊 ⊊ 𝑈 ↔ (𝑊 ⊆ 𝑈 ∧ 𝑊 ≠ 𝑈))
96	7, 94, 95	sylanbrc 595	. . . 4 ⊢ (𝜑 → 𝑊 ⊊ 𝑈)
97		psseq1 4041	. . . . . 6 ⊢ (𝑡 = 𝑊 → (𝑡 ⊊ 𝑈 ↔ 𝑊 ⊊ 𝑈))
98		eqeq2 2774	. . . . . . . 8 ⊢ (𝑡 = 𝑊 → ((𝐺 DProd 𝑠) = 𝑡 ↔ (𝐺 DProd 𝑠) = 𝑊))
99	98	anbi2d 642	. . . . . . 7 ⊢ (𝑡 = 𝑊 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡) ↔ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))
100	99	rexbidv 3188	. . . . . 6 ⊢ (𝑡 = 𝑊 → (∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡) ↔ ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))
101	97, 100	imbi12d 347	. . . . 5 ⊢ (𝑡 = 𝑊 → ((𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)) ↔ (𝑊 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊))))
102		pgpfac.a	. . . . 5 ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)))
103	6	simpld 500	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))
104	101, 102, 103	rspcdva 3580	. . . 4 ⊢ (𝜑 → (𝑊 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))
105	96, 104	mpd 16	. . 3 ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊))
106		breq2 5111	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑎))
107		oveq2 7425	. . . . . 6 ⊢ (𝑠 = 𝑎 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑎))
108	107	eqeq1d 2764	. . . . 5 ⊢ (𝑠 = 𝑎 → ((𝐺 DProd 𝑠) = 𝑊 ↔ (𝐺 DProd 𝑎) = 𝑊))
109	106, 108	anbi12d 644	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊) ↔ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊)))
110	109	cbvrexvw 3243	. . 3 ⊢ (∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊) ↔ ∃𝑎 ∈ Word 𝐶(𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))
111	105, 110	sylib 221	. 2 ⊢ (𝜑 → ∃𝑎 ∈ Word 𝐶(𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))
112		pgpfac.c	. . 3 ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾_s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
113	82	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐺 ∈ Abel)
114		pgpfac.p	. . . 4 ⊢ (𝜑 → 𝑃 pGrp 𝐺)
115	114	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑃 pGrp 𝐺)
116	8	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐵 ∈ Fin)
117	2	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑈 ∈ (SubGrp‘𝐺))
118	102	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)))
119		pgpfac.e	. . 3 ⊢ 𝐸 = (gEx‘𝐻)
120	45	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐸 ≠ 1)
121	32	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑋 ∈ 𝑈)
122	44	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → (𝑂‘𝑋) = 𝐸)
123	1	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑊 ∈ (SubGrp‘𝐻))
124	81	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })
125	87	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈)
126		simprl 783	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑎 ∈ Word 𝐶)
127		simprrl 793	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐺dom DProd 𝑎)
128		simprrr 794	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → (𝐺 DProd 𝑎) = 𝑊)
129		eqid 2762	. . 3 ⊢ (𝑎 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑎 ++ ⟨“(𝐾‘{𝑋})”⟩)
130	9, 112, 113, 115, 116, 117, 118, 3, 26, 47, 119, 17, 79, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129	pgpfaclem1 20216	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
131	111, 130	rexlimddv 3171	1 ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 {crab 3414 Vcvv 3453 ∩ cin 3901 ⊆ wss 3902 ⊊ wpss 3903 ∅c0 4282 {csn 4587 class class class wbr 5107 dom cdm 5659 ran crn 5660 ‘cfv 6537 (class class class)co 7417 ≺ csdm 8955 Fincfn 8956 ℝcr 11127 0cc0 11128 1c1 11129 · cmul 11133 < clt 11271 ℕcn 12261 ℕ₀cn0 12532 ♯chash 14398 Word cword 14582 ++ cconcat 14639 ⟨“cs1 14666 Basecbs 17307 ↾_s cress 17328 0_gc0g 17530 Moorecmre 17672 mrClscmrc 17673 ACScacs 17675 Grpcgrp 19063 SubGrpcsubg 19249 Cntzccntz 19448 odcod 19657 gExcgex 19658 pGrp cpgp 19659 LSSumclsm 19767 Abelcabl 19914 CycGrpccyg 20010 DProd cdprd 20128

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8163 df-tpos 8228 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-oadd 8463 df-er 8700 df-map 8832 df-ixp 8909 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fsupp 9336 df-sup 9416 df-inf 9417 df-oi 9486 df-dju 9910 df-card 9948 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-nn 12262 df-2 12331 df-n0 12533 df-xnn0 12606 df-z 12620 df-uz 12892 df-fz 13566 df-fzo 13714 df-seq 14070 df-hash 14399 df-word 14583 df-concat 14640 df-s1 14667 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-0g 17532 df-gsum 17533 df-mre 17676 df-mrc 17677 df-acs 17679 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-mhm 18897 df-submnd 18898 df-grp 19066 df-minusg 19067 df-sbg 19068 df-mulg 19197 df-subg 19252 df-ghm 19347 df-gim 19392 df-cntz 19450 df-oppg 19479 df-od 19661 df-pgp 19663 df-lsm 19769 df-pj1 19770 df-cmn 19915 df-abl 19916 df-cyg 20011 df-dprd 20130

This theorem is used by: pgpfaclem3 20218

W3C validator