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 
|- B = ( Base ` G )
ablfac1.o 
|- O = ( od ` G )
ablfac1.s 
|- S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )
ablfac1.g 
|- ( ph -> G e. Abel )
ablfac1.f 
|- ( ph -> B e. Fin )
ablfac1.1 
|- ( ph -> A C_ Prime )
Assertion ablfac1b 
|- ( ph -> G dom DProd S )

Proof

Step Hyp Ref Expression
1 ablfac1.b 
 |-  B = ( Base ` G )
2 ablfac1.o 
 |-  O = ( od ` G )
3 ablfac1.s 
 |-  S = ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )
4 ablfac1.g 
 |-  ( ph -> G e. Abel )
5 ablfac1.f 
 |-  ( ph -> B e. Fin )
6 ablfac1.1 
 |-  ( ph -> A C_ Prime )
7 eqid 
 |-  ( Cntz ` G ) = ( Cntz ` G )
8 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
9 eqid 
 |-  ( mrCls ` ( SubGrp ` G ) ) = ( mrCls ` ( SubGrp ` G ) )
10 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
11 4 10 syl 
 |-  ( ph -> G e. Grp )
12 prmex 
 |-  Prime e. _V
13 12 ssex 
 |-  ( A C_ Prime -> A e. _V )
14 6 13 syl 
 |-  ( ph -> A e. _V )
15 4 adantr 
 |-  ( ( ph /\ p e. A ) -> G e. Abel )
16 6 sselda 
 |-  ( ( ph /\ p e. A ) -> p e. Prime )
17 prmnn 
 |-  ( p e. Prime -> p e. NN )
18 16 17 syl 
 |-  ( ( ph /\ p e. A ) -> p e. NN )
19 1 grpbn0 
 |-  ( G e. Grp -> B =/= (/) )
20 11 19 syl 
 |-  ( ph -> B =/= (/) )
