Theorem pgpfac1lem4

Description: Lemma for pgpfac1 . (Contributed by Mario Carneiro, 27-Apr-2016)

	Ref	Expression
Hypotheses	pgpfac1.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
	pgpfac1.s	⊢ 𝑆 = ( 𝐾 ‘ { 𝐴 } )
	pgpfac1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	pgpfac1.o	⊢ 𝑂 = ( od ‘ 𝐺 )
	pgpfac1.e	⊢ 𝐸 = ( gEx ‘ 𝐺 )
	pgpfac1.z	⊢ 0 = ( 0g ‘ 𝐺 )
	pgpfac1.l	⊢ ⊕ = ( LSSum ‘ 𝐺 )
	pgpfac1.p	⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
	pgpfac1.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	pgpfac1.n	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	pgpfac1.oe	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) = 𝐸 )
	pgpfac1.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
	pgpfac1.au	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	pgpfac1.w	⊢ ( 𝜑 → 𝑊 ∈ ( SubGrp ‘ 𝐺 ) )
	pgpfac1.i	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑊 ) = { 0 } )
	pgpfac1.ss	⊢ ( 𝜑 → ( 𝑆 ⊕ 𝑊 ) ⊆ 𝑈 )
	pgpfac1.2	⊢ ( 𝜑 → ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ 𝑤 ) )
	pgpfac1.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) )
	pgpfac1.mg	⊢ · = ( .g ‘ 𝐺 )
