Metamath Proof Explorer

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 syl5eq ⊢ ( 𝜑 → 𝑆 = 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 } ∧ ( 𝑆 ⊕ 𝑡 ) = 𝑈 ) )