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 19989

Description: Lemma for pgpfac 19991. (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 19054	. . . . . . . 8 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝑊 ∈ (SubGrp‘𝐻) ↔ (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊 ⊆ 𝑈)))
5	2, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑊 ∈ (SubGrp‘𝐻) ↔ (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊 ⊆ 𝑈)))
6	1, 5	mpbid 232	. . . . . 6 ⊢ (𝜑 → (𝑊 ∈ (SubGrp‘𝐺) ∧ 𝑊 ⊆ 𝑈))
7	6	simprd 495	. . . . 5 ⊢ (𝜑 → 𝑊 ⊆ 𝑈)
8		pgpfac.f	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ Fin)
9		pgpfac.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝐺)
10	9	subgss 19032	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 ⊆ 𝐵)
11	2, 10	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ⊆ 𝐵)
12	8, 11	ssfid 9148	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ Fin)
13	12, 7	ssfid 9148	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ Fin)
14		hashcl 14255	. . . . . . . . 9 ⊢ (𝑊 ∈ Fin → (♯‘𝑊) ∈ ℕ₀)
15	13, 14	syl 17	. . . . . . . 8 ⊢ (𝜑 → (♯‘𝑊) ∈ ℕ₀)
16	15	nn0red 12435	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑊) ∈ ℝ)
17		pgpfac.0	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘𝐻)
18	17	fvexi 6831	. . . . . . . . . . 11 ⊢ 0 ∈ V
19		hashsng 14268	. . . . . . . . . . 11 ⊢ ( 0 ∈ V → (♯‘{ 0 }) = 1)
20	18, 19	ax-mp 5	. . . . . . . . . 10 ⊢ (♯‘{ 0 }) = 1
21		subgrcl 19036	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 ∈ (SubGrp‘𝐻) → 𝐻 ∈ Grp)
22		eqid 2730	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝐻) = (Base‘𝐻)
23	22	subgacs 19066	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ Grp → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
24		acsmre 17550	. . . . . . . . . . . . . . . 16 ⊢ ((SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)) → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
25	1, 21, 23, 24	4syl 19	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
26		pgpfac.k	. . . . . . . . . . . . . . 15 ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻))
27	25, 26	mrcssvd 17521	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ (Base‘𝐻))
28	3	subgbas 19035	. . . . . . . . . . . . . . 15 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻))
29	2, 28	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 = (Base‘𝐻))
30	27, 29	sseqtrrd 3970	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈)
31	12, 30	ssfid 9148	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ Fin)
32		pgpfac.x	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
33	32, 29	eleqtrd 2831	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻))
34	26	mrcsncl 17510	. . . . . . . . . . . . . . . 16 ⊢ (((SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
35	25, 33, 34	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
36	17	subg0cl 19039	. . . . . . . . . . . . . . 15 ⊢ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) → 0 ∈ (𝐾‘{𝑋}))
37	35, 36	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (𝐾‘{𝑋}))
38	37	snssd 4759	. . . . . . . . . . . . 13 ⊢ (𝜑 → { 0 } ⊆ (𝐾‘{𝑋}))
39	33	snssd 4759	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → {𝑋} ⊆ (Base‘𝐻))
40	25, 26, 39	mrcssidd 17523	. . . . . . . . . . . . . 14 ⊢ (𝜑 → {𝑋} ⊆ (𝐾‘{𝑋}))
41		snssg 4734	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝑈 → (𝑋 ∈ (𝐾‘{𝑋}) ↔ {𝑋} ⊆ (𝐾‘{𝑋})))
42	32, 41	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ∈ (𝐾‘{𝑋}) ↔ {𝑋} ⊆ (𝐾‘{𝑋})))
43	40, 42	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ (𝐾‘{𝑋}))
44		pgpfac.oe	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑂‘𝑋) = 𝐸)
45		pgpfac.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐸 ≠ 1)
46	44, 45	eqnetrd 2993	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑂‘𝑋) ≠ 1)
47		pgpfac.o	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑂 = (od‘𝐻)
48	47, 17	od1 19464	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻 ∈ Grp → (𝑂‘ 0 ) = 1)
49	1, 21, 48	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑂‘ 0 ) = 1)
50		elsni 4591	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ { 0 } → 𝑋 = 0 )
51	50	fveqeq2d 6825	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ { 0 } → ((𝑂‘𝑋) = 1 ↔ (𝑂‘ 0 ) = 1))
52	49, 51	syl5ibrcom 247	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑋 ∈ { 0 } → (𝑂‘𝑋) = 1))
53	52	necon3ad 2939	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑂‘𝑋) ≠ 1 → ¬ 𝑋 ∈ { 0 }))
54	46, 53	mpd 15	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ 𝑋 ∈ { 0 })
55	38, 43, 54	ssnelpssd 4063	. . . . . . . . . . . 12 ⊢ (𝜑 → { 0 } ⊊ (𝐾‘{𝑋}))
56		php3 9113	. . . . . . . . . . . 12 ⊢ (((𝐾‘{𝑋}) ∈ Fin ∧ { 0 } ⊊ (𝐾‘{𝑋})) → { 0 } ≺ (𝐾‘{𝑋}))
57	31, 55, 56	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → { 0 } ≺ (𝐾‘{𝑋}))
58		snfi 8960	. . . . . . . . . . . 12 ⊢ { 0 } ∈ Fin
59		hashsdom 14280	. . . . . . . . . . . 12 ⊢ (({ 0 } ∈ Fin ∧ (𝐾‘{𝑋}) ∈ Fin) → ((♯‘{ 0 }) < (♯‘(𝐾‘{𝑋})) ↔ { 0 } ≺ (𝐾‘{𝑋})))
60	58, 31, 59	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → ((♯‘{ 0 }) < (♯‘(𝐾‘{𝑋})) ↔ { 0 } ≺ (𝐾‘{𝑋})))
61	57, 60	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘{ 0 }) < (♯‘(𝐾‘{𝑋})))
62	20, 61	eqbrtrrid 5125	. . . . . . . . 9 ⊢ (𝜑 → 1 < (♯‘(𝐾‘{𝑋})))
63		1red 11105	. . . . . . . . . 10 ⊢ (𝜑 → 1 ∈ ℝ)
64		hashcl 14255	. . . . . . . . . . . 12 ⊢ ((𝐾‘{𝑋}) ∈ Fin → (♯‘(𝐾‘{𝑋})) ∈ ℕ₀)
65	31, 64	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘(𝐾‘{𝑋})) ∈ ℕ₀)
66	65	nn0red 12435	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘(𝐾‘{𝑋})) ∈ ℝ)
67	17	subg0cl 19039	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ (SubGrp‘𝐻) → 0 ∈ 𝑊)
68		ne0i 4289	. . . . . . . . . . . . 13 ⊢ ( 0 ∈ 𝑊 → 𝑊 ≠ ∅)
69	1, 67, 68	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 ≠ ∅)
70		hashnncl 14265	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ Fin → ((♯‘𝑊) ∈ ℕ ↔ 𝑊 ≠ ∅))
71	13, 70	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → ((♯‘𝑊) ∈ ℕ ↔ 𝑊 ≠ ∅))
72	69, 71	mpbird 257	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑊) ∈ ℕ)
73	72	nngt0d 12166	. . . . . . . . . 10 ⊢ (𝜑 → 0 < (♯‘𝑊))
74		ltmul1 11963	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ (♯‘(𝐾‘{𝑋})) ∈ ℝ ∧ ((♯‘𝑊) ∈ ℝ ∧ 0 < (♯‘𝑊))) → (1 < (♯‘(𝐾‘{𝑋})) ↔ (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊))))
75	63, 66, 16, 73, 74	syl112anc 1376	. . . . . . . . 9 ⊢ (𝜑 → (1 < (♯‘(𝐾‘{𝑋})) ↔ (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊))))
76	62, 75	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → (1 · (♯‘𝑊)) < ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)))
77	16	recnd 11132	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝑊) ∈ ℂ)
78	77	mullidd 11122	. . . . . . . 8 ⊢ (𝜑 → (1 · (♯‘𝑊)) = (♯‘𝑊))
79		pgpfac.l	. . . . . . . . . 10 ⊢ ⊕ = (LSSum‘𝐻)
80		eqid 2730	. . . . . . . . . 10 ⊢ (Cntz‘𝐻) = (Cntz‘𝐻)
81		pgpfac.i	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })
82		pgpfac.g	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 ∈ Abel)
83	3	subgabl 19741	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Abel ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Abel)
84	82, 2, 83	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ∈ Abel)
85	80, 84, 35, 1	ablcntzd 19762	. . . . . . . . . 10 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ ((Cntz‘𝐻)‘𝑊))
86	79, 17, 80, 35, 1, 81, 85, 31, 13	lsmhash 19610	. . . . . . . . 9 ⊢ (𝜑 → (♯‘((𝐾‘{𝑋}) ⊕ 𝑊)) = ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)))
87		pgpfac.s	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈)
88	87	fveq2d 6821	. . . . . . . . 9 ⊢ (𝜑 → (♯‘((𝐾‘{𝑋}) ⊕ 𝑊)) = (♯‘𝑈))
89	86, 88	eqtr3d 2767	. . . . . . . 8 ⊢ (𝜑 → ((♯‘(𝐾‘{𝑋})) · (♯‘𝑊)) = (♯‘𝑈))
90	76, 78, 89	3brtr3d 5120	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑊) < (♯‘𝑈))
91	16, 90	ltned 11241	. . . . . 6 ⊢ (𝜑 → (♯‘𝑊) ≠ (♯‘𝑈))
92		fveq2 6817	. . . . . . 7 ⊢ (𝑊 = 𝑈 → (♯‘𝑊) = (♯‘𝑈))
93	92	necon3i 2958	. . . . . 6 ⊢ ((♯‘𝑊) ≠ (♯‘𝑈) → 𝑊 ≠ 𝑈)
94	91, 93	syl 17	. . . . 5 ⊢ (𝜑 → 𝑊 ≠ 𝑈)
95		df-pss 3920	. . . . 5 ⊢ (𝑊 ⊊ 𝑈 ↔ (𝑊 ⊆ 𝑈 ∧ 𝑊 ≠ 𝑈))
96	7, 94, 95	sylanbrc 583	. . . 4 ⊢ (𝜑 → 𝑊 ⊊ 𝑈)
97		psseq1 4038	. . . . . 6 ⊢ (𝑡 = 𝑊 → (𝑡 ⊊ 𝑈 ↔ 𝑊 ⊊ 𝑈))
98		eqeq2 2742	. . . . . . . 8 ⊢ (𝑡 = 𝑊 → ((𝐺 DProd 𝑠) = 𝑡 ↔ (𝐺 DProd 𝑠) = 𝑊))
99	98	anbi2d 630	. . . . . . 7 ⊢ (𝑡 = 𝑊 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡) ↔ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))
100	99	rexbidv 3154	. . . . . 6 ⊢ (𝑡 = 𝑊 → (∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡) ↔ ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))
101	97, 100	imbi12d 344	. . . . 5 ⊢ (𝑡 = 𝑊 → ((𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)) ↔ (𝑊 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊))))
102		pgpfac.a	. . . . 5 ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)))
103	6	simpld 494	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))
104	101, 102, 103	rspcdva 3576	. . . 4 ⊢ (𝜑 → (𝑊 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊)))
105	96, 104	mpd 15	. . 3 ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊))
106		breq2 5093	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑎))
107		oveq2 7349	. . . . . 6 ⊢ (𝑠 = 𝑎 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑎))
108	107	eqeq1d 2732	. . . . 5 ⊢ (𝑠 = 𝑎 → ((𝐺 DProd 𝑠) = 𝑊 ↔ (𝐺 DProd 𝑎) = 𝑊))
109	106, 108	anbi12d 632	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊) ↔ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊)))
110	109	cbvrexvw 3209	. . 3 ⊢ (∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑊) ↔ ∃𝑎 ∈ Word 𝐶(𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))
111	105, 110	sylib 218	. 2 ⊢ (𝜑 → ∃𝑎 ∈ Word 𝐶(𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))
112		pgpfac.c	. . 3 ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾_s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
113	82	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐺 ∈ Abel)
114		pgpfac.p	. . . 4 ⊢ (𝜑 → 𝑃 pGrp 𝐺)
115	114	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑃 pGrp 𝐺)
116	8	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐵 ∈ Fin)
117	2	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑈 ∈ (SubGrp‘𝐺))
118	102	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡)))
119		pgpfac.e	. . 3 ⊢ 𝐸 = (gEx‘𝐻)
120	45	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐸 ≠ 1)
121	32	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑋 ∈ 𝑈)
122	44	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → (𝑂‘𝑋) = 𝐸)
123	1	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑊 ∈ (SubGrp‘𝐻))
124	81	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })
125	87	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈)
126		simprl 770	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝑎 ∈ Word 𝐶)
127		simprrl 780	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → 𝐺dom DProd 𝑎)
128		simprrr 781	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → (𝐺 DProd 𝑎) = 𝑊)
129		eqid 2730	. . 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 19988	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑎 ∧ (𝐺 DProd 𝑎) = 𝑊))) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
131	111, 130	rexlimddv 3137	1 ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2110 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 {crab 3393 Vcvv 3434 ∩ cin 3899 ⊆ wss 3900 ⊊ wpss 3901 ∅c0 4281 {csn 4574 class class class wbr 5089 dom cdm 5614 ran crn 5615 ‘cfv 6477 (class class class)co 7341 ≺ csdm 8863 Fincfn 8864 ℝcr 10997 0cc0 10998 1c1 10999 · cmul 11003 < clt 11138 ℕcn 12117 ℕ₀cn0 12373 ♯chash 14229 Word cword 14412 ++ cconcat 14469 ⟨“cs1 14495 Basecbs 17112 ↾_s cress 17133 0_gc0g 17335 Moorecmre 17476 mrClscmrc 17477 ACScacs 17479 Grpcgrp 18838 SubGrpcsubg 19025 Cntzccntz 19220 odcod 19429 gExcgex 19430 pGrp cpgp 19431 LSSumclsm 19539 Abelcabl 19686 CycGrpccyg 19782 DProd cdprd 19900

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2112 ax-9 2120 ax-10 2143 ax-11 2159 ax-12 2179 ax-ext 2702 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7663 ax-cnex 11054 ax-resscn 11055 ax-1cn 11056 ax-icn 11057 ax-addcl 11058 ax-addrcl 11059 ax-mulcl 11060 ax-mulrcl 11061 ax-mulcom 11062 ax-addass 11063 ax-mulass 11064 ax-distr 11065 ax-i2m1 11066 ax-1ne0 11067 ax-1rid 11068 ax-rnegex 11069 ax-rrecex 11070 ax-cnre 11071 ax-pre-lttri 11072 ax-pre-lttrn 11073 ax-pre-ltadd 11074 ax-pre-mulgt0 11075

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3344 df-reu 3345 df-rab 3394 df-v 3436 df-sbc 3740 df-csb 3849 df-dif 3903 df-un 3905 df-in 3907 df-ss 3917 df-pss 3920 df-nul 4282 df-if 4474 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4858 df-int 4896 df-iun 4941 df-iin 4942 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6244 df-ord 6305 df-on 6306 df-lim 6307 df-suc 6308 df-iota 6433 df-fun 6479 df-fn 6480 df-f 6481 df-f1 6482 df-fo 6483 df-f1o 6484 df-fv 6485 df-isom 6486 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-of 7605 df-om 7792 df-1st 7916 df-2nd 7917 df-supp 8086 df-tpos 8151 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-2o 8381 df-oadd 8384 df-er 8617 df-map 8747 df-ixp 8817 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-fsupp 9241 df-sup 9321 df-inf 9322 df-oi 9391 df-dju 9786 df-card 9824 df-pnf 11140 df-mnf 11141 df-xr 11142 df-ltxr 11143 df-le 11144 df-sub 11338 df-neg 11339 df-nn 12118 df-2 12180 df-n0 12374 df-xnn0 12447 df-z 12461 df-uz 12725 df-fz 13400 df-fzo 13547 df-seq 13901 df-hash 14230 df-word 14413 df-concat 14470 df-s1 14496 df-sets 17067 df-slot 17085 df-ndx 17097 df-base 17113 df-ress 17134 df-plusg 17166 df-0g 17337 df-gsum 17338 df-mre 17480 df-mrc 17481 df-acs 17483 df-mgm 18540 df-sgrp 18619 df-mnd 18635 df-mhm 18683 df-submnd 18684 df-grp 18841 df-minusg 18842 df-sbg 18843 df-mulg 18973 df-subg 19028 df-ghm 19118 df-gim 19164 df-cntz 19222 df-oppg 19251 df-od 19433 df-pgp 19435 df-lsm 19541 df-pj1 19542 df-cmn 19687 df-abl 19688 df-cyg 19783 df-dprd 19902

This theorem is referenced by: pgpfaclem3 19990

W3C validator