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