Assertion	pgpfac1lem4	⊢ ( 𝜑 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		pgpfac1.k	⊢ 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
2		pgpfac1.s	⊢ 𝑆 = ( 𝐾 ‘ { 𝐴 } )
3		pgpfac1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
4		pgpfac1.o	⊢ 𝑂 = ( od ‘ 𝐺 )
5		pgpfac1.e	⊢ 𝐸 = ( gEx ‘ 𝐺 )
6		pgpfac1.z	⊢ 0 = ( 0g ‘ 𝐺 )
7		pgpfac1.l	⊢ ⊕ = ( LSSum ‘ 𝐺 )
8		pgpfac1.p	⊢ ( 𝜑 → 𝑃 pGrp 𝐺 )
9		pgpfac1.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
10		pgpfac1.n	⊢ ( 𝜑 → 𝐵 ∈ Fin )
11		pgpfac1.oe	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐴 ) = 𝐸 )
12		pgpfac1.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
13		pgpfac1.au	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
14		pgpfac1.w	⊢ ( 𝜑 → 𝑊 ∈ ( SubGrp ‘ 𝐺 ) )
15		pgpfac1.i	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑊 ) = { 0 } )
16		pgpfac1.ss	⊢ ( 𝜑 → ( 𝑆 ⊕ 𝑊 ) ⊆ 𝑈 )
17		pgpfac1.2	⊢ ( 𝜑 → ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ 𝑤 ) )
18		pgpfac1.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) )
19		pgpfac1.mg	⊢ · = ( .g ‘ 𝐺 )
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	pgpfac1lem2	⊢ ( 𝜑 → ( 𝑃 · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) )
21		ablgrp	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
22	9 21	syl	⊢ ( 𝜑 → 𝐺 ∈ Grp )
23	3	subgacs	⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
24		acsmre	⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
25	22 23 24	3syl	⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
26	3	subgss	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ 𝐵 )
27	12 26	syl	⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 )
28	27 13	sseldd	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
29	1	mrcsncl	⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
30	25 28 29	syl2anc	⊢ ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
31	2 30	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
32	7	lsmcom	⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 ⊕ 𝑊 ) = ( 𝑊 ⊕ 𝑆 ) )
33	9 31 14 32	syl3anc	⊢ ( 𝜑 → ( 𝑆 ⊕ 𝑊 ) = ( 𝑊 ⊕ 𝑆 ) )
34	20 33	eleqtrd	⊢ ( 𝜑 → ( 𝑃 · 𝐶 ) ∈ ( 𝑊 ⊕ 𝑆 ) )
35		eqid	⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
36	35 7 14 31	lsmelvalm	⊢ ( 𝜑 → ( ( 𝑃 · 𝐶 ) ∈ ( 𝑊 ⊕ 𝑆 ) ↔ ∃ 𝑤 ∈ 𝑊 ∃ 𝑠 ∈ 𝑆 ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) 𝑠 ) ) )
37	34 36	mpbid	⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑊 ∃ 𝑠 ∈ 𝑆 ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) 𝑠 ) )
38		eqid	⊢ ( 𝑘 ∈ ℤ ↦ ( 𝑘 · 𝐴 ) ) = ( 𝑘 ∈ ℤ ↦ ( 𝑘 · 𝐴 ) )
39	3 19 38 1	cycsubg2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐴 } ) = ran ( 𝑘 ∈ ℤ ↦ ( 𝑘 · 𝐴 ) ) )
40	22 28 39	syl2anc	⊢ ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) = ran ( 𝑘 ∈ ℤ ↦ ( 𝑘 · 𝐴 ) ) )
41	2 40	eqtrid	⊢ ( 𝜑 → 𝑆 = ran ( 𝑘 ∈ ℤ ↦ ( 𝑘 · 𝐴 ) ) )
42	41	rexeqdv	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝑆 ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) 𝑠 ) ↔ ∃ 𝑠 ∈ ran ( 𝑘 ∈ ℤ ↦ ( 𝑘 · 𝐴 ) ) ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) 𝑠 ) ) )
43		ovex	⊢ ( 𝑘 · 𝐴 ) ∈ V
44	43	rgenw	⊢ ∀ 𝑘 ∈ ℤ ( 𝑘 · 𝐴 ) ∈ V
45		oveq2	⊢ ( 𝑠 = ( 𝑘 · 𝐴 ) → ( 𝑤 ( -g ‘ 𝐺 ) 𝑠 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) )
46	45	eqeq2d	⊢ ( 𝑠 = ( 𝑘 · 𝐴 ) → ( ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) 𝑠 ) ↔ ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ) )
47	38 46	rexrnmptw	⊢ ( ∀ 𝑘 ∈ ℤ ( 𝑘 · 𝐴 ) ∈ V → ( ∃ 𝑠 ∈ ran ( 𝑘 ∈ ℤ ↦ ( 𝑘 · 𝐴 ) ) ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) 𝑠 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ) )
48	44 47	ax-mp	⊢ ( ∃ 𝑠 ∈ ran ( 𝑘 ∈ ℤ ↦ ( 𝑘 · 𝐴 ) ) ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) 𝑠 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) )
49	42 48	bitrdi	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝑆 ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) 𝑠 ) ↔ ∃ 𝑘 ∈ ℤ ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ) )
50	49	rexbidv	⊢ ( 𝜑 → ( ∃ 𝑤 ∈ 𝑊 ∃ 𝑠 ∈ 𝑆 ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) 𝑠 ) ↔ ∃ 𝑤 ∈ 𝑊 ∃ 𝑘 ∈ ℤ ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ) )
51	37 50	mpbid	⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑊 ∃ 𝑘 ∈ ℤ ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) )
52		rexcom	⊢ ( ∃ 𝑤 ∈ 𝑊 ∃ 𝑘 ∈ ℤ ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ↔ ∃ 𝑘 ∈ ℤ ∃ 𝑤 ∈ 𝑊 ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) )
53	51 52	sylib	⊢ ( 𝜑 → ∃ 𝑘 ∈ ℤ ∃ 𝑤 ∈ 𝑊 ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) )
54	22	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑤 ∈ 𝑊 ) → 𝐺 ∈ Grp )
55	3	subgss	⊢ ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) → 𝑊 ⊆ 𝐵 )
56	14 55	syl	⊢ ( 𝜑 → 𝑊 ⊆ 𝐵 )
57	56	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑊 ⊆ 𝐵 )
58	57	sselda	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑤 ∈ 𝑊 ) → 𝑤 ∈ 𝐵 )
59		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑤 ∈ 𝑊 ) → 𝑘 ∈ ℤ )
60	28	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑤 ∈ 𝑊 ) → 𝐴 ∈ 𝐵 )
61	3 19	mulgcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑘 ∈ ℤ ∧ 𝐴 ∈ 𝐵 ) → ( 𝑘 · 𝐴 ) ∈ 𝐵 )
62	54 59 60 61	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑤 ∈ 𝑊 ) → ( 𝑘 · 𝐴 ) ∈ 𝐵 )
63		pgpprm	⊢ ( 𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ )
64		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
65	8 63 64	3syl	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
66	18	eldifad	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
67	27 66	sseldd	⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
68	3 19	mulgcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑃 ∈ ℤ ∧ 𝐶 ∈ 𝐵 ) → ( 𝑃 · 𝐶 ) ∈ 𝐵 )
69	22 65 67 68	syl3anc	⊢ ( 𝜑 → ( 𝑃 · 𝐶 ) ∈ 𝐵 )
70	69	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑤 ∈ 𝑊 ) → ( 𝑃 · 𝐶 ) ∈ 𝐵 )
71		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
72	3 71 35	grpsubadd	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑘 · 𝐴 ) ∈ 𝐵 ∧ ( 𝑃 · 𝐶 ) ∈ 𝐵 ) ) → ( ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) = ( 𝑃 · 𝐶 ) ↔ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) = 𝑤 ) )
73	54 58 62 70 72	syl13anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑤 ∈ 𝑊 ) → ( ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) = ( 𝑃 · 𝐶 ) ↔ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) = 𝑤 ) )
74		eqcom	⊢ ( ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ↔ ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) = ( 𝑃 · 𝐶 ) )
75		eqcom	⊢ ( 𝑤 = ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ↔ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) = 𝑤 )
76	73 74 75	3bitr4g	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑤 ∈ 𝑊 ) → ( ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ↔ 𝑤 = ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ) )
77	76	rexbidva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ∃ 𝑤 ∈ 𝑊 ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ↔ ∃ 𝑤 ∈ 𝑊 𝑤 = ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ) )
78		risset	⊢ ( ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ↔ ∃ 𝑤 ∈ 𝑊 𝑤 = ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) )
79	77 78	bitr4di	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ∃ 𝑤 ∈ 𝑊 ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ↔ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) )
80	79	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℤ ∃ 𝑤 ∈ 𝑊 ( 𝑃 · 𝐶 ) = ( 𝑤 ( -g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ↔ ∃ 𝑘 ∈ ℤ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) )
81	53 80	mpbid	⊢ ( 𝜑 → ∃ 𝑘 ∈ ℤ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 )
82	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → 𝑃 pGrp 𝐺 )
83	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → 𝐺 ∈ Abel )
84	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → 𝐵 ∈ Fin )
85	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → ( 𝑂 ‘ 𝐴 ) = 𝐸 )
86	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
87	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → 𝐴 ∈ 𝑈 )
88	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → 𝑊 ∈ ( SubGrp ‘ 𝐺 ) )
89	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → ( 𝑆 ∩ 𝑊 ) = { 0 } )
90	16	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → ( 𝑆 ⊕ 𝑊 ) ⊆ 𝑈 )
91	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → ∀ 𝑤 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤 ) → ¬ ( 𝑆 ⊕ 𝑊 ) ⊊ 𝑤 ) )
92	18	adantr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → 𝐶 ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) )
93		simprl	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → 𝑘 ∈ ℤ )
94		simprr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 )
95		eqid	⊢ ( 𝐶 ( +g ‘ 𝐺 ) ( ( 𝑘 / 𝑃 ) · 𝐴 ) ) = ( 𝐶 ( +g ‘ 𝐺 ) ( ( 𝑘 / 𝑃 ) · 𝐴 ) )
96	1 2 3 4 5 6 7 82 83 84 85 86 87 88 89 90 91 92 19 93 94 95	pgpfac1lem3	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℤ ∧ ( ( 𝑃 · 𝐶 ) ( +g ‘ 𝐺 ) ( 𝑘 · 𝐴 ) ) ∈ 𝑊 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) )
97	81 96	rexlimddv	⊢ ( 𝜑 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆 ∩ 𝑡 ) = { 0 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) )