Theorem pgpfaclem2

Description: Lemma for pgpfac . (Contributed by Mario Carneiro, 27-Apr-2016) (Revised by Mario Carneiro, 3-May-2016)

	Ref	Expression
Hypotheses	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	pgpfaclem2	⊢ ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		pgpfac.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		pgpfac.c	⊢ 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
3		pgpfac.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
4		pgpfac.p	⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
5		pgpfac.f	⊢ ( 𝜑 → 𝐵 ∈ Fin )
6		pgpfac.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
7		pgpfac.a	⊢ ( 𝜑 → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑈 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) )
8		pgpfac.h	⊢ 𝐻 = ( 𝐺 ↾s 𝑈 )
9		pgpfac.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐻 ) )
10		pgpfac.o	⊢ 𝑂 = ( od ‘ 𝐻 )
11		pgpfac.e	⊢ 𝐸 = ( gEx ‘ 𝐻 )
12		pgpfac.0	⊢ 0 = ( 0g ‘ 𝐻 )
13		pgpfac.l	⊢ ⊕ = ( LSSum ‘ 𝐻 )
14		pgpfac.1	⊢ ( 𝜑 → 𝐸 ≠ 1 )
15		pgpfac.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
16		pgpfac.oe	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = 𝐸 )
17		pgpfac.w	⊢ ( 𝜑 → 𝑊 ∈ ( SubGrp ‘ 𝐻 ) )
18		pgpfac.i	⊢ ( 𝜑 → ( ( 𝐾 ‘ { 𝑋 } ) ∩ 𝑊 ) = { 0 } )
19		pgpfac.s	⊢ ( 𝜑 → ( ( 𝐾 ‘ { 𝑋 } ) ⊕ 𝑊 ) = 𝑈 )
20	8	subsubg	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑊 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ⊆ 𝑈 ) ) )
21	6 20	syl	⊢ ( 𝜑 → ( 𝑊 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ⊆ 𝑈 ) ) )
22	17 21	mpbid	⊢ ( 𝜑 → ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ⊆ 𝑈 ) )
23	22	simprd	⊢ ( 𝜑 → 𝑊 ⊆ 𝑈 )
24	1	subgss	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ 𝐵 )
25	6 24	syl	⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 )
26	5 25	ssfid	⊢ ( 𝜑 → 𝑈 ∈ Fin )
27	26 23	ssfid	⊢ ( 𝜑 → 𝑊 ∈ Fin )
28		hashcl	⊢ ( 𝑊 ∈ Fin → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
29	27 28	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
30	29	nn0red	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
31	12	fvexi	⊢ 0 ∈ V
32		hashsng	⊢ ( 0 ∈ V → ( ♯ ‘ { 0 } ) = 1 )
33	31 32	ax-mp	⊢ ( ♯ ‘ { 0 } ) = 1
34		subgrcl	⊢ ( 𝑊 ∈ ( SubGrp ‘ 𝐻 ) → 𝐻 ∈ Grp )
35		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
36	35	subgacs	⊢ ( 𝐻 ∈ Grp → ( SubGrp ‘ 𝐻 ) ∈ ( ACS ‘ ( Base ‘ 𝐻 ) ) )
37		acsmre	⊢ ( ( SubGrp ‘ 𝐻 ) ∈ ( ACS ‘ ( Base ‘ 𝐻 ) ) → ( SubGrp ‘ 𝐻 ) ∈ ( Moore ‘ ( Base ‘ 𝐻 ) ) )
38	17 34 36 37	4syl	⊢ ( 𝜑 → ( SubGrp ‘ 𝐻 ) ∈ ( Moore ‘ ( Base ‘ 𝐻 ) ) )
39	38 9	mrcssvd	⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ⊆ ( Base ‘ 𝐻 ) )
40	8	subgbas	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 = ( Base ‘ 𝐻 ) )
41	6 40	syl	⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐻 ) )
42	39 41	sseqtrrd	⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ⊆ 𝑈 )
43	26 42	ssfid	⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ∈ Fin )
44	15 41	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐻 ) )
45	9	mrcsncl	⊢ ( ( ( SubGrp ‘ 𝐻 ) ∈ ( Moore ‘ ( Base ‘ 𝐻 ) ) ∧ 𝑋 ∈ ( Base ‘ 𝐻 ) ) → ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐻 ) )
46	38 44 45	syl2anc	⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐻 ) )
47	12	subg0cl	⊢ ( ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐻 ) → 0 ∈ ( 𝐾 ‘ { 𝑋 } ) )
48	46 47	syl	⊢ ( 𝜑 → 0 ∈ ( 𝐾 ‘ { 𝑋 } ) )
49	48	snssd	⊢ ( 𝜑 → { 0 } ⊆ ( 𝐾 ‘ { 𝑋 } ) )
50	44	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ ( Base ‘ 𝐻 ) )
51	38 9 50	mrcssidd	⊢ ( 𝜑 → { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) )
52		snssg	⊢ ( 𝑋 ∈ 𝑈 → ( 𝑋 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) ) )
53	15 52	syl	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) ) )
54	51 53	mpbird	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐾 ‘ { 𝑋 } ) )
55	16 14	eqnetrd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) ≠ 1 )
56	10 12	od1	⊢ ( 𝐻 ∈ Grp → ( 𝑂 ‘ 0 ) = 1 )
57	17 34 56	3syl	⊢ ( 𝜑 → ( 𝑂 ‘ 0 ) = 1 )
58		elsni	⊢ ( 𝑋 ∈ { 0 } → 𝑋 = 0 )
59	58	fveqeq2d	⊢ ( 𝑋 ∈ { 0 } → ( ( 𝑂 ‘ 𝑋 ) = 1 ↔ ( 𝑂 ‘ 0 ) = 1 ) )
60	57 59	syl5ibrcom	⊢ ( 𝜑 → ( 𝑋 ∈ { 0 } → ( 𝑂 ‘ 𝑋 ) = 1 ) )
61	60	necon3ad	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑋 ) ≠ 1 → ¬ 𝑋 ∈ { 0 } ) )
62	55 61	mpd	⊢ ( 𝜑 → ¬ 𝑋 ∈ { 0 } )
63	49 54 62	ssnelpssd	⊢ ( 𝜑 → { 0 } ⊊ ( 𝐾 ‘ { 𝑋 } ) )
64		php3	⊢ ( ( ( 𝐾 ‘ { 𝑋 } ) ∈ Fin ∧ { 0 } ⊊ ( 𝐾 ‘ { 𝑋 } ) ) → { 0 } ≺ ( 𝐾 ‘ { 𝑋 } ) )
65	43 63 64	syl2anc	⊢ ( 𝜑 → { 0 } ≺ ( 𝐾 ‘ { 𝑋 } ) )
66		snfi	⊢ { 0 } ∈ Fin
67		hashsdom	⊢ ( ( { 0 } ∈ Fin ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ Fin ) → ( ( ♯ ‘ { 0 } ) < ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ↔ { 0 } ≺ ( 𝐾 ‘ { 𝑋 } ) ) )
68	66 43 67	sylancr	⊢ ( 𝜑 → ( ( ♯ ‘ { 0 } ) < ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ↔ { 0 } ≺ ( 𝐾 ‘ { 𝑋 } ) ) )
69	65 68	mpbird	⊢ ( 𝜑 → ( ♯ ‘ { 0 } ) < ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) )
70	33 69	eqbrtrrid	⊢ ( 𝜑 → 1 < ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) )
71		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
72		hashcl	⊢ ( ( 𝐾 ‘ { 𝑋 } ) ∈ Fin → ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ∈ ℕ0 )
73	43 72	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ∈ ℕ0 )
74	73	nn0red	⊢ ( 𝜑 → ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ∈ ℝ )
75	12	subg0cl	⊢ ( 𝑊 ∈ ( SubGrp ‘ 𝐻 ) → 0 ∈ 𝑊 )
76		ne0i	⊢ ( 0 ∈ 𝑊 → 𝑊 ≠ ∅ )
77	17 75 76	3syl	⊢ ( 𝜑 → 𝑊 ≠ ∅ )
78		hashnncl	⊢ ( 𝑊 ∈ Fin → ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ 𝑊 ≠ ∅ ) )
79	27 78	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ 𝑊 ≠ ∅ ) )
80	77 79	mpbird	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ )
81	80	nngt0d	⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝑊 ) )
82		ltmul1	⊢ ( ( 1 ∈ ℝ ∧ ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ∈ ℝ ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℝ ∧ 0 < ( ♯ ‘ 𝑊 ) ) ) → ( 1 < ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ↔ ( 1 · ( ♯ ‘ 𝑊 ) ) < ( ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) · ( ♯ ‘ 𝑊 ) ) ) )
83	71 74 30 81 82	syl112anc	⊢ ( 𝜑 → ( 1 < ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ↔ ( 1 · ( ♯ ‘ 𝑊 ) ) < ( ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) · ( ♯ ‘ 𝑊 ) ) ) )
84	70 83	mpbid	⊢ ( 𝜑 → ( 1 · ( ♯ ‘ 𝑊 ) ) < ( ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) · ( ♯ ‘ 𝑊 ) ) )
85	30	recnd	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
86	85	mullidd	⊢ ( 𝜑 → ( 1 · ( ♯ ‘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )
87		eqid	⊢ ( Cntz ‘ 𝐻 ) = ( Cntz ‘ 𝐻 )
88	8	subgabl	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 ∈ Abel )
89	3 6 88	syl2anc	⊢ ( 𝜑 → 𝐻 ∈ Abel )
90	87 89 46 17	ablcntzd	⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ 𝑊 ) )
91	13 12 87 46 17 18 90 43 27	lsmhash	⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐾 ‘ { 𝑋 } ) ⊕ 𝑊 ) ) = ( ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) · ( ♯ ‘ 𝑊 ) ) )
92	19	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐾 ‘ { 𝑋 } ) ⊕ 𝑊 ) ) = ( ♯ ‘ 𝑈 ) )
93	91 92	eqtr3d	⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) · ( ♯ ‘ 𝑊 ) ) = ( ♯ ‘ 𝑈 ) )
94	84 86 93	3brtr3d	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) < ( ♯ ‘ 𝑈 ) )
95	30 94	ltned	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ≠ ( ♯ ‘ 𝑈 ) )
96		fveq2	⊢ ( 𝑊 = 𝑈 → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) )
97	96	necon3i	⊢ ( ( ♯ ‘ 𝑊 ) ≠ ( ♯ ‘ 𝑈 ) → 𝑊 ≠ 𝑈 )
98	95 97	syl	⊢ ( 𝜑 → 𝑊 ≠ 𝑈 )
99		df-pss	⊢ ( 𝑊 ⊊ 𝑈 ↔ ( 𝑊 ⊆ 𝑈 ∧ 𝑊 ≠ 𝑈 ) )
100	23 98 99	sylanbrc	⊢ ( 𝜑 → 𝑊 ⊊ 𝑈 )
101		psseq1	⊢ ( 𝑡 = 𝑊 → ( 𝑡 ⊊ 𝑈 ↔ 𝑊 ⊊ 𝑈 ) )
102		eqeq2	⊢ ( 𝑡 = 𝑊 → ( ( 𝐺 DProd 𝑠 ) = 𝑡 ↔ ( 𝐺 DProd 𝑠 ) = 𝑊 ) )
103	102	anbi2d	⊢ ( 𝑡 = 𝑊 → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) ) )
104	103	rexbidv	⊢ ( 𝑡 = 𝑊 → ( ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) ) )
105	101 104	imbi12d	⊢ ( 𝑡 = 𝑊 → ( ( 𝑡 ⊊ 𝑈 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ↔ ( 𝑊 ⊊ 𝑈 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) ) ) )
106	22	simpld	⊢ ( 𝜑 → 𝑊 ∈ ( SubGrp ‘ 𝐺 ) )
107	105 7 106	rspcdva	⊢ ( 𝜑 → ( 𝑊 ⊊ 𝑈 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) ) )
108	100 107	mpd	⊢ ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) )
109		breq2	⊢ ( 𝑠 = 𝑎 → ( 𝐺 dom DProd 𝑠 ↔ 𝐺 dom DProd 𝑎 ) )
110		oveq2	⊢ ( 𝑠 = 𝑎 → ( 𝐺 DProd 𝑠 ) = ( 𝐺 DProd 𝑎 ) )
111	110	eqeq1d	⊢ ( 𝑠 = 𝑎 → ( ( 𝐺 DProd 𝑠 ) = 𝑊 ↔ ( 𝐺 DProd 𝑎 ) = 𝑊 ) )
112	109 111	anbi12d	⊢ ( 𝑠 = 𝑎 → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) ↔ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) )
113	112	cbvrexvw	⊢ ( ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) ↔ ∃ 𝑎 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) )
114	108 113	sylib	⊢ ( 𝜑 → ∃ 𝑎 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) )
115	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝐺 ∈ Abel )
116	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝑃 pGrp 𝐺 )
117	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝐵 ∈ Fin )
118	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
119	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑈 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) )
120	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝐸 ≠ 1 )
121	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝑋 ∈ 𝑈 )
122	16	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → ( 𝑂 ‘ 𝑋 ) = 𝐸 )
123	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝑊 ∈ ( SubGrp ‘ 𝐻 ) )
124	18	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → ( ( 𝐾 ‘ { 𝑋 } ) ∩ 𝑊 ) = { 0 } )
125	19	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → ( ( 𝐾 ‘ { 𝑋 } ) ⊕ 𝑊 ) = 𝑈 )
126		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝑎 ∈ Word 𝐶 )
127		simprrl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝐺 dom DProd 𝑎 )
128		simprrr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → ( 𝐺 DProd 𝑎 ) = 𝑊 )
129		eqid	⊢ ( 𝑎 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) = ( 𝑎 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ )
130	1 2 115 116 117 118 119 8 9 10 11 12 13 120 121 122 123 124 125 126 127 128 129	pgpfaclem1	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )
131	114 130	rexlimddv	⊢ ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )