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 bitrid ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ( 𝑆 ⊕ 𝑊 ) ∃ 𝑘 ∈ ℤ 𝐶 = ( 𝑠 ( -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 ⊢ ( 𝜑 → ( 𝑃 · 𝐶 ) ∈ ( 𝑆 ⊕ 𝑊 ) )