21 hashnncl 
 |-  ( B e. Fin -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
22 5 21 syl 
 |-  ( ph -> ( ( # ` B ) e. NN <-> B =/= (/) ) )
23 20 22 mpbird 
 |-  ( ph -> ( # ` B ) e. NN )
24 23 adantr 
 |-  ( ( ph /\ p e. A ) -> ( # ` B ) e. NN )
25 16 24 pccld 
 |-  ( ( ph /\ p e. A ) -> ( p pCnt ( # ` B ) ) e. NN0 )
26 18 25 nnexpcld 
 |-  ( ( ph /\ p e. A ) -> ( p ^ ( p pCnt ( # ` B ) ) ) e. NN )
27 26 nnzd 
 |-  ( ( ph /\ p e. A ) -> ( p ^ ( p pCnt ( # ` B ) ) ) e. ZZ )
28 2 1 oddvdssubg 
 |-  ( ( G e. Abel /\ ( p ^ ( p pCnt ( # ` B ) ) ) e. ZZ ) -> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } e. ( SubGrp ` G ) )
29 15 27 28 syl2anc 
 |-  ( ( ph /\ p e. A ) -> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } e. ( SubGrp ` G ) )
30 29 3 fmptd 
 |-  ( ph -> S : A --> ( SubGrp ` G ) )
31 4 adantr 
 |-  ( ( ph /\ ( a e. A /\ b e. A /\ a =/= b ) ) -> G e. Abel )
32 30 adantr 
 |-  ( ( ph /\ ( a e. A /\ b e. A /\ a =/= b ) ) -> S : A --> ( SubGrp ` G ) )
33 simpr1 
 |-  ( ( ph /\ ( a e. A /\ b e. A /\ a =/= b ) ) -> a e. A )
34 32 33 ffvelrnd 
 |-  ( ( ph /\ ( a e. A /\ b e. A /\ a =/= b ) ) -> ( S ` a ) e. ( SubGrp ` G ) )
35 simpr2 
 |-  ( ( ph /\ ( a e. A /\ b e. A /\ a =/= b ) ) -> b e. A )
36 32 35 ffvelrnd 
 |-  ( ( ph /\ ( a e. A /\ b e. A /\ a =/= b ) ) -> ( S ` b ) e. ( SubGrp ` G ) )
37 7 31 34 36 ablcntzd 
 |-  ( ( ph /\ ( a e. A /\ b e. A /\ a =/= b ) ) -> ( S ` a ) C_ ( ( Cntz ` G ) ` ( S ` b ) ) )
38 id 
 |-  ( p = a -> p = a )
39 oveq1 
 |-  ( p = a -> ( p pCnt ( # ` B ) ) = ( a pCnt ( # ` B ) ) )
40 38 39 oveq12d 
 |-  ( p = a -> ( p ^ ( p pCnt ( # ` B ) ) ) = ( a ^ ( a pCnt ( # ` B ) ) ) )
41 40 breq2d 
 |-  ( p = a -> ( ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) <-> ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) ) )
42 41 rabbidv 
 |-  ( p = a -> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } = { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) } )
43 1 fvexi 
 |-  B e. _V
44 43 rabex 
 |-  { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } e. _V
45 42 3 44 fvmpt3i 
 |-  ( a e. A -> ( S ` a ) = { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) } )
46 45 adantl 
 |-  ( ( ph /\ a e. A ) -> ( S ` a ) = { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) } )
47 eqimss 
 |-  ( ( S ` a ) = { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) } -> ( S ` a ) C_ { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) } )
48 46 47 syl 
 |-  ( ( ph /\ a e. A ) -> ( S ` a ) C_ { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) } )
49 4 adantr 
 |-  ( ( ph /\ a e. A ) -> G e. Abel )
50 eqid 
 |-  ( Base ` G ) = ( Base ` G )
51 50 subgacs 
 |-  ( G e. Grp -> ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) )
52 acsmre 
 |-  ( ( SubGrp ` G ) e. ( ACS ` ( Base ` G ) ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
53 49 10 51 52 4syl 
 |-  ( ( ph /\ a e. A ) -> ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) )
54 df-ima 
 |-  ( S " ( A \ { a } ) ) = ran ( S |` ( A \ { a } ) )
55 6 sselda 
 |-  ( ( ph /\ a e. A ) -> a e. Prime )
56 55 ad2antrr 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> a e. Prime )
57 23 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( # ` B ) e. NN )
58 pcdvds 
 |-  ( ( a e. Prime /\ ( # ` B ) e. NN ) -> ( a ^ ( a pCnt ( # ` B ) ) ) || ( # ` B ) )
59 56 57 58 syl2anc 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( a ^ ( a pCnt ( # ` B ) ) ) || ( # ` B ) )
60 6 ad3antrrr 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> A C_ Prime )
61 eldifi 
 |-  ( p e. ( A \ { a } ) -> p e. A )
62 61 ad2antlr 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> p e. A )
63 60 62 sseldd 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> p e. Prime )
64 pcdvds 
 |-  ( ( p e. Prime /\ ( # ` B ) e. NN ) -> ( p ^ ( p pCnt ( # ` B ) ) ) || ( # ` B ) )
65 63 57 64 syl2anc 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( p ^ ( p pCnt ( # ` B ) ) ) || ( # ` B ) )
66 eqid 
 |-  ( a ^ ( a pCnt ( # ` B ) ) ) = ( a ^ ( a pCnt ( # ` B ) ) )
67 eqid 
 |-  ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) = ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) )
68 1 2 3 4 5 6 66 67 ablfac1lem 
 |-  ( ( ph /\ a e. A ) -> ( ( ( a ^ ( a pCnt ( # ` B ) ) ) e. NN /\ ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) e. NN ) /\ ( ( a ^ ( a pCnt ( # ` B ) ) ) gcd ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) = 1 /\ ( # ` B ) = ( ( a ^ ( a pCnt ( # ` B ) ) ) x. ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) ) )
69 68 simp1d 
 |-  ( ( ph /\ a e. A ) -> ( ( a ^ ( a pCnt ( # ` B ) ) ) e. NN /\ ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) e. NN ) )
70 69 simpld 
 |-  ( ( ph /\ a e. A ) -> ( a ^ ( a pCnt ( # ` B ) ) ) e. NN )
71 70 ad2antrr 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( a ^ ( a pCnt ( # ` B ) ) ) e. NN )
72 71 nnzd 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( a ^ ( a pCnt ( # ` B ) ) ) e. ZZ )
73 63 17 syl 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> p e. NN )
74 63 57 pccld 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( p pCnt ( # ` B ) ) e. NN0 )
75 73 74 nnexpcld 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( p ^ ( p pCnt ( # ` B ) ) ) e. NN )
76 75 nnzd 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( p ^ ( p pCnt ( # ` B ) ) ) e. ZZ )
77 57 nnzd 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( # ` B ) e. ZZ )
78 eldifsni 
 |-  ( p e. ( A \ { a } ) -> p =/= a )
79 78 ad2antlr 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> p =/= a )
80 79 necomd 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> a =/= p )
81 prmrp 
 |-  ( ( a e. Prime /\ p e. Prime ) -> ( ( a gcd p ) = 1 <-> a =/= p ) )
82 56 63 81 syl2anc 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( ( a gcd p ) = 1 <-> a =/= p ) )
83 80 82 mpbird 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( a gcd p ) = 1 )
84 prmz 
 |-  ( a e. Prime -> a e. ZZ )
85 56 84 syl 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> a e. ZZ )
86 prmz 
 |-  ( p e. Prime -> p e. ZZ )
87 63 86 syl 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> p e. ZZ )
88 56 57 pccld 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( a pCnt ( # ` B ) ) e. NN0 )
89 rpexp12i 
 |-  ( ( a e. ZZ /\ p e. ZZ /\ ( ( a pCnt ( # ` B ) ) e. NN0 /\ ( p pCnt ( # ` B ) ) e. NN0 ) ) -> ( ( a gcd p ) = 1 -> ( ( a ^ ( a pCnt ( # ` B ) ) ) gcd ( p ^ ( p pCnt ( # ` B ) ) ) ) = 1 ) )
90 85 87 88 74 89 syl112anc 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( ( a gcd p ) = 1 -> ( ( a ^ ( a pCnt ( # ` B ) ) ) gcd ( p ^ ( p pCnt ( # ` B ) ) ) ) = 1 ) )
91 83 90 mpd 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( ( a ^ ( a pCnt ( # ` B ) ) ) gcd ( p ^ ( p pCnt ( # ` B ) ) ) ) = 1 )
92 coprmdvds2 
 |-  ( ( ( ( a ^ ( a pCnt ( # ` B ) ) ) e. ZZ /\ ( p ^ ( p pCnt ( # ` B ) ) ) e. ZZ /\ ( # ` B ) e. ZZ ) /\ ( ( a ^ ( a pCnt ( # ` B ) ) ) gcd ( p ^ ( p pCnt ( # ` B ) ) ) ) = 1 ) -> ( ( ( a ^ ( a pCnt ( # ` B ) ) ) || ( # ` B ) /\ ( p ^ ( p pCnt ( # ` B ) ) ) || ( # ` B ) ) -> ( ( a ^ ( a pCnt ( # ` B ) ) ) x. ( p ^ ( p pCnt ( # ` B ) ) ) ) || ( # ` B ) ) )
93 72 76 77 91 92 syl31anc 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( ( ( a ^ ( a pCnt ( # ` B ) ) ) || ( # ` B ) /\ ( p ^ ( p pCnt ( # ` B ) ) ) || ( # ` B ) ) -> ( ( a ^ ( a pCnt ( # ` B ) ) ) x. ( p ^ ( p pCnt ( # ` B ) ) ) ) || ( # ` B ) ) )
94 59 65 93 mp2and 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( ( a ^ ( a pCnt ( # ` B ) ) ) x. ( p ^ ( p pCnt ( # ` B ) ) ) ) || ( # ` B ) )
95 68 simp3d 
 |-  ( ( ph /\ a e. A ) -> ( # ` B ) = ( ( a ^ ( a pCnt ( # ` B ) ) ) x. ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) )
96 95 ad2antrr 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( # ` B ) = ( ( a ^ ( a pCnt ( # ` B ) ) ) x. ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) )
97 94 96 breqtrd 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( ( a ^ ( a pCnt ( # ` B ) ) ) x. ( p ^ ( p pCnt ( # ` B ) ) ) ) || ( ( a ^ ( a pCnt ( # ` B ) ) ) x. ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) )
98 69 simprd 
 |-  ( ( ph /\ a e. A ) -> ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) e. NN )
99 98 ad2antrr 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) e. NN )
100 99 nnzd 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) e. ZZ )
101 71 nnne0d 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( a ^ ( a pCnt ( # ` B ) ) ) =/= 0 )
102 dvdscmulr 
 |-  ( ( ( p ^ ( p pCnt ( # ` B ) ) ) e. ZZ /\ ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) e. ZZ /\ ( ( a ^ ( a pCnt ( # ` B ) ) ) e. ZZ /\ ( a ^ ( a pCnt ( # ` B ) ) ) =/= 0 ) ) -> ( ( ( a ^ ( a pCnt ( # ` B ) ) ) x. ( p ^ ( p pCnt ( # ` B ) ) ) ) || ( ( a ^ ( a pCnt ( # ` B ) ) ) x. ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) <-> ( p ^ ( p pCnt ( # ` B ) ) ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) )
103 76 100 72 101 102 syl112anc 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( ( ( a ^ ( a pCnt ( # ` B ) ) ) x. ( p ^ ( p pCnt ( # ` B ) ) ) ) || ( ( a ^ ( a pCnt ( # ` B ) ) ) x. ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) <-> ( p ^ ( p pCnt ( # ` B ) ) ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) )
104 97 103 mpbid 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( p ^ ( p pCnt ( # ` B ) ) ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) )
105 1 2 odcl 
 |-  ( x e. B -> ( O ` x ) e. NN0 )
106 105 adantl 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( O ` x ) e. NN0 )
107 106 nn0zd 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( O ` x ) e. ZZ )
108 dvdstr 
 |-  ( ( ( O ` x ) e. ZZ /\ ( p ^ ( p pCnt ( # ` B ) ) ) e. ZZ /\ ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) e. ZZ ) -> ( ( ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) /\ ( p ^ ( p pCnt ( # ` B ) ) ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) -> ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) )
109 107 76 100 108 syl3anc 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( ( ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) /\ ( p ^ ( p pCnt ( # ` B ) ) ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) -> ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) )
110 104 109 mpan2d 
 |-  ( ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) /\ x e. B ) -> ( ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) -> ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) )
111 110 ss2rabdv 
 |-  ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) -> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } C_ { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } )
112 44 elpw 
 |-  ( { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } e. ~P { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } <-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } C_ { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } )
113 111 112 sylibr 
 |-  ( ( ( ph /\ a e. A ) /\ p e. ( A \ { a } ) ) -> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } e. ~P { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } )
114 3 reseq1i 
 |-  ( S |` ( A \ { a } ) ) = ( ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } ) |` ( A \ { a } ) )
115 difss 
 |-  ( A \ { a } ) C_ A
116 resmpt 
 |-  ( ( A \ { a } ) C_ A -> ( ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } ) |` ( A \ { a } ) ) = ( p e. ( A \ { a } ) |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } ) )
117 115 116 ax-mp 
 |-  ( ( p e. A |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } ) |` ( A \ { a } ) ) = ( p e. ( A \ { a } ) |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )
118 114 117 eqtri 
 |-  ( S |` ( A \ { a } ) ) = ( p e. ( A \ { a } ) |-> { x e. B | ( O ` x ) || ( p ^ ( p pCnt ( # ` B ) ) ) } )
119 113 118 fmptd 
 |-  ( ( ph /\ a e. A ) -> ( S |` ( A \ { a } ) ) : ( A \ { a } ) --> ~P { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } )
120 119 frnd 
 |-  ( ( ph /\ a e. A ) -> ran ( S |` ( A \ { a } ) ) C_ ~P { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } )
121 54 120 eqsstrid 
 |-  ( ( ph /\ a e. A ) -> ( S " ( A \ { a } ) ) C_ ~P { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } )
122 sspwuni 
 |-  ( ( S " ( A \ { a } ) ) C_ ~P { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } <-> U. ( S " ( A \ { a } ) ) C_ { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } )
123 121 122 sylib 
 |-  ( ( ph /\ a e. A ) -> U. ( S " ( A \ { a } ) ) C_ { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } )
124 98 nnzd 
 |-  ( ( ph /\ a e. A ) -> ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) e. ZZ )
125 2 1 oddvdssubg 
 |-  ( ( G e. Abel /\ ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) e. ZZ ) -> { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } e. ( SubGrp ` G ) )
126 49 124 125 syl2anc 
 |-  ( ( ph /\ a e. A ) -> { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } e. ( SubGrp ` G ) )
127 9 mrcsscl 
 |-  ( ( ( SubGrp ` G ) e. ( Moore ` ( Base ` G ) ) /\ U. ( S " ( A \ { a } ) ) C_ { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } /\ { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } e. ( SubGrp ` G ) ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( A \ { a } ) ) ) C_ { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } )
128 53 123 126 127 syl3anc 
 |-  ( ( ph /\ a e. A ) -> ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( A \ { a } ) ) ) C_ { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } )
129 ss2in 
 |-  ( ( ( S ` a ) C_ { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) } /\ ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( A \ { a } ) ) ) C_ { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } ) -> ( ( S ` a ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( A \ { a } ) ) ) ) C_ ( { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) } i^i { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } ) )
130 48 128 129 syl2anc 
 |-  ( ( ph /\ a e. A ) -> ( ( S ` a ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( A \ { a } ) ) ) ) C_ ( { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) } i^i { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } ) )
131 eqid 
 |-  { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) } = { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) }
132 eqid 
 |-  { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } = { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) }
133 68 simp2d 
 |-  ( ( ph /\ a e. A ) -> ( ( a ^ ( a pCnt ( # ` B ) ) ) gcd ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) ) = 1 )
134 eqid 
 |-  ( LSSum ` G ) = ( LSSum ` G )
135 1 2 131 132 49 70 98 133 95 8 134 ablfacrp 
 |-  ( ( ph /\ a e. A ) -> ( ( { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) } i^i { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } ) = { ( 0g ` G ) } /\ ( { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) } ( LSSum ` G ) { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } ) = B ) )
136 135 simpld 
 |-  ( ( ph /\ a e. A ) -> ( { x e. B | ( O ` x ) || ( a ^ ( a pCnt ( # ` B ) ) ) } i^i { x e. B | ( O ` x ) || ( ( # ` B ) / ( a ^ ( a pCnt ( # ` B ) ) ) ) } ) = { ( 0g ` G ) } )
137 130 136 sseqtrd 
 |-  ( ( ph /\ a e. A ) -> ( ( S ` a ) i^i ( ( mrCls ` ( SubGrp ` G ) ) ` U. ( S " ( A \ { a } ) ) ) ) C_ { ( 0g ` G ) } )
138 7 8 9 11 14 30 37 137 dmdprdd 
 |-  ( ph -> G dom DProd S )