Metamath Proof Explorer

Theorem ablfac1b

Description: Any abelian group is the direct product of factors of prime power order (with the exact order further matching the prime factorization of the group order). (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses ablfac1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablfac1.o ⊢ 𝑂 = ( od ‘ 𝐺 )
ablfac1.s ⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
ablfac1.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablfac1.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
ablfac1.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℙ )
Assertion ablfac1b ( 𝜑 → 𝐺 dom DProd 𝑆 )

Proof

Step Hyp Ref Expression
1 ablfac1.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablfac1.o ⊢ 𝑂 = ( od ‘ 𝐺 )
3 ablfac1.s ⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
4 ablfac1.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
5 ablfac1.f ⊢ ( 𝜑 → 𝐵 ∈ Fin )
6 ablfac1.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℙ )
7 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
8 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
9 eqid ⊢ ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) = ( mrCls ‘ ( SubGrp ‘ 𝐺 ) )
10 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
11 4 10 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
12 prmex ⊢ ℙ ∈ V
13 12 ssex ⊢ ( 𝐴 ⊆ ℙ → 𝐴 ∈ V )
14 6 13 syl ⊢ ( 𝜑 → 𝐴 ∈ V )
15 4 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝐺 ∈ Abel )
16 6 sselda ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ ℙ )
17 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ ℕ )
19 1 grpbn0 ⊢ ( 𝐺 ∈ Grp → 𝐵 ≠ ∅ )
20 11 19 syl ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
21 hashnncl ⊢ ( 𝐵 ∈ Fin → ( ( ♯ ‘ 𝐵 ) ∈ ℕ ↔ 𝐵 ≠ ∅ ) )
22 5 21 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) ∈ ℕ ↔ 𝐵 ≠ ∅ ) )
23 20 22 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( ♯ ‘ 𝐵 ) ∈ ℕ )
25 16 24 pccld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 )
26 18 25 nnexpcld ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℕ )
27 26 nnzd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℤ )
28 2 1 oddvdssubg ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℤ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∈ ( SubGrp ‘ 𝐺 ) )
29 15 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐴 ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∈ ( SubGrp ‘ 𝐺 ) )
30 29 3 fmptd ⊢ ( 𝜑 → 𝑆 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) )
31 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏 ) ) → 𝐺 ∈ Abel )
32 30 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏 ) ) → 𝑆 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) )
33 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏 ) ) → 𝑎 ∈ 𝐴 )
34 32 33 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏 ) ) → ( 𝑆 ‘ 𝑎 ) ∈ ( SubGrp ‘ 𝐺 ) )
35 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏 ) ) → 𝑏 ∈ 𝐴 )
36 32 35 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏 ) ) → ( 𝑆 ‘ 𝑏 ) ∈ ( SubGrp ‘ 𝐺 ) )
37 7 31 34 36 ablcntzd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑎 ≠ 𝑏 ) ) → ( 𝑆 ‘ 𝑎 ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝑆 ‘ 𝑏 ) ) )
38 id ⊢ ( 𝑝 = 𝑎 → 𝑝 = 𝑎 )
39 oveq1 ⊢ ( 𝑝 = 𝑎 → ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) = ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) )
40 38 39 oveq12d ⊢ ( 𝑝 = 𝑎 → ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) = ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) )
41 40 breq2d ⊢ ( 𝑝 = 𝑎 → ( ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) )
42 41 rabbidv ⊢ ( 𝑝 = 𝑎 → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
43 1 fvexi ⊢ 𝐵 ∈ V
44 43 rabex ⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∈ V
45 42 3 44 fvmpt3i ⊢ ( 𝑎 ∈ 𝐴 → ( 𝑆 ‘ 𝑎 ) = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
46 45 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑎 ) = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
47 eqimss ⊢ ( ( 𝑆 ‘ 𝑎 ) = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) } → ( 𝑆 ‘ 𝑎 ) ⊆ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
48 46 47 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑎 ) ⊆ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
49 4 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝐺 ∈ Abel )
50 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
51 50 subgacs ⊢ ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) )
52 acsmre ⊢ ( ( SubGrp ‘ 𝐺 ) ∈ ( ACS ‘ ( Base ‘ 𝐺 ) ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
53 49 10 51 52 4syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) )
54 df-ima ⊢ ( 𝑆 “ ( 𝐴 ∖ { 𝑎 } ) ) = ran ( 𝑆 ↾ ( 𝐴 ∖ { 𝑎 } ) )
55 6 sselda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ ℙ )
56 55 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑎 ∈ ℙ )
57 23 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ♯ ‘ 𝐵 ) ∈ ℕ )
58 pcdvds ⊢ ( ( 𝑎 ∈ ℙ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) )
59 56 57 58 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) )
60 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝐴 ⊆ ℙ )
61 eldifi ⊢ ( 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) → 𝑝 ∈ 𝐴 )
62 61 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑝 ∈ 𝐴 )
63 60 62 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑝 ∈ ℙ )
64 pcdvds ⊢ ( ( 𝑝 ∈ ℙ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) )
65 63 57 64 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) )
66 eqid ⊢ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) = ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) )
67 eqid ⊢ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) = ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) )
68 1 2 3 4 5 6 66 67 ablfac1lem ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∈ ℕ ) ∧ ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) = 1 ∧ ( ♯ ‘ 𝐵 ) = ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) ) )
69 68 simp1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℕ ∧ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∈ ℕ ) )
70 69 simpld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℕ )
71 70 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℕ )
72 71 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℤ )
73 63 17 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑝 ∈ ℕ )
74 63 57 pccld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 )
75 73 74 nnexpcld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℕ )
76 75 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℤ )
77 57 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
78 eldifsni ⊢ ( 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) → 𝑝 ≠ 𝑎 )
79 78 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑝 ≠ 𝑎 )
80 79 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑎 ≠ 𝑝 )
81 prmrp ⊢ ( ( 𝑎 ∈ ℙ ∧ 𝑝 ∈ ℙ ) → ( ( 𝑎 gcd 𝑝 ) = 1 ↔ 𝑎 ≠ 𝑝 ) )
82 56 63 81 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑎 gcd 𝑝 ) = 1 ↔ 𝑎 ≠ 𝑝 ) )
83 80 82 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑎 gcd 𝑝 ) = 1 )
84 prmz ⊢ ( 𝑎 ∈ ℙ → 𝑎 ∈ ℤ )
85 56 84 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑎 ∈ ℤ )
86 prmz ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
87 63 86 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑝 ∈ ℤ )
88 56 57 pccld ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 )
89 rpexp12i ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑝 ∈ ℤ ∧ ( ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ∧ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 ) ) → ( ( 𝑎 gcd 𝑝 ) = 1 → ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ) = 1 ) )
90 85 87 88 74 89 syl112anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑎 gcd 𝑝 ) = 1 → ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ) = 1 ) )
91 83 90 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ) = 1 )
92 coprmdvds2 ⊢ ( ( ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℤ ∧ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℤ ) ∧ ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ) = 1 ) → ( ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) ∧ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) → ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) )
93 72 76 77 91 92 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) ∧ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) → ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∥ ( ♯ ‘ 𝐵 ) ) )
94 59 65 93 mp2and ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∥ ( ♯ ‘ 𝐵 ) )
95 68 simp3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ♯ ‘ 𝐵 ) = ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) )
96 95 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ♯ ‘ 𝐵 ) = ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) )
97 94 96 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∥ ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) )
98 69 simprd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∈ ℕ )
99 98 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∈ ℕ )
100 99 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∈ ℤ )
101 71 nnne0d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ≠ 0 )
102 dvdscmulr ⊢ ( ( ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∈ ℤ ∧ ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℤ ∧ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ≠ 0 ) ) → ( ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∥ ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) ↔ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) )
103 76 100 72 101 102 syl112anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∥ ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) · ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) ↔ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) )
104 97 103 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) )
105 1 2 odcl ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 )
106 105 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑂 ‘ 𝑥 ) ∈ ℕ0 )
107 106 nn0zd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑂 ‘ 𝑥 ) ∈ ℤ )
108 dvdstr ⊢ ( ( ( 𝑂 ‘ 𝑥 ) ∈ ℤ ∧ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∈ ℤ ∧ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∈ ℤ ) → ( ( ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∧ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) )
109 107 76 100 108 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∧ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) )
110 104 109 mpan2d ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) → ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) )
111 110 ss2rabdv ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ⊆ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } )
112 44 elpw ⊢ ( { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∈ 𝒫 { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } ↔ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ⊆ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } )
113 111 112 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∈ 𝒫 { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } )
114 3 reseq1i ⊢ ( 𝑆 ↾ ( 𝐴 ∖ { 𝑎 } ) ) = ( ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) ↾ ( 𝐴 ∖ { 𝑎 } ) )
115 difss ⊢ ( 𝐴 ∖ { 𝑎 } ) ⊆ 𝐴
116 resmpt ⊢ ( ( 𝐴 ∖ { 𝑎 } ) ⊆ 𝐴 → ( ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) ↾ ( 𝐴 ∖ { 𝑎 } ) ) = ( 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) )
117 115 116 ax-mp ⊢ ( ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) ↾ ( 𝐴 ∖ { 𝑎 } ) ) = ( 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
118 114 117 eqtri ⊢ ( 𝑆 ↾ ( 𝐴 ∖ { 𝑎 } ) ) = ( 𝑝 ∈ ( 𝐴 ∖ { 𝑎 } ) ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
119 113 118 fmptd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑆 ↾ ( 𝐴 ∖ { 𝑎 } ) ) : ( 𝐴 ∖ { 𝑎 } ) ⟶ 𝒫 { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } )
120 119 frnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ran ( 𝑆 ↾ ( 𝐴 ∖ { 𝑎 } ) ) ⊆ 𝒫 { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } )
121 54 120 eqsstrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑆 “ ( 𝐴 ∖ { 𝑎 } ) ) ⊆ 𝒫 { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } )
122 sspwuni ⊢ ( ( 𝑆 “ ( 𝐴 ∖ { 𝑎 } ) ) ⊆ 𝒫 { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } ↔ ∪ ( 𝑆 “ ( 𝐴 ∖ { 𝑎 } ) ) ⊆ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } )
123 121 122 sylib ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ∪ ( 𝑆 “ ( 𝐴 ∖ { 𝑎 } ) ) ⊆ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } )
124 98 nnzd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∈ ℤ )
125 2 1 oddvdssubg ⊢ ( ( 𝐺 ∈ Abel ∧ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ∈ ℤ ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } ∈ ( SubGrp ‘ 𝐺 ) )
126 49 124 125 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } ∈ ( SubGrp ‘ 𝐺 ) )
127 9 mrcsscl ⊢ ( ( ( SubGrp ‘ 𝐺 ) ∈ ( Moore ‘ ( Base ‘ 𝐺 ) ) ∧ ∪ ( 𝑆 “ ( 𝐴 ∖ { 𝑎 } ) ) ⊆ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } ∧ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐴 ∖ { 𝑎 } ) ) ) ⊆ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } )
128 53 123 126 127 syl3anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐴 ∖ { 𝑎 } ) ) ) ⊆ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } )
129 ss2in ⊢ ( ( ( 𝑆 ‘ 𝑎 ) ⊆ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∧ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐴 ∖ { 𝑎 } ) ) ) ⊆ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } ) → ( ( 𝑆 ‘ 𝑎 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐴 ∖ { 𝑎 } ) ) ) ) ⊆ ( { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∩ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } ) )
130 48 128 129 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑆 ‘ 𝑎 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐴 ∖ { 𝑎 } ) ) ) ) ⊆ ( { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∩ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } ) )
131 eqid ⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) } = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) }
132 eqid ⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } = { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) }
133 68 simp2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) gcd ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) ) = 1 )
134 eqid ⊢ ( LSSum ‘ 𝐺 ) = ( LSSum ‘ 𝐺 )
135 1 2 131 132 49 70 98 133 95 8 134 ablfacrp ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∩ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } ) = { ( 0g ‘ 𝐺 ) } ∧ ( { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) } ( LSSum ‘ 𝐺 ) { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } ) = 𝐵 ) )
136 135 simpld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∩ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( ( ♯ ‘ 𝐵 ) / ( 𝑎 ↑ ( 𝑎 pCnt ( ♯ ‘ 𝐵 ) ) ) ) } ) = { ( 0g ‘ 𝐺 ) } )
137 130 136 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑆 ‘ 𝑎 ) ∩ ( ( mrCls ‘ ( SubGrp ‘ 𝐺 ) ) ‘ ∪ ( 𝑆 “ ( 𝐴 ∖ { 𝑎 } ) ) ) ) ⊆ { ( 0g ‘ 𝐺 ) } )
138 7 8 9 11 14 30 37 137 dmdprdd ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )