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 20331

Description: Lemma for pgpfac 20333. (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 19392	. . . . . . . 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 19369	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ 𝐵)
11	2, 10	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ⊆ 𝐵)
12	8, 11	ssfid 9291	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ Fin)
13	12, 7	ssfid 9291	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ Fin)
14		hashcl 14530	. . . . . . . . 9 ⊢ (𝑊 ∈ Fin → (♯‘𝑊) ∈ ℕ₀)
15	13, 14	syl 18	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑊) ∈ ℕ₀)
16	15	nn0red 12698	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑊) ∈ ℝ)
17		pgpfac.0	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘𝐻)
18	17	fvexi 6925	. . . . . . . . . . 11 ⊢ 0 ∈ V
19		hashsng 14543	. . . . . . . . . . 11 ⊢ ( 0 ∈ V → (♯‘{ 0 }) = 1)
20	18, 19	ax-mp 5	. . . . . . . . . 10 ⊢ (♯‘{ 0 }) = 1
21		subgrcl 19373	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ (SubGrp‘𝐻) → 𝐻 ∈ Grp)
22		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝐻) = (Base‘𝐻)
23	22	subgacs 19403	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ Grp → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
24		acsmre 17858	. . . . . . . . . . . . . . . 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 17829	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ (Base‘𝐻))
28	3	subgbas 19372	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻))
29	2, 28	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 = (Base‘𝐻))
30	27, 29	sseqtrrd 3950	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈)
31	12, 30	ssfid 9291	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ Fin)
32		pgpfac.x	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
33	32, 29	eleqtrd 2866	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻))
34	26	mrcsncl 17818	. . . . . . . . . . . . . . . 16 ⊢ (((SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
35	25, 33, 34	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
36	17	subg0cl 19376	. . . . . . . . . . . . . . 15 ⊢ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) → 0 ∈ (𝐾‘{𝑋}))
37	35, 36	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (𝐾‘{𝑋}))
38	37	snssd 4747	. . . . . . . . . . . . 13 ⊢ (𝜑 → { 0 } ⊆ (𝐾‘{𝑋}))
39	33	snssd 4747	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑋} ⊆ (Base‘𝐻))
40	25, 26, 39	mrcssidd 17831	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑋} ⊆ (𝐾‘{𝑋}))
41		snssg 4744	. . . . . . . . . . . . . . 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 3026	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑂‘𝑋) ≠ 1)
47		pgpfac.o	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑂 = (od‘𝐻)
48	47, 17	od1 19806	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻 ∈ Grp → (𝑂‘ 0 ) = 1)
49	1, 21, 48	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑂‘ 0 ) = 1)
50		elsni 4601	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ { 0 } → 𝑋 = 0 )
51	50	fveqeq2d 6919	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ { 0 } → ((𝑂‘𝑋) = 1 ↔ (𝑂‘ 0 ) = 1))
52	49, 51	syl5ibrcom 250	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∈ { 0 } → (𝑂‘𝑋) = 1))
53	52	necon3ad 2972	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑂‘𝑋) ≠ 1 → ¬ 𝑋 ∈ { 0 }))
54	46, 53	mpd 16	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑋 ∈ { 0 })
55	38, 43, 54	ssnelpssd 4046	. . . . . . . . . . . 12 ⊢ (𝜑 → { 0 } ⊊ (𝐾‘{𝑋}))
56		php3 9255	. . . . . . . . . . . 12 ⊢ (((𝐾‘{𝑋}) ∈ Fin ∧ { 0 } ⊊ (𝐾‘{𝑋})) → { 0 } ≺ (𝐾‘{𝑋}))
57	31, 55, 56	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → { 0 } ≺ (𝐾‘{𝑋}))
58		snfi 9102	. . . . . . . . . . . 12 ⊢ { 0 } ∈ Fin
59		hashsdom 14555	. . . . . . . . . . . 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 11339	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℝ)
64		hashcl 14530	. . . . . . . . . . . 12 ⊢ ((𝐾‘{𝑋}) ∈ Fin → (♯‘(𝐾‘{𝑋})) ∈ ℕ₀)
65	31, 64	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(𝐾‘{𝑋})) ∈ ℕ₀)
66	65	nn0red 12698	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(𝐾‘{𝑋})) ∈ ℝ)
67	17	subg0cl 19376	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ (SubGrp‘𝐻) → 0 ∈ 𝑊)
68		ne0i 4290	. . . . . . . . . . . . 13 ⊢ ( 0 ∈ 𝑊 → 𝑊 ≠ ∅)
69	1, 67, 68	3syl 19	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 ≠ ∅)
70		hashnncl 14540	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ Fin → ((♯‘𝑊) ∈ ℕ ↔ 𝑊 ≠ ∅))
71	13, 70	syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝑊) ∈ ℕ ↔ 𝑊 ≠ ∅))
72	69, 71	mpbird 260	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑊) ∈ ℕ)
73	72	nngt0d 12417	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (♯‘𝑊))
74		ltmul1 12197	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ (♯‘(𝐾‘{𝑋})) ∈ ℝ ∧ ((♯‘𝑊) ∈ ℝ ∧ 0 < (♯‘𝑊))) → (1 < (♯‘(𝐾‘{𝑋})) ↔ (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊))))
75	63, 66, 16, 73, 74	syl112anc 1402	. . . . . . . . 9 ⊢ (𝜑 → (1 < (♯‘(𝐾‘{𝑋})) ↔ (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊))))
76	62, 75	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)))
77	16	recnd 11367	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝑊) ∈ ℂ)
78	77	mullidd 11357	. . . . . . . 8 ⊢ (𝜑 → (1 · (♯‘𝑊)) = (♯‘𝑊))
79		pgpfac.l	. . . . . . . . . 10 ⊢ ⊕ = (LSSum‘𝐻)
80		eqid 2763	. . . . . . . . . 10 ⊢ (Cntz‘𝐻) = (Cntz‘𝐻)
81		pgpfac.i	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })
82		pgpfac.g	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 ∈ Abel)
83	3	subgabl 20083	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Abel ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Abel)
84	82, 2, 83	syl2anc 596	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ Abel)
85	80, 84, 35, 1	ablcntzd 20104	. . . . . . . . . 10 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ ((Cntz‘𝐻)‘𝑊))
86	79, 17, 80, 35, 1, 81, 85, 31, 13	lsmhash 19952	. . . . . . . . 9 ⊢ (𝜑 → (♯‘((𝐾‘{𝑋}) ⊕ 𝑊)) = ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)))
87		pgpfac.s	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈)
88	87	fveq2d 6915	. . . . . . . . 9 ⊢ (𝜑 → (♯‘((𝐾‘{𝑋}) ⊕ 𝑊)) = (♯‘𝑈))
89	86, 88	eqtr3d 2800	. . . . . . . 8 ⊢ (𝜑 → ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)) = (♯‘𝑈))
90	76, 78, 89	3brtr3d 5140	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑊) < (♯‘𝑈))
91	16, 90	ltned 11476	. . . . . 6 ⊢ (𝜑 → (♯‘𝑊) ≠ (♯‘𝑈))
92		fveq2 6911	. . . . . . 7 ⊢ (𝑊 = 𝑈 → (♯‘𝑊) = (♯‘𝑈))
93	92	necon3i 2991	. . . . . 6 ⊢ ((♯‘𝑊) ≠ (♯‘𝑈) → 𝑊 ≠ 𝑈)
94	91, 93	syl 18	. . . . 5 ⊢ (𝜑 → 𝑊 ≠ 𝑈)
95		df-pss 4017	. . . . 5 ⊢ (𝑊 ⊊ 𝑈 ↔ (𝑊 ⊆ 𝑈 ∧ 𝑊 ≠ 𝑈))
96	7, 94, 95	sylanbrc 595	. . . 4 ⊢ (𝜑 → 𝑊 ⊊ 𝑈)
97		psseq1 4020	. . . . . 6 ⊢ (𝑡 = 𝑊 → (𝑡 ⊊ 𝑈 ↔ 𝑊 ⊊ 𝑈))
98		eqeq2 2775	. . . . . . . 8 ⊢ (𝑡 = 𝑊 → ((𝐺 DProd 𝑠) = 𝑡 ↔ (𝐺 DProd 𝑠) = 𝑊))
99	98	anbi2d 642	. . . . . . 7 ⊢ (𝑡 = 𝑊 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡) ↔ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))
100	99	rexbidv 3190	. . . . . 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 3581	. . . 4 ⊢ (𝜑 → (𝑊 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))
105	96, 104	mpd 16	. . 3 ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊))
106		breq2 5110	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑎))
107		oveq2 7454	. . . . . 6 ⊢ (𝑠 = 𝑎 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑎))
108	107	eqeq1d 2765	. . . . 5 ⊢ (𝑠 = 𝑎 → ((𝐺 DProd 𝑠) = 𝑊 ↔ (𝐺 DProd 𝑎) = 𝑊))
109	106, 108	anbi12d 644	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊) ↔ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊)))
110	109	cbvrexvw 3245	. . 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 2763	. . 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 20330	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
131	111, 130	rexlimddv 3173	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 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 {crab 3416 Vcvv 3454 ⊆ wss 3900 ⊊ wpss 4016 ∩ cin 4092 ∅c0 4281 {csn 4588 class class class wbr 5106 dom cdm 5656 ran crn 5657 ‘cfv 6561 (class class class)co 7446 ≺ csdm 9003 Fincfn 9004 ℝcr 11229 0cc0 11230 1c1 11231 · cmul 11235 < clt 11373 ℕcn 12365 ℕ₀cn0 12636 ♯chash 14504 Word cword 14688 ++ cconcat 14745 ⟨“cs1 14772 Basecbs 17419 ↾_s cress 17440 0_gc0g 17642 Moorecmre 17784 mrClscmrc 17785 ACScacs 17787 Grpcgrp 19176 SubGrpcsubg 19362 Cntzccntz 19562 odcod 19771 gExcgex 19772 pGrp cpgp 19773 LSSumclsm 19881 Abelcabl 20028 CycGrpccyg 20124 DProd cdprd 20242

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-of 7720 df-om 7905 df-1st 8028 df-2nd 8029 df-supp 8208 df-tpos 8274 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-2o 8508 df-oadd 8511 df-er 8748 df-map 8880 df-ixp 8957 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-fsupp 9385 df-sup 9464 df-inf 9465 df-oi 9534 df-dju 10012 df-card 10050 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-nn 12366 df-2 12435 df-n0 12637 df-xnn0 12710 df-z 12724 df-uz 12996 df-fz 13670 df-fzo 13819 df-seq 14175 df-hash 14505 df-word 14689 df-concat 14746 df-s1 14773 df-sets 17374 df-slot 17392 df-ndx 17404 df-base 17420 df-ress 17441 df-plusg 17473 df-0g 17644 df-gsum 17645 df-mre 17788 df-mrc 17789 df-acs 17791 df-mgm 18848 df-sgrp 18940 df-mnd 18956 df-mhm 19010 df-submnd 19011 df-grp 19179 df-minusg 19180 df-sbg 19181 df-mulg 19310 df-subg 19365 df-ghm 19460 df-gim 19505 df-cntz 19564 df-oppg 19593 df-od 19775 df-pgp 19777 df-lsm 19883 df-pj1 19884 df-cmn 20029 df-abl 20030 df-cyg 20125 df-dprd 20244

This theorem is used by: pgpfaclem3 20332

W3C validator