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 |
18
|
eldifbd |
⊢ ( 𝜑 → ¬ 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) |
21 |
18
|
eldifad |
⊢ ( 𝜑 → 𝐶 ∈ 𝑈 ) |
22 |
21
|
adantr |
⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) → 𝐶 ∈ 𝑈 ) |
23 |
|
pgpprm |
⊢ ( 𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ ) |
24 |
8 23
|
syl |
⊢ ( 𝜑 → 𝑃 ∈ ℙ ) |
25 |
|
prmz |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ ) |
26 |
24 25
|
syl |
⊢ ( 𝜑 → 𝑃 ∈ ℤ ) |
27 |
19
|
subgmulgcl |
⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑃 ∈ ℤ ∧ 𝐶 ∈ 𝑈 ) → ( 𝑃 · 𝐶 ) ∈ 𝑈 ) |
28 |
12 26 21 27
|
syl3anc |
⊢ ( 𝜑 → ( 𝑃 · 𝐶 ) ∈ 𝑈 ) |
29 |
28
|
adantr |
⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( 𝑃 · 𝐶 ) ∈ 𝑈 ) |
30 |
|
simpr |
⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) → ¬ ( 𝑃 · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) |
31 |
29 30
|
eldifd |
⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( 𝑃 · 𝐶 ) ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) |
32 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
|
pgpfac1lem1 |
⊢ ( ( 𝜑 ∧ ( 𝑃 · 𝐶 ) ∈ ( 𝑈 ∖ ( 𝑆 ⊕ 𝑊 ) ) ) → ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) ) = 𝑈 ) |
33 |
31 32
|
syldan |
⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) ) = 𝑈 ) |
34 |
22 33
|
eleqtrrd |
⊢ ( ( 𝜑 ∧ ¬ ( 𝑃 · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) → 𝐶 ∈ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) ) ) |
35 |
34
|
ex |
⊢ ( 𝜑 → ( ¬ ( 𝑃 · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) → 𝐶 ∈ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) ) ) ) |
36 |
|
eqid |
⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 ) |
37 |
|
ablgrp |
⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp ) |
38 |
9 37
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ Grp ) |
39 |
3
|
subgacs |
⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) ) |
40 |
38 39
|
syl |
⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ 𝐵 ) ) |
41 |
40
|
acsmred |
⊢ ( 𝜑 → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ) |
42 |
3
|
subgss |
⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ 𝐵 ) |
43 |
12 42
|
syl |
⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 ) |
44 |
43 13
|
sseldd |
⊢ ( 𝜑 → 𝐴 ∈ 𝐵 ) |
45 |
1
|
mrcsncl |
⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) ) |
46 |
41 44 45
|
syl2anc |
⊢ ( 𝜑 → ( 𝐾 ‘ { 𝐴 } ) ∈ ( SubGrp ‘ 𝐺 ) ) |
47 |
2 46
|
eqeltrid |
⊢ ( 𝜑 → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) |
48 |
7
|
lsmsubg2 |
⊢ ( ( 𝐺 ∈ Abel ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ) |
49 |
9 47 14 48
|
syl3anc |
⊢ ( 𝜑 → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ) |
50 |
43 28
|
sseldd |
⊢ ( 𝜑 → ( 𝑃 · 𝐶 ) ∈ 𝐵 ) |
51 |
1
|
mrcsncl |
⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ 𝐵 ) ∧ ( 𝑃 · 𝐶 ) ∈ 𝐵 ) → ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) ∈ ( SubGrp ‘ 𝐺 ) ) |
52 |
41 50 51
|
syl2anc |
⊢ ( 𝜑 → ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) ∈ ( SubGrp ‘ 𝐺 ) ) |
53 |
36 7 49 52
|
lsmelvalm |
⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) ) ↔ ∃ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ∃ 𝑡 ∈ ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) 𝑡 ) ) ) |
54 |
|
eqid |
⊢ ( 𝑘 ∈ ℤ ↦ ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) = ( 𝑘 ∈ ℤ ↦ ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) |
55 |
3 19 54 1
|
cycsubg2 |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑃 · 𝐶 ) ∈ 𝐵 ) → ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) = ran ( 𝑘 ∈ ℤ ↦ ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ) |
56 |
38 50 55
|
syl2anc |
⊢ ( 𝜑 → ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) = ran ( 𝑘 ∈ ℤ ↦ ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ) |
57 |
56
|
rexeqdv |
⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) 𝑡 ) ↔ ∃ 𝑡 ∈ ran ( 𝑘 ∈ ℤ ↦ ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) 𝑡 ) ) ) |
58 |
|
ovex |
⊢ ( 𝑘 · ( 𝑃 · 𝐶 ) ) ∈ V |
59 |
58
|
rgenw |
⊢ ∀ 𝑘 ∈ ℤ ( 𝑘 · ( 𝑃 · 𝐶 ) ) ∈ V |
60 |
|
oveq2 |
⊢ ( 𝑡 = ( 𝑘 · ( 𝑃 · 𝐶 ) ) → ( 𝑠 ( -g ‘ 𝐺 ) 𝑡 ) = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ) |
61 |
60
|
eqeq2d |
⊢ ( 𝑡 = ( 𝑘 · ( 𝑃 · 𝐶 ) ) → ( 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) 𝑡 ) ↔ 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ) ) |
62 |
54 61
|
rexrnmptw |
⊢ ( ∀ 𝑘 ∈ ℤ ( 𝑘 · ( 𝑃 · 𝐶 ) ) ∈ V → ( ∃ 𝑡 ∈ ran ( 𝑘 ∈ ℤ ↦ ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) 𝑡 ) ↔ ∃ 𝑘 ∈ ℤ 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ) ) |
63 |
59 62
|
mp1i |
⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ran ( 𝑘 ∈ ℤ ↦ ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) 𝑡 ) ↔ ∃ 𝑘 ∈ ℤ 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ) ) |
64 |
57 63
|
bitrd |
⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) 𝑡 ) ↔ ∃ 𝑘 ∈ ℤ 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ) ) |
65 |
64
|
rexbidv |
⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ∃ 𝑡 ∈ ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) 𝑡 ) ↔ ∃ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ∃ 𝑘 ∈ ℤ 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ) ) |
66 |
|
rexcom |
⊢ ( ∃ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ∃ 𝑘 ∈ ℤ 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ↔ ∃ 𝑘 ∈ ℤ ∃ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ) |
67 |
38
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → 𝐺 ∈ Grp ) |
68 |
16 43
|
sstrd |
⊢ ( 𝜑 → ( 𝑆 ⊕ 𝑊 ) ⊆ 𝐵 ) |
69 |
68
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑆 ⊕ 𝑊 ) ⊆ 𝐵 ) |
70 |
69
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → 𝑠 ∈ 𝐵 ) |
71 |
|
simplr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → 𝑘 ∈ ℤ ) |
72 |
50
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( 𝑃 · 𝐶 ) ∈ 𝐵 ) |
73 |
3 19
|
mulgcl |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝑘 ∈ ℤ ∧ ( 𝑃 · 𝐶 ) ∈ 𝐵 ) → ( 𝑘 · ( 𝑃 · 𝐶 ) ) ∈ 𝐵 ) |
74 |
67 71 72 73
|
syl3anc |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( 𝑘 · ( 𝑃 · 𝐶 ) ) ∈ 𝐵 ) |
75 |
43 21
|
sseldd |
⊢ ( 𝜑 → 𝐶 ∈ 𝐵 ) |
76 |
75
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → 𝐶 ∈ 𝐵 ) |
77 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
78 |
3 77 36
|
grpsubadd |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑠 ∈ 𝐵 ∧ ( 𝑘 · ( 𝑃 · 𝐶 ) ) ∈ 𝐵 ∧ 𝐶 ∈ 𝐵 ) ) → ( ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) = 𝐶 ↔ ( 𝐶 ( +g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) = 𝑠 ) ) |
79 |
67 70 74 76 78
|
syl13anc |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) = 𝐶 ↔ ( 𝐶 ( +g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) = 𝑠 ) ) |
80 |
|
1zzd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → 1 ∈ ℤ ) |
81 |
26
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → 𝑃 ∈ ℤ ) |
82 |
71 81
|
zmulcld |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( 𝑘 · 𝑃 ) ∈ ℤ ) |
83 |
3 19 77
|
mulgdir |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 1 ∈ ℤ ∧ ( 𝑘 · 𝑃 ) ∈ ℤ ∧ 𝐶 ∈ 𝐵 ) ) → ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) = ( ( 1 · 𝐶 ) ( +g ‘ 𝐺 ) ( ( 𝑘 · 𝑃 ) · 𝐶 ) ) ) |
84 |
67 80 82 76 83
|
syl13anc |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) = ( ( 1 · 𝐶 ) ( +g ‘ 𝐺 ) ( ( 𝑘 · 𝑃 ) · 𝐶 ) ) ) |
85 |
3 19
|
mulg1 |
⊢ ( 𝐶 ∈ 𝐵 → ( 1 · 𝐶 ) = 𝐶 ) |
86 |
76 85
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( 1 · 𝐶 ) = 𝐶 ) |
87 |
3 19
|
mulgass |
⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝐶 ∈ 𝐵 ) ) → ( ( 𝑘 · 𝑃 ) · 𝐶 ) = ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) |
88 |
67 71 81 76 87
|
syl13anc |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( ( 𝑘 · 𝑃 ) · 𝐶 ) = ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) |
89 |
86 88
|
oveq12d |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( ( 1 · 𝐶 ) ( +g ‘ 𝐺 ) ( ( 𝑘 · 𝑃 ) · 𝐶 ) ) = ( 𝐶 ( +g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ) |
90 |
84 89
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) = ( 𝐶 ( +g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ) |
91 |
90
|
eqeq1d |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) = 𝑠 ↔ ( 𝐶 ( +g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) = 𝑠 ) ) |
92 |
79 91
|
bitr4d |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) = 𝐶 ↔ ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) = 𝑠 ) ) |
93 |
|
eqcom |
⊢ ( 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ↔ ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) = 𝐶 ) |
94 |
|
eqcom |
⊢ ( 𝑠 = ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ↔ ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) = 𝑠 ) |
95 |
92 93 94
|
3bitr4g |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ↔ 𝑠 = ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) ) |
96 |
95
|
rexbidva |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ∃ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ↔ ∃ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) 𝑠 = ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) ) |
97 |
|
risset |
⊢ ( ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ↔ ∃ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) 𝑠 = ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) |
98 |
96 97
|
bitr4di |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ∃ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ↔ ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) ) |
99 |
98
|
rexbidva |
⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℤ ∃ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ↔ ∃ 𝑘 ∈ ℤ ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) ) |
100 |
66 99
|
syl5bb |
⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ∃ 𝑘 ∈ ℤ 𝐶 = ( 𝑠 ( -g ‘ 𝐺 ) ( 𝑘 · ( 𝑃 · 𝐶 ) ) ) ↔ ∃ 𝑘 ∈ ℤ ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) ) |
101 |
53 65 100
|
3bitrd |
⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝑆 ⊕ 𝑊 ) ⊕ ( 𝐾 ‘ { ( 𝑃 · 𝐶 ) } ) ) ↔ ∃ 𝑘 ∈ ℤ ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) ) |
102 |
35 101
|
sylibd |
⊢ ( 𝜑 → ( ¬ ( 𝑃 · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) → ∃ 𝑘 ∈ ℤ ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) ) |
103 |
38
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝐺 ∈ Grp ) |
104 |
75
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝐶 ∈ 𝐵 ) |
105 |
|
1z |
⊢ 1 ∈ ℤ |
106 |
|
id |
⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℤ ) |
107 |
|
zmulcl |
⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑘 · 𝑃 ) ∈ ℤ ) |
108 |
106 26 107
|
syl2anr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · 𝑃 ) ∈ ℤ ) |
109 |
|
zaddcl |
⊢ ( ( 1 ∈ ℤ ∧ ( 𝑘 · 𝑃 ) ∈ ℤ ) → ( 1 + ( 𝑘 · 𝑃 ) ) ∈ ℤ ) |
110 |
105 108 109
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 1 + ( 𝑘 · 𝑃 ) ) ∈ ℤ ) |
111 |
3 4
|
odcl |
⊢ ( 𝐶 ∈ 𝐵 → ( 𝑂 ‘ 𝐶 ) ∈ ℕ0 ) |
112 |
104 111
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑂 ‘ 𝐶 ) ∈ ℕ0 ) |
113 |
112
|
nn0zd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑂 ‘ 𝐶 ) ∈ ℤ ) |
114 |
|
hashcl |
⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) |
115 |
10 114
|
syl |
⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) |
116 |
115
|
nn0zd |
⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℤ ) |
117 |
116
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ♯ ‘ 𝐵 ) ∈ ℤ ) |
118 |
110 117
|
gcdcomd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( 1 + ( 𝑘 · 𝑃 ) ) gcd ( ♯ ‘ 𝐵 ) ) = ( ( ♯ ‘ 𝐵 ) gcd ( 1 + ( 𝑘 · 𝑃 ) ) ) ) |
119 |
3
|
pgphash |
⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
120 |
8 10 119
|
syl2anc |
⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
121 |
120
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ♯ ‘ 𝐵 ) = ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) ) |
122 |
121
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( ♯ ‘ 𝐵 ) gcd ( 1 + ( 𝑘 · 𝑃 ) ) ) = ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( 1 + ( 𝑘 · 𝑃 ) ) ) ) |
123 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℤ ) |
124 |
26
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑃 ∈ ℤ ) |
125 |
|
1zzd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 1 ∈ ℤ ) |
126 |
|
gcdaddm |
⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑃 gcd 1 ) = ( 𝑃 gcd ( 1 + ( 𝑘 · 𝑃 ) ) ) ) |
127 |
123 124 125 126
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑃 gcd 1 ) = ( 𝑃 gcd ( 1 + ( 𝑘 · 𝑃 ) ) ) ) |
128 |
|
gcd1 |
⊢ ( 𝑃 ∈ ℤ → ( 𝑃 gcd 1 ) = 1 ) |
129 |
124 128
|
syl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑃 gcd 1 ) = 1 ) |
130 |
127 129
|
eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑃 gcd ( 1 + ( 𝑘 · 𝑃 ) ) ) = 1 ) |
131 |
3
|
grpbn0 |
⊢ ( 𝐺 ∈ Grp → 𝐵 ≠ ∅ ) |
132 |
38 131
|
syl |
⊢ ( 𝜑 → 𝐵 ≠ ∅ ) |
133 |
|
hashnncl |
⊢ ( 𝐵 ∈ Fin → ( ( ♯ ‘ 𝐵 ) ∈ ℕ ↔ 𝐵 ≠ ∅ ) ) |
134 |
10 133
|
syl |
⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) ∈ ℕ ↔ 𝐵 ≠ ∅ ) ) |
135 |
132 134
|
mpbird |
⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ ) |
136 |
24 135
|
pccld |
⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ) |
137 |
136
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ) |
138 |
|
rpexp1i |
⊢ ( ( 𝑃 ∈ ℤ ∧ ( 1 + ( 𝑘 · 𝑃 ) ) ∈ ℤ ∧ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ) → ( ( 𝑃 gcd ( 1 + ( 𝑘 · 𝑃 ) ) ) = 1 → ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( 1 + ( 𝑘 · 𝑃 ) ) ) = 1 ) ) |
139 |
124 110 137 138
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑃 gcd ( 1 + ( 𝑘 · 𝑃 ) ) ) = 1 → ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( 1 + ( 𝑘 · 𝑃 ) ) ) = 1 ) ) |
140 |
130 139
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑃 ↑ ( 𝑃 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( 1 + ( 𝑘 · 𝑃 ) ) ) = 1 ) |
141 |
118 122 140
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( 1 + ( 𝑘 · 𝑃 ) ) gcd ( ♯ ‘ 𝐵 ) ) = 1 ) |
142 |
3 4
|
oddvds2 |
⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ Fin ∧ 𝐶 ∈ 𝐵 ) → ( 𝑂 ‘ 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) ) |
143 |
38 10 75 142
|
syl3anc |
⊢ ( 𝜑 → ( 𝑂 ‘ 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) ) |
144 |
143
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑂 ‘ 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) ) |
145 |
|
rpdvds |
⊢ ( ( ( ( 1 + ( 𝑘 · 𝑃 ) ) ∈ ℤ ∧ ( 𝑂 ‘ 𝐶 ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ) ∧ ( ( ( 1 + ( 𝑘 · 𝑃 ) ) gcd ( ♯ ‘ 𝐵 ) ) = 1 ∧ ( 𝑂 ‘ 𝐶 ) ∥ ( ♯ ‘ 𝐵 ) ) ) → ( ( 1 + ( 𝑘 · 𝑃 ) ) gcd ( 𝑂 ‘ 𝐶 ) ) = 1 ) |
146 |
110 113 117 141 144 145
|
syl32anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( 1 + ( 𝑘 · 𝑃 ) ) gcd ( 𝑂 ‘ 𝐶 ) ) = 1 ) |
147 |
3 4 19
|
odbezout |
⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝐶 ∈ 𝐵 ∧ ( 1 + ( 𝑘 · 𝑃 ) ) ∈ ℤ ) ∧ ( ( 1 + ( 𝑘 · 𝑃 ) ) gcd ( 𝑂 ‘ 𝐶 ) ) = 1 ) → ∃ 𝑎 ∈ ℤ ( 𝑎 · ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) = 𝐶 ) |
148 |
103 104 110 146 147
|
syl31anc |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ∃ 𝑎 ∈ ℤ ( 𝑎 · ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) = 𝐶 ) |
149 |
49
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ) |
150 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → 𝑎 ∈ ℤ ) |
151 |
19
|
subgmulgcl |
⊢ ( ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑎 ∈ ℤ ∧ ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) → ( 𝑎 · ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) ) |
152 |
151
|
3expia |
⊢ ( ( ( 𝑆 ⊕ 𝑊 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑎 ∈ ℤ ) → ( ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) → ( 𝑎 · ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) ) ) |
153 |
149 150 152
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → ( ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) → ( 𝑎 · ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) ) ) |
154 |
|
eleq1 |
⊢ ( ( 𝑎 · ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) = 𝐶 → ( ( 𝑎 · ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) ↔ 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) ) |
155 |
154
|
imbi2d |
⊢ ( ( 𝑎 · ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) = 𝐶 → ( ( ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) → ( 𝑎 · ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) ∈ ( 𝑆 ⊕ 𝑊 ) ) ↔ ( ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) → 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) ) ) |
156 |
153 155
|
syl5ibcom |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → ( ( 𝑎 · ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) = 𝐶 → ( ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) → 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) ) ) |
157 |
156
|
rexlimdva |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ∃ 𝑎 ∈ ℤ ( 𝑎 · ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ) = 𝐶 → ( ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) → 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) ) ) |
158 |
148 157
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) → 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) ) |
159 |
158
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℤ ( ( 1 + ( 𝑘 · 𝑃 ) ) · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) → 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) ) |
160 |
102 159
|
syld |
⊢ ( 𝜑 → ( ¬ ( 𝑃 · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) → 𝐶 ∈ ( 𝑆 ⊕ 𝑊 ) ) ) |
161 |
20 160
|
mt3d |
⊢ ( 𝜑 → ( 𝑃 · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) ) |