Metamath Proof Explorer


Theorem pgpfac1lem2

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 pgpfac1lem2 ( 𝜑 → ( 𝑃 · 𝐶 ) ∈ ( 𝑆 𝑊 ) )

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 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 ( 𝜑 → ( 𝑃 · 𝐶 ) ∈ ( 𝑆 𝑊 ) )