Metamath Proof Explorer


Theorem pgpfac1lem3

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𝐺 )
pgpfac1.m ( 𝜑𝑀 ∈ ℤ )
pgpfac1.mw ( 𝜑 → ( ( 𝑃 · 𝐶 ) ( +g𝐺 ) ( 𝑀 · 𝐴 ) ) ∈ 𝑊 )
pgpfac1.d 𝐷 = ( 𝐶 ( +g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) )
Assertion pgpfac1lem3 ( 𝜑 → ∃ 𝑡 ∈ ( 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 pgpfac1.m ( 𝜑𝑀 ∈ ℤ )
21 pgpfac1.mw ( 𝜑 → ( ( 𝑃 · 𝐶 ) ( +g𝐺 ) ( 𝑀 · 𝐴 ) ) ∈ 𝑊 )
22 pgpfac1.d 𝐷 = ( 𝐶 ( +g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) )
23 ablgrp ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
24 9 23 syl ( 𝜑𝐺 ∈ Grp )
25 3 subgacs ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) )
26 acsmre ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
27 24 25 26 3syl ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) )
28 3 subgss ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈𝐵 )
29 12 28 syl ( 𝜑𝑈𝐵 )
30 18 eldifad ( 𝜑𝐶𝑈 )
31 29 13 sseldd ( 𝜑𝐴𝐵 )
32 1 mrcsncl ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐴𝐵 ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
33 27 31 32 syl2anc ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) )
34 2 33 eqeltrid ( 𝜑𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
35 7 lsmub1 ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ⊆ ( 𝑆 𝑊 ) )
36 34 14 35 syl2anc ( 𝜑𝑆 ⊆ ( 𝑆 𝑊 ) )
37 36 16 sstrd ( 𝜑𝑆𝑈 )
38 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 pgpfac1lem3a ( 𝜑 → ( 𝑃𝐸𝑃𝑀 ) )
39 38 simprd ( 𝜑𝑃𝑀 )
40 pgpprm ( 𝑃 pGrp 𝐺𝑃 ∈ ℙ )
41 8 40 syl ( 𝜑𝑃 ∈ ℙ )
42 prmz ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
43 41 42 syl ( 𝜑𝑃 ∈ ℤ )
44 prmnn ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
45 41 44 syl ( 𝜑𝑃 ∈ ℕ )
46 45 nnne0d ( 𝜑𝑃 ≠ 0 )
47 dvdsval2 ( ( 𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑀 ∈ ℤ ) → ( 𝑃𝑀 ↔ ( 𝑀 / 𝑃 ) ∈ ℤ ) )
48 43 46 20 47 syl3anc ( 𝜑 → ( 𝑃𝑀 ↔ ( 𝑀 / 𝑃 ) ∈ ℤ ) )
49 39 48 mpbid ( 𝜑 → ( 𝑀 / 𝑃 ) ∈ ℤ )
50 31 snssd ( 𝜑 → { 𝐴 } ⊆ 𝐵 )
51 27 1 50 mrcssidd ( 𝜑 → { 𝐴 } ⊆ ( 𝐾 ‘ { 𝐴 } ) )
52 51 2 sseqtrrdi ( 𝜑 → { 𝐴 } ⊆ 𝑆 )
53 snssg ( 𝐴𝑈 → ( 𝐴𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
54 13 53 syl ( 𝜑 → ( 𝐴𝑆 ↔ { 𝐴 } ⊆ 𝑆 ) )
55 52 54 mpbird ( 𝜑𝐴𝑆 )
56 19 subgmulgcl ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑀 / 𝑃 ) ∈ ℤ ∧ 𝐴𝑆 ) → ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝑆 )
57 34 49 55 56 syl3anc ( 𝜑 → ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝑆 )
58 37 57 sseldd ( 𝜑 → ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝑈 )
59 eqid ( +g𝐺 ) = ( +g𝐺 )
60 59 subgcl ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐶𝑈 ∧ ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝑈 ) → ( 𝐶 ( +g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ 𝑈 )
61 12 30 58 60 syl3anc ( 𝜑 → ( 𝐶 ( +g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ 𝑈 )
62 22 61 eqeltrid ( 𝜑𝐷𝑈 )
63 29 62 sseldd ( 𝜑𝐷𝐵 )
64 1 mrcsncl ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐷𝐵 ) → ( 𝐾 ‘ { 𝐷 } ) ∈ ( SubGrp ‘ 𝐺 ) )
65 27 63 64 syl2anc ( 𝜑 → ( 𝐾 ‘ { 𝐷 } ) ∈ ( SubGrp ‘ 𝐺 ) )
66 7 lsmsubg2 ( ( 𝐺 ∈ Abel ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝐷 } ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ∈ ( SubGrp ‘ 𝐺 ) )
67 9 14 65 66 syl3anc ( 𝜑 → ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ∈ ( SubGrp ‘ 𝐺 ) )
68 eqid ( -g𝐺 ) = ( -g𝐺 )
69 68 7 14 65 lsmelvalm ( 𝜑 → ( 𝑥 ∈ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ↔ ∃ 𝑤𝑊𝑦 ∈ ( 𝐾 ‘ { 𝐷 } ) 𝑥 = ( 𝑤 ( -g𝐺 ) 𝑦 ) ) )
70 eqid ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) )
71 3 19 70 1 cycsubg2 ( ( 𝐺 ∈ Grp ∧ 𝐷𝐵 ) → ( 𝐾 ‘ { 𝐷 } ) = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) ) )
72 24 63 71 syl2anc ( 𝜑 → ( 𝐾 ‘ { 𝐷 } ) = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) ) )
73 72 rexeqdv ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝐾 ‘ { 𝐷 } ) 𝑥 = ( 𝑤 ( -g𝐺 ) 𝑦 ) ↔ ∃ 𝑦 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) ) 𝑥 = ( 𝑤 ( -g𝐺 ) 𝑦 ) ) )
74 ovex ( 𝑛 · 𝐷 ) ∈ V
75 74 rgenw 𝑛 ∈ ℤ ( 𝑛 · 𝐷 ) ∈ V
76 oveq2 ( 𝑦 = ( 𝑛 · 𝐷 ) → ( 𝑤 ( -g𝐺 ) 𝑦 ) = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) )
77 76 eqeq2d ( 𝑦 = ( 𝑛 · 𝐷 ) → ( 𝑥 = ( 𝑤 ( -g𝐺 ) 𝑦 ) ↔ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
78 70 77 rexrnmptw ( ∀ 𝑛 ∈ ℤ ( 𝑛 · 𝐷 ) ∈ V → ( ∃ 𝑦 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) ) 𝑥 = ( 𝑤 ( -g𝐺 ) 𝑦 ) ↔ ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
79 75 78 ax-mp ( ∃ 𝑦 ∈ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝐷 ) ) 𝑥 = ( 𝑤 ( -g𝐺 ) 𝑦 ) ↔ ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) )
80 73 79 bitrdi ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝐾 ‘ { 𝐷 } ) 𝑥 = ( 𝑤 ( -g𝐺 ) 𝑦 ) ↔ ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
81 80 rexbidv ( 𝜑 → ( ∃ 𝑤𝑊𝑦 ∈ ( 𝐾 ‘ { 𝐷 } ) 𝑥 = ( 𝑤 ( -g𝐺 ) 𝑦 ) ↔ ∃ 𝑤𝑊𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
82 69 81 bitrd ( 𝜑 → ( 𝑥 ∈ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ↔ ∃ 𝑤𝑊𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
83 82 adantr ( ( 𝜑𝑥𝑆 ) → ( 𝑥 ∈ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ↔ ∃ 𝑤𝑊𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
84 simpr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) )
85 14 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑊 ∈ ( SubGrp ‘ 𝐺 ) )
86 simplrl ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑤𝑊 )
87 simplrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑛 ∈ ℤ )
88 87 zcnd ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑛 ∈ ℂ )
89 45 nncnd ( 𝜑𝑃 ∈ ℂ )
90 89 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑃 ∈ ℂ )
91 46 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑃 ≠ 0 )
92 88 90 91 divcan1d ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( 𝑛 / 𝑃 ) · 𝑃 ) = 𝑛 )
93 92 oveq1d ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( ( 𝑛 / 𝑃 ) · 𝑃 ) · 𝐷 ) = ( 𝑛 · 𝐷 ) )
94 24 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝐺 ∈ Grp )
95 18 eldifbd ( 𝜑 → ¬ 𝐶 ∈ ( 𝑆 𝑊 ) )
96 7 lsmsubg2 ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
97 9 34 14 96 syl3anc ( 𝜑 → ( 𝑆 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
98 36 57 sseldd ( 𝜑 → ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ ( 𝑆 𝑊 ) )
99 68 subgsubcl ( ( ( 𝑆 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐷 ∈ ( 𝑆 𝑊 ) ∧ ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ ( 𝑆 𝑊 ) ) → ( 𝐷 ( -g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ ( 𝑆 𝑊 ) )
100 99 3expia ( ( ( 𝑆 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐷 ∈ ( 𝑆 𝑊 ) ) → ( ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ ( 𝑆 𝑊 ) → ( 𝐷 ( -g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ ( 𝑆 𝑊 ) ) )
101 100 impancom ( ( ( 𝑆 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ ( 𝑆 𝑊 ) ) → ( 𝐷 ∈ ( 𝑆 𝑊 ) → ( 𝐷 ( -g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ ( 𝑆 𝑊 ) ) )
102 97 98 101 syl2anc ( 𝜑 → ( 𝐷 ∈ ( 𝑆 𝑊 ) → ( 𝐷 ( -g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ ( 𝑆 𝑊 ) ) )
103 22 oveq1i ( 𝐷 ( -g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) = ( ( 𝐶 ( +g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ( -g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) )
104 29 30 sseldd ( 𝜑𝐶𝐵 )
105 3 subgss ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆𝐵 )
106 34 105 syl ( 𝜑𝑆𝐵 )
107 106 57 sseldd ( 𝜑 → ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝐵 )
108 3 59 68 grppncan ( ( 𝐺 ∈ Grp ∧ 𝐶𝐵 ∧ ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝐵 ) → ( ( 𝐶 ( +g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ( -g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) = 𝐶 )
109 24 104 107 108 syl3anc ( 𝜑 → ( ( 𝐶 ( +g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ( -g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) = 𝐶 )
110 103 109 syl5eq ( 𝜑 → ( 𝐷 ( -g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) = 𝐶 )
111 110 eleq1d ( 𝜑 → ( ( 𝐷 ( -g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ∈ ( 𝑆 𝑊 ) ↔ 𝐶 ∈ ( 𝑆 𝑊 ) ) )
112 102 111 sylibd ( 𝜑 → ( 𝐷 ∈ ( 𝑆 𝑊 ) → 𝐶 ∈ ( 𝑆 𝑊 ) ) )
113 95 112 mtod ( 𝜑 → ¬ 𝐷 ∈ ( 𝑆 𝑊 ) )
114 113 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ¬ 𝐷 ∈ ( 𝑆 𝑊 ) )
115 41 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑃 ∈ ℙ )
116 coprm ( ( 𝑃 ∈ ℙ ∧ 𝑛 ∈ ℤ ) → ( ¬ 𝑃𝑛 ↔ ( 𝑃 gcd 𝑛 ) = 1 ) )
117 115 87 116 syl2anc ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ¬ 𝑃𝑛 ↔ ( 𝑃 gcd 𝑛 ) = 1 ) )
118 43 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑃 ∈ ℤ )
119 bezout ( ( 𝑃 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑃 gcd 𝑛 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) )
120 118 87 119 syl2anc ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑃 gcd 𝑛 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) )
121 eqeq1 ( ( 𝑃 gcd 𝑛 ) = 1 → ( ( 𝑃 gcd 𝑛 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) ↔ 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) ) )
122 121 2rexbidv ( ( 𝑃 gcd 𝑛 ) = 1 → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( 𝑃 gcd 𝑛 ) = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) ) )
123 120 122 syl5ibcom ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( 𝑃 gcd 𝑛 ) = 1 → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) ) )
124 94 adantr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐺 ∈ Grp )
125 118 adantr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑃 ∈ ℤ )
126 simprl ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℤ )
127 125 126 zmulcld ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑃 · 𝑎 ) ∈ ℤ )
128 87 adantr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑛 ∈ ℤ )
129 simprr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℤ )
130 128 129 zmulcld ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑛 · 𝑏 ) ∈ ℤ )
131 63 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝐷𝐵 )
132 131 adantr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝐷𝐵 )
133 3 19 59 mulgdir ( ( 𝐺 ∈ Grp ∧ ( ( 𝑃 · 𝑎 ) ∈ ℤ ∧ ( 𝑛 · 𝑏 ) ∈ ℤ ∧ 𝐷𝐵 ) ) → ( ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) · 𝐷 ) = ( ( ( 𝑃 · 𝑎 ) · 𝐷 ) ( +g𝐺 ) ( ( 𝑛 · 𝑏 ) · 𝐷 ) ) )
134 124 127 130 132 133 syl13anc ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) · 𝐷 ) = ( ( ( 𝑃 · 𝑎 ) · 𝐷 ) ( +g𝐺 ) ( ( 𝑛 · 𝑏 ) · 𝐷 ) ) )
135 97 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑆 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
136 135 adantr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑆 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) )
137 90 adantr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑃 ∈ ℂ )
138 zcn ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
139 138 ad2antrl ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℂ )
140 137 139 mulcomd ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑃 · 𝑎 ) = ( 𝑎 · 𝑃 ) )
141 140 oveq1d ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑃 · 𝑎 ) · 𝐷 ) = ( ( 𝑎 · 𝑃 ) · 𝐷 ) )
142 3 19 mulgass ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝐷𝐵 ) ) → ( ( 𝑎 · 𝑃 ) · 𝐷 ) = ( 𝑎 · ( 𝑃 · 𝐷 ) ) )
143 124 126 125 132 142 syl13anc ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑎 · 𝑃 ) · 𝐷 ) = ( 𝑎 · ( 𝑃 · 𝐷 ) ) )
144 141 143 eqtrd ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑃 · 𝑎 ) · 𝐷 ) = ( 𝑎 · ( 𝑃 · 𝐷 ) ) )
145 7 lsmub2 ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑊 ⊆ ( 𝑆 𝑊 ) )
146 34 14 145 syl2anc ( 𝜑𝑊 ⊆ ( 𝑆 𝑊 ) )
147 22 oveq2i ( 𝑃 · 𝐷 ) = ( 𝑃 · ( 𝐶 ( +g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) )
148 3 19 59 mulgdi ( ( 𝐺 ∈ Abel ∧ ( 𝑃 ∈ ℤ ∧ 𝐶𝐵 ∧ ( ( 𝑀 / 𝑃 ) · 𝐴 ) ∈ 𝐵 ) ) → ( 𝑃 · ( 𝐶 ( +g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ) = ( ( 𝑃 · 𝐶 ) ( +g𝐺 ) ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ) )
149 9 43 104 107 148 syl13anc ( 𝜑 → ( 𝑃 · ( 𝐶 ( +g𝐺 ) ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ) = ( ( 𝑃 · 𝐶 ) ( +g𝐺 ) ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ) )
150 147 149 syl5eq ( 𝜑 → ( 𝑃 · 𝐷 ) = ( ( 𝑃 · 𝐶 ) ( +g𝐺 ) ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ) )
151 3 19 mulgass ( ( 𝐺 ∈ Grp ∧ ( 𝑃 ∈ ℤ ∧ ( 𝑀 / 𝑃 ) ∈ ℤ ∧ 𝐴𝐵 ) ) → ( ( 𝑃 · ( 𝑀 / 𝑃 ) ) · 𝐴 ) = ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) )
152 24 43 49 31 151 syl13anc ( 𝜑 → ( ( 𝑃 · ( 𝑀 / 𝑃 ) ) · 𝐴 ) = ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) )
153 20 zcnd ( 𝜑𝑀 ∈ ℂ )
154 153 89 46 divcan2d ( 𝜑 → ( 𝑃 · ( 𝑀 / 𝑃 ) ) = 𝑀 )
155 154 oveq1d ( 𝜑 → ( ( 𝑃 · ( 𝑀 / 𝑃 ) ) · 𝐴 ) = ( 𝑀 · 𝐴 ) )
156 152 155 eqtr3d ( 𝜑 → ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) = ( 𝑀 · 𝐴 ) )
157 156 oveq2d ( 𝜑 → ( ( 𝑃 · 𝐶 ) ( +g𝐺 ) ( 𝑃 · ( ( 𝑀 / 𝑃 ) · 𝐴 ) ) ) = ( ( 𝑃 · 𝐶 ) ( +g𝐺 ) ( 𝑀 · 𝐴 ) ) )
158 150 157 eqtrd ( 𝜑 → ( 𝑃 · 𝐷 ) = ( ( 𝑃 · 𝐶 ) ( +g𝐺 ) ( 𝑀 · 𝐴 ) ) )
159 158 21 eqeltrd ( 𝜑 → ( 𝑃 · 𝐷 ) ∈ 𝑊 )
160 146 159 sseldd ( 𝜑 → ( 𝑃 · 𝐷 ) ∈ ( 𝑆 𝑊 ) )
161 160 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑃 · 𝐷 ) ∈ ( 𝑆 𝑊 ) )
162 161 adantr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑃 · 𝐷 ) ∈ ( 𝑆 𝑊 ) )
163 19 subgmulgcl ( ( ( 𝑆 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑎 ∈ ℤ ∧ ( 𝑃 · 𝐷 ) ∈ ( 𝑆 𝑊 ) ) → ( 𝑎 · ( 𝑃 · 𝐷 ) ) ∈ ( 𝑆 𝑊 ) )
164 136 126 162 163 syl3anc ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 · ( 𝑃 · 𝐷 ) ) ∈ ( 𝑆 𝑊 ) )
165 144 164 eqeltrd ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑃 · 𝑎 ) · 𝐷 ) ∈ ( 𝑆 𝑊 ) )
166 88 adantr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑛 ∈ ℂ )
167 zcn ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
168 167 ad2antll ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℂ )
169 166 168 mulcomd ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑛 · 𝑏 ) = ( 𝑏 · 𝑛 ) )
170 169 oveq1d ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑛 · 𝑏 ) · 𝐷 ) = ( ( 𝑏 · 𝑛 ) · 𝐷 ) )
171 3 19 mulgass ( ( 𝐺 ∈ Grp ∧ ( 𝑏 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝐷𝐵 ) ) → ( ( 𝑏 · 𝑛 ) · 𝐷 ) = ( 𝑏 · ( 𝑛 · 𝐷 ) ) )
172 124 129 128 132 171 syl13anc ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑏 · 𝑛 ) · 𝐷 ) = ( 𝑏 · ( 𝑛 · 𝐷 ) ) )
173 170 172 eqtrd ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑛 · 𝑏 ) · 𝐷 ) = ( 𝑏 · ( 𝑛 · 𝐷 ) ) )
174 84 oveq2d ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑤 ( -g𝐺 ) 𝑥 ) = ( 𝑤 ( -g𝐺 ) ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) )
175 9 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝐺 ∈ Abel )
176 3 subgss ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) → 𝑊𝐵 )
177 85 176 syl ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑊𝐵 )
178 177 86 sseldd ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑤𝐵 )
179 3 19 mulgcl ( ( 𝐺 ∈ Grp ∧ 𝑛 ∈ ℤ ∧ 𝐷𝐵 ) → ( 𝑛 · 𝐷 ) ∈ 𝐵 )
180 94 87 131 179 syl3anc ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑛 · 𝐷 ) ∈ 𝐵 )
181 3 68 175 178 180 ablnncan ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑤 ( -g𝐺 ) ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) = ( 𝑛 · 𝐷 ) )
182 174 181 eqtrd ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑤 ( -g𝐺 ) 𝑥 ) = ( 𝑛 · 𝐷 ) )
183 146 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑊 ⊆ ( 𝑆 𝑊 ) )
184 183 86 sseldd ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑤 ∈ ( 𝑆 𝑊 ) )
185 36 sselda ( ( 𝜑𝑥𝑆 ) → 𝑥 ∈ ( 𝑆 𝑊 ) )
186 185 ad2antrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑥 ∈ ( 𝑆 𝑊 ) )
187 68 subgsubcl ( ( ( 𝑆 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑤 ∈ ( 𝑆 𝑊 ) ∧ 𝑥 ∈ ( 𝑆 𝑊 ) ) → ( 𝑤 ( -g𝐺 ) 𝑥 ) ∈ ( 𝑆 𝑊 ) )
188 135 184 186 187 syl3anc ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑤 ( -g𝐺 ) 𝑥 ) ∈ ( 𝑆 𝑊 ) )
189 182 188 eqeltrrd ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑛 · 𝐷 ) ∈ ( 𝑆 𝑊 ) )
190 189 adantr ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑛 · 𝐷 ) ∈ ( 𝑆 𝑊 ) )
191 19 subgmulgcl ( ( ( 𝑆 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑏 ∈ ℤ ∧ ( 𝑛 · 𝐷 ) ∈ ( 𝑆 𝑊 ) ) → ( 𝑏 · ( 𝑛 · 𝐷 ) ) ∈ ( 𝑆 𝑊 ) )
192 136 129 190 191 syl3anc ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑏 · ( 𝑛 · 𝐷 ) ) ∈ ( 𝑆 𝑊 ) )
193 173 192 eqeltrd ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑛 · 𝑏 ) · 𝐷 ) ∈ ( 𝑆 𝑊 ) )
194 59 subgcl ( ( ( 𝑆 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑃 · 𝑎 ) · 𝐷 ) ∈ ( 𝑆 𝑊 ) ∧ ( ( 𝑛 · 𝑏 ) · 𝐷 ) ∈ ( 𝑆 𝑊 ) ) → ( ( ( 𝑃 · 𝑎 ) · 𝐷 ) ( +g𝐺 ) ( ( 𝑛 · 𝑏 ) · 𝐷 ) ) ∈ ( 𝑆 𝑊 ) )
195 136 165 193 194 syl3anc ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ( 𝑃 · 𝑎 ) · 𝐷 ) ( +g𝐺 ) ( ( 𝑛 · 𝑏 ) · 𝐷 ) ) ∈ ( 𝑆 𝑊 ) )
196 134 195 eqeltrd ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) · 𝐷 ) ∈ ( 𝑆 𝑊 ) )
197 oveq1 ( 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) → ( 1 · 𝐷 ) = ( ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) · 𝐷 ) )
198 197 eleq1d ( 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) → ( ( 1 · 𝐷 ) ∈ ( 𝑆 𝑊 ) ↔ ( ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) · 𝐷 ) ∈ ( 𝑆 𝑊 ) ) )
199 196 198 syl5ibrcom ( ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) → ( 1 · 𝐷 ) ∈ ( 𝑆 𝑊 ) ) )
200 199 rexlimdvva ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 1 = ( ( 𝑃 · 𝑎 ) + ( 𝑛 · 𝑏 ) ) → ( 1 · 𝐷 ) ∈ ( 𝑆 𝑊 ) ) )
201 123 200 syld ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( 𝑃 gcd 𝑛 ) = 1 → ( 1 · 𝐷 ) ∈ ( 𝑆 𝑊 ) ) )
202 3 19 mulg1 ( 𝐷𝐵 → ( 1 · 𝐷 ) = 𝐷 )
203 131 202 syl ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 1 · 𝐷 ) = 𝐷 )
204 203 eleq1d ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( 1 · 𝐷 ) ∈ ( 𝑆 𝑊 ) ↔ 𝐷 ∈ ( 𝑆 𝑊 ) ) )
205 201 204 sylibd ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( 𝑃 gcd 𝑛 ) = 1 → 𝐷 ∈ ( 𝑆 𝑊 ) ) )
206 117 205 sylbid ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ¬ 𝑃𝑛𝐷 ∈ ( 𝑆 𝑊 ) ) )
207 114 206 mt3d ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑃𝑛 )
208 dvdsval2 ( ( 𝑃 ∈ ℤ ∧ 𝑃 ≠ 0 ∧ 𝑛 ∈ ℤ ) → ( 𝑃𝑛 ↔ ( 𝑛 / 𝑃 ) ∈ ℤ ) )
209 118 91 87 208 syl3anc ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑃𝑛 ↔ ( 𝑛 / 𝑃 ) ∈ ℤ ) )
210 207 209 mpbid ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑛 / 𝑃 ) ∈ ℤ )
211 3 19 mulgass ( ( 𝐺 ∈ Grp ∧ ( ( 𝑛 / 𝑃 ) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝐷𝐵 ) ) → ( ( ( 𝑛 / 𝑃 ) · 𝑃 ) · 𝐷 ) = ( ( 𝑛 / 𝑃 ) · ( 𝑃 · 𝐷 ) ) )
212 94 210 118 131 211 syl13anc ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( ( 𝑛 / 𝑃 ) · 𝑃 ) · 𝐷 ) = ( ( 𝑛 / 𝑃 ) · ( 𝑃 · 𝐷 ) ) )
213 93 212 eqtr3d ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑛 · 𝐷 ) = ( ( 𝑛 / 𝑃 ) · ( 𝑃 · 𝐷 ) ) )
214 159 ad3antrrr ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑃 · 𝐷 ) ∈ 𝑊 )
215 19 subgmulgcl ( ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑛 / 𝑃 ) ∈ ℤ ∧ ( 𝑃 · 𝐷 ) ∈ 𝑊 ) → ( ( 𝑛 / 𝑃 ) · ( 𝑃 · 𝐷 ) ) ∈ 𝑊 )
216 85 210 214 215 syl3anc ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( ( 𝑛 / 𝑃 ) · ( 𝑃 · 𝐷 ) ) ∈ 𝑊 )
217 213 216 eqeltrd ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑛 · 𝐷 ) ∈ 𝑊 )
218 68 subgsubcl ( ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑤𝑊 ∧ ( 𝑛 · 𝐷 ) ∈ 𝑊 ) → ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ∈ 𝑊 )
219 85 86 217 218 syl3anc ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ∈ 𝑊 )
220 84 219 eqeltrd ( ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) ) → 𝑥𝑊 )
221 220 ex ( ( ( 𝜑𝑥𝑆 ) ∧ ( 𝑤𝑊𝑛 ∈ ℤ ) ) → ( 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) → 𝑥𝑊 ) )
222 221 rexlimdvva ( ( 𝜑𝑥𝑆 ) → ( ∃ 𝑤𝑊𝑛 ∈ ℤ 𝑥 = ( 𝑤 ( -g𝐺 ) ( 𝑛 · 𝐷 ) ) → 𝑥𝑊 ) )
223 83 222 sylbid ( ( 𝜑𝑥𝑆 ) → ( 𝑥 ∈ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) → 𝑥𝑊 ) )
224 223 imdistanda ( 𝜑 → ( ( 𝑥𝑆𝑥 ∈ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) → ( 𝑥𝑆𝑥𝑊 ) ) )
225 elin ( 𝑥 ∈ ( 𝑆 ∩ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) ↔ ( 𝑥𝑆𝑥 ∈ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) )
226 elin ( 𝑥 ∈ ( 𝑆𝑊 ) ↔ ( 𝑥𝑆𝑥𝑊 ) )
227 224 225 226 3imtr4g ( 𝜑 → ( 𝑥 ∈ ( 𝑆 ∩ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) → 𝑥 ∈ ( 𝑆𝑊 ) ) )
228 227 ssrdv ( 𝜑 → ( 𝑆 ∩ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) ⊆ ( 𝑆𝑊 ) )
229 228 15 sseqtrd ( 𝜑 → ( 𝑆 ∩ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) ⊆ { 0 } )
230 6 subg0cl ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 0𝑆 )
231 34 230 syl ( 𝜑0𝑆 )
232 6 subg0cl ( ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ∈ ( SubGrp ‘ 𝐺 ) → 0 ∈ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) )
233 67 232 syl ( 𝜑0 ∈ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) )
234 231 233 elind ( 𝜑0 ∈ ( 𝑆 ∩ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) )
235 234 snssd ( 𝜑 → { 0 } ⊆ ( 𝑆 ∩ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) )
236 229 235 eqssd ( 𝜑 → ( 𝑆 ∩ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) = { 0 } )
237 7 lsmass ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝐷 } ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑆 𝑊 ) ( 𝐾 ‘ { 𝐷 } ) ) = ( 𝑆 ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) )
238 34 14 65 237 syl3anc ( 𝜑 → ( ( 𝑆 𝑊 ) ( 𝐾 ‘ { 𝐷 } ) ) = ( 𝑆 ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) )
239 62 113 eldifd ( 𝜑𝐷 ∈ ( 𝑈 ∖ ( 𝑆 𝑊 ) ) )
240 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pgpfac1lem1 ( ( 𝜑𝐷 ∈ ( 𝑈 ∖ ( 𝑆 𝑊 ) ) ) → ( ( 𝑆 𝑊 ) ( 𝐾 ‘ { 𝐷 } ) ) = 𝑈 )
241 239 240 mpdan ( 𝜑 → ( ( 𝑆 𝑊 ) ( 𝐾 ‘ { 𝐷 } ) ) = 𝑈 )
242 238 241 eqtr3d ( 𝜑 → ( 𝑆 ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) = 𝑈 )
243 ineq2 ( 𝑡 = ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) → ( 𝑆𝑡 ) = ( 𝑆 ∩ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) )
244 243 eqeq1d ( 𝑡 = ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) → ( ( 𝑆𝑡 ) = { 0 } ↔ ( 𝑆 ∩ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) = { 0 } ) )
245 oveq2 ( 𝑡 = ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) → ( 𝑆 𝑡 ) = ( 𝑆 ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) )
246 245 eqeq1d ( 𝑡 = ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) → ( ( 𝑆 𝑡 ) = 𝑈 ↔ ( 𝑆 ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) = 𝑈 ) )
247 244 246 anbi12d ( 𝑡 = ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) → ( ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) ↔ ( ( 𝑆 ∩ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) = { 0 } ∧ ( 𝑆 ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) = 𝑈 ) ) )
248 247 rspcev ( ( ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ( 𝑆 ∩ ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) = { 0 } ∧ ( 𝑆 ( 𝑊 ( 𝐾 ‘ { 𝐷 } ) ) ) = 𝑈 ) ) → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) )
249 67 236 242 248 syl12anc ( 𝜑 → ∃ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( ( 𝑆𝑡 ) = { 0 } ∧ ( 𝑆 𝑡 ) = 𝑈 ) )