Metamath Proof Explorer

Theorem grpods

Description: Relate sums of elements of orders and roots of unity. (Contributed by metakunt, 14-Jul-2025)

Ref Expression
Hypotheses grpods.1 
|- B = ( Base ` G )
grpods.2 
|- .^ = ( .g ` G )
grpods.3 
|- ( ph -> G e. Grp )
grpods.4 
|- ( ph -> B e. Fin )
grpods.5 
|- ( ph -> N e. NN )
Assertion grpods 
|- ( ph -> sum_ k e. { m e. ( 1 ... N ) | m || N } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( # ` { x e. B | ( N .^ x ) = ( 0g ` G ) } ) )

Proof

Step Hyp Ref Expression
1 grpods.1 
 |-  B = ( Base ` G )
2 grpods.2 
 |-  .^ = ( .g ` G )
3 grpods.3 
 |-  ( ph -> G e. Grp )
4 grpods.4 
 |-  ( ph -> B e. Fin )
5 grpods.5 
 |-  ( ph -> N e. NN )
6 oveq2 
 |-  ( x = y -> ( N .^ x ) = ( N .^ y ) )
7 6 eqeq1d 
 |-  ( x = y -> ( ( N .^ x ) = ( 0g ` G ) <-> ( N .^ y ) = ( 0g ` G ) ) )
8 7 elrab 
 |-  ( y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } <-> ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) )
9 8 biimpi 
 |-  ( y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } -> ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) )
10 9 adantl 
 |-  ( ( ph /\ y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } ) -> ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) )
11 simpl 
 |-  ( ( ph /\ ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) ) -> ph )
12 simprl 
 |-  ( ( ph /\ ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) ) -> y e. B )
13 11 12 jca 
 |-  ( ( ph /\ ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) ) -> ( ph /\ y e. B ) )
14 simprr 
 |-  ( ( ph /\ ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) ) -> ( N .^ y ) = ( 0g ` G ) )
15 11 3 syl 
 |-  ( ( ph /\ ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) ) -> G e. Grp )
16 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
17 15 16 syl 
 |-  ( ( ph /\ ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) ) -> G e. Mnd )
18 11 5 syl 
 |-  ( ( ph /\ ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) ) -> N e. NN )
19 18 nnnn0d 
 |-  ( ( ph /\ ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) ) -> N e. NN0 )
20 eqid 
 |-  ( od ` G ) = ( od ` G )
21 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
22 1 20 2 21 oddvdsnn0 
 |-  ( ( G e. Mnd /\ y e. B /\ N e. NN0 ) -> ( ( ( od ` G ) ` y ) || N <-> ( N .^ y ) = ( 0g ` G ) ) )
23 17 12 19 22 syl3anc 
 |-  ( ( ph /\ ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) ) -> ( ( ( od ` G ) ` y ) || N <-> ( N .^ y ) = ( 0g ` G ) ) )
24 14 23 mpbird 
 |-  ( ( ph /\ ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) ) -> ( ( od ` G ) ` y ) || N )
25 13 24 jca 
 |-  ( ( ph /\ ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) ) -> ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) )
26 breq1 
 |-  ( m = ( ( od ` G ) ` y ) -> ( m || N <-> ( ( od ` G ) ` y ) || N ) )
27 1zzd 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> 1 e. ZZ )
28 5 ad2antrr 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> N e. NN )
29 28 nnzd 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> N e. ZZ )
30 dvdszrcl 
 |-  ( ( ( od ` G ) ` y ) || N -> ( ( ( od ` G ) ` y ) e. ZZ /\ N e. ZZ ) )
31 30 simpld 
 |-  ( ( ( od ` G ) ` y ) || N -> ( ( od ` G ) ` y ) e. ZZ )
32 31 adantl 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> ( ( od ` G ) ` y ) e. ZZ )
33 3 ad2antrr 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> G e. Grp )
34 4 ad2antrr 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> B e. Fin )
35 simplr 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> y e. B )
36 1 20 odcl2 
 |-  ( ( G e. Grp /\ B e. Fin /\ y e. B ) -> ( ( od ` G ) ` y ) e. NN )
37 33 34 35 36 syl3anc 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> ( ( od ` G ) ` y ) e. NN )
38 37 nnge1d 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> 1 <_ ( ( od ` G ) ` y ) )
39 32 28 jca 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> ( ( ( od ` G ) ` y ) e. ZZ /\ N e. NN ) )
40 simpr 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> ( ( od ` G ) ` y ) || N )
41 dvdsle 
 |-  ( ( ( ( od ` G ) ` y ) e. ZZ /\ N e. NN ) -> ( ( ( od ` G ) ` y ) || N -> ( ( od ` G ) ` y ) <_ N ) )
42 41 imp 
 |-  ( ( ( ( ( od ` G ) ` y ) e. ZZ /\ N e. NN ) /\ ( ( od ` G ) ` y ) || N ) -> ( ( od ` G ) ` y ) <_ N )
43 39 40 42 syl2anc 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> ( ( od ` G ) ` y ) <_ N )
44 27 29 32 38 43 elfzd 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> ( ( od ` G ) ` y ) e. ( 1 ... N ) )
45 26 44 40 elrabd 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> ( ( od ` G ) ` y ) e. { m e. ( 1 ... N ) | m || N } )
46 fveqeq2 
 |-  ( x = y -> ( ( ( od ` G ) ` x ) = ( ( od ` G ) ` y ) <-> ( ( od ` G ) ` y ) = ( ( od ` G ) ` y ) ) )
47 eqidd 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> ( ( od ` G ) ` y ) = ( ( od ` G ) ` y ) )
48 46 35 47 elrabd 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> y e. { x e. B | ( ( od ` G ) ` x ) = ( ( od ` G ) ` y ) } )
49 eqeq2 
 |-  ( k = ( ( od ` G ) ` y ) -> ( ( ( od ` G ) ` x ) = k <-> ( ( od ` G ) ` x ) = ( ( od ` G ) ` y ) ) )
50 49 rabbidv 
 |-  ( k = ( ( od ` G ) ` y ) -> { x e. B | ( ( od ` G ) ` x ) = k } = { x e. B | ( ( od ` G ) ` x ) = ( ( od ` G ) ` y ) } )
51 50 eliuni 
 |-  ( ( ( ( od ` G ) ` y ) e. { m e. ( 1 ... N ) | m || N } /\ y e. { x e. B | ( ( od ` G ) ` x ) = ( ( od ` G ) ` y ) } ) -> y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } )
52 45 48 51 syl2anc 
 |-  ( ( ( ph /\ y e. B ) /\ ( ( od ` G ) ` y ) || N ) -> y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } )
53 25 52 syl 
 |-  ( ( ph /\ ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) ) -> y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } )
54 53 ex 
 |-  ( ph -> ( ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) -> y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } ) )
55 54 adantr 
 |-  ( ( ph /\ y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } ) -> ( ( y e. B /\ ( N .^ y ) = ( 0g ` G ) ) -> y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } ) )
56 10 55 mpd 
 |-  ( ( ph /\ y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } ) -> y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } )
57 56 ex 
 |-  ( ph -> ( y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } -> y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } ) )
58 eliun 
 |-  ( y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } <-> E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } )
59 58 biimpi 
 |-  ( y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } -> E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } )
60 59 adantl 
 |-  ( ( ph /\ y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } ) -> E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } )
61 simplll 
 |-  ( ( ( ( ph /\ E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } ) /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> ph )
62 simplr 
 |-  ( ( ( ( ph /\ E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } ) /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> l e. { m e. ( 1 ... N ) | m || N } )
63 61 62 jca 
 |-  ( ( ( ( ph /\ E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } ) /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> ( ph /\ l e. { m e. ( 1 ... N ) | m || N } ) )
64 simpr 
 |-  ( ( ( ( ph /\ E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } ) /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> y e. { x e. B | ( ( od ` G ) ` x ) = l } )
65 63 64 jca 
 |-  ( ( ( ( ph /\ E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } ) /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> ( ( ph /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) )
66 elrabi 
 |-  ( y e. { x e. B | ( ( od ` G ) ` x ) = l } -> y e. B )
67 66 adantl 
 |-  ( ( ( ph /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> y e. B )
68 simpll 
 |-  ( ( ( ph /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> ph )
69 breq1 
 |-  ( m = l -> ( m || N <-> l || N ) )
70 69 elrab 
 |-  ( l e. { m e. ( 1 ... N ) | m || N } <-> ( l e. ( 1 ... N ) /\ l || N ) )
71 70 biimpi 
 |-  ( l e. { m e. ( 1 ... N ) | m || N } -> ( l e. ( 1 ... N ) /\ l || N ) )
72 71 adantl 
 |-  ( ( ph /\ l e. { m e. ( 1 ... N ) | m || N } ) -> ( l e. ( 1 ... N ) /\ l || N ) )
73 72 adantr 
 |-  ( ( ( ph /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> ( l e. ( 1 ... N ) /\ l || N ) )
74 68 73 jca 
 |-  ( ( ( ph /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) )
75 fveqeq2 
 |-  ( x = y -> ( ( ( od ` G ) ` x ) = l <-> ( ( od ` G ) ` y ) = l ) )
76 75 elrab 
 |-  ( y e. { x e. B | ( ( od ` G ) ` x ) = l } <-> ( y e. B /\ ( ( od ` G ) ` y ) = l ) )
77 76 biimpi 
 |-  ( y e. { x e. B | ( ( od ` G ) ` x ) = l } -> ( y e. B /\ ( ( od ` G ) ` y ) = l ) )
78 77 adantl 
 |-  ( ( ( ph /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> ( y e. B /\ ( ( od ` G ) ` y ) = l ) )
79 74 78 jca 
 |-  ( ( ( ph /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> ( ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) )
80 simpll 
 |-  ( ( ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) -> ph )
81 simprr 
 |-  ( ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) -> l || N )
82 elfzelz 
 |-  ( l e. ( 1 ... N ) -> l e. ZZ )
83 82 adantr 
 |-  ( ( l e. ( 1 ... N ) /\ l || N ) -> l e. ZZ )
84 83 adantl 
 |-  ( ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) -> l e. ZZ )
85 5 adantr 
 |-  ( ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) -> N e. NN )
86 85 nnzd 
 |-  ( ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) -> N e. ZZ )
87 divides 
 |-  ( ( l e. ZZ /\ N e. ZZ ) -> ( l || N <-> E. c e. ZZ ( c x. l ) = N ) )
88 84 86 87 syl2anc 
 |-  ( ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) -> ( l || N <-> E. c e. ZZ ( c x. l ) = N ) )
89 81 88 mpbid 
 |-  ( ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) -> E. c e. ZZ ( c x. l ) = N )
90 89 adantr 
 |-  ( ( ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) -> E. c e. ZZ ( c x. l ) = N )
91 80 90 jca 
 |-  ( ( ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) -> ( ph /\ E. c e. ZZ ( c x. l ) = N ) )
92 simpr 
 |-  ( ( ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) -> ( y e. B /\ ( ( od ` G ) ` y ) = l ) )
93 91 92 jca 
 |-  ( ( ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) -> ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) )
94 oveq1 
 |-  ( ( d x. l ) = N -> ( ( d x. l ) .^ y ) = ( N .^ y ) )
95 94 eqcomd 
 |-  ( ( d x. l ) = N -> ( N .^ y ) = ( ( d x. l ) .^ y ) )
96 95 adantl 
 |-  ( ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) /\ ( d x. l ) = N ) -> ( N .^ y ) = ( ( d x. l ) .^ y ) )
97 simplrr 
 |-  ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) -> ( ( od ` G ) ` y ) = l )
98 97 oveq2d 
 |-  ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) -> ( d x. ( ( od ` G ) ` y ) ) = ( d x. l ) )
99 98 eqcomd 
 |-  ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) -> ( d x. l ) = ( d x. ( ( od ` G ) ` y ) ) )
100 99 oveq1d 
 |-  ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) -> ( ( d x. l ) .^ y ) = ( ( d x. ( ( od ` G ) ` y ) ) .^ y ) )
101 simplll 
 |-  ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) -> ph )
102 simplrl 
 |-  ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) -> y e. B )
103 101 102 jca 
 |-  ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) -> ( ph /\ y e. B ) )
104 simpr 
 |-  ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) -> d e. ZZ )
105 103 104 jca 
 |-  ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) -> ( ( ph /\ y e. B ) /\ d e. ZZ ) )
106 3 ad2antrr 
 |-  ( ( ( ph /\ y e. B ) /\ d e. ZZ ) -> G e. Grp )
107 simpr 
 |-  ( ( ( ph /\ y e. B ) /\ d e. ZZ ) -> d e. ZZ )
108 1 20 odcl 
 |-  ( y e. B -> ( ( od ` G ) ` y ) e. NN0 )
109 108 ad2antlr 
 |-  ( ( ( ph /\ y e. B ) /\ d e. ZZ ) -> ( ( od ` G ) ` y ) e. NN0 )
110 109 nn0zd 
 |-  ( ( ( ph /\ y e. B ) /\ d e. ZZ ) -> ( ( od ` G ) ` y ) e. ZZ )
111 simplr 
 |-  ( ( ( ph /\ y e. B ) /\ d e. ZZ ) -> y e. B )
112 107 110 111 3jca 
 |-  ( ( ( ph /\ y e. B ) /\ d e. ZZ ) -> ( d e. ZZ /\ ( ( od ` G ) ` y ) e. ZZ /\ y e. B ) )
113 1 2 mulgass 
 |-  ( ( G e. Grp /\ ( d e. ZZ /\ ( ( od ` G ) ` y ) e. ZZ /\ y e. B ) ) -> ( ( d x. ( ( od ` G ) ` y ) ) .^ y ) = ( d .^ ( ( ( od ` G ) ` y ) .^ y ) ) )
114 106 112 113 syl2anc 
 |-  ( ( ( ph /\ y e. B ) /\ d e. ZZ ) -> ( ( d x. ( ( od ` G ) ` y ) ) .^ y ) = ( d .^ ( ( ( od ` G ) ` y ) .^ y ) ) )
115 1 20 2 21 odid 
 |-  ( y e. B -> ( ( ( od ` G ) ` y ) .^ y ) = ( 0g ` G ) )
116 111 115 syl 
 |-  ( ( ( ph /\ y e. B ) /\ d e. ZZ ) -> ( ( ( od ` G ) ` y ) .^ y ) = ( 0g ` G ) )
117 116 oveq2d 
 |-  ( ( ( ph /\ y e. B ) /\ d e. ZZ ) -> ( d .^ ( ( ( od ` G ) ` y ) .^ y ) ) = ( d .^ ( 0g ` G ) ) )
118 1 2 21 mulgz 
 |-  ( ( G e. Grp /\ d e. ZZ ) -> ( d .^ ( 0g ` G ) ) = ( 0g ` G ) )
119 106 107 118 syl2anc 
 |-  ( ( ( ph /\ y e. B ) /\ d e. ZZ ) -> ( d .^ ( 0g ` G ) ) = ( 0g ` G ) )
120 117 119 eqtrd 
 |-  ( ( ( ph /\ y e. B ) /\ d e. ZZ ) -> ( d .^ ( ( ( od ` G ) ` y ) .^ y ) ) = ( 0g ` G ) )
121 114 120 eqtrd 
 |-  ( ( ( ph /\ y e. B ) /\ d e. ZZ ) -> ( ( d x. ( ( od ` G ) ` y ) ) .^ y ) = ( 0g ` G ) )
122 105 121 syl 
 |-  ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) -> ( ( d x. ( ( od ` G ) ` y ) ) .^ y ) = ( 0g ` G ) )
123 100 122 eqtrd 
 |-  ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) -> ( ( d x. l ) .^ y ) = ( 0g ` G ) )
124 123 adantr 
 |-  ( ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) /\ ( d x. l ) = N ) -> ( ( d x. l ) .^ y ) = ( 0g ` G ) )
125 96 124 eqtrd 
 |-  ( ( ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) /\ d e. ZZ ) /\ ( d x. l ) = N ) -> ( N .^ y ) = ( 0g ` G ) )
126 nfv 
 |-  F/ d ( c x. l ) = N
127 nfv 
 |-  F/ c ( d x. l ) = N
128 oveq1 
 |-  ( c = d -> ( c x. l ) = ( d x. l ) )
129 128 eqeq1d 
 |-  ( c = d -> ( ( c x. l ) = N <-> ( d x. l ) = N ) )
130 126 127 129 cbvrexw 
 |-  ( E. c e. ZZ ( c x. l ) = N <-> E. d e. ZZ ( d x. l ) = N )
131 130 biimpi 
 |-  ( E. c e. ZZ ( c x. l ) = N -> E. d e. ZZ ( d x. l ) = N )
132 131 adantl 
 |-  ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) -> E. d e. ZZ ( d x. l ) = N )
133 132 adantr 
 |-  ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) -> E. d e. ZZ ( d x. l ) = N )
134 125 133 r19.29a 
 |-  ( ( ( ph /\ E. c e. ZZ ( c x. l ) = N ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) -> ( N .^ y ) = ( 0g ` G ) )
135 93 134 syl 
 |-  ( ( ( ph /\ ( l e. ( 1 ... N ) /\ l || N ) ) /\ ( y e. B /\ ( ( od ` G ) ` y ) = l ) ) -> ( N .^ y ) = ( 0g ` G ) )
136 79 135 syl 
 |-  ( ( ( ph /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> ( N .^ y ) = ( 0g ` G ) )
137 7 67 136 elrabd 
 |-  ( ( ( ph /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } )
138 65 137 syl 
 |-  ( ( ( ( ph /\ E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } ) /\ l e. { m e. ( 1 ... N ) | m || N } ) /\ y e. { x e. B | ( ( od ` G ) ` x ) = l } ) -> y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } )
139 nfv 
 |-  F/ l y e. { x e. B | ( ( od ` G ) ` x ) = k }
140 nfv 
 |-  F/ k y e. { x e. B | ( ( od ` G ) ` x ) = l }
141 eqeq2 
 |-  ( k = l -> ( ( ( od ` G ) ` x ) = k <-> ( ( od ` G ) ` x ) = l ) )
142 141 rabbidv 
 |-  ( k = l -> { x e. B | ( ( od ` G ) ` x ) = k } = { x e. B | ( ( od ` G ) ` x ) = l } )
143 142 eleq2d 
 |-  ( k = l -> ( y e. { x e. B | ( ( od ` G ) ` x ) = k } <-> y e. { x e. B | ( ( od ` G ) ` x ) = l } ) )
144 139 140 143 cbvrexw 
 |-  ( E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } <-> E. l e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = l } )
145 144 biimpi 
 |-  ( E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } -> E. l e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = l } )
146 145 adantl 
 |-  ( ( ph /\ E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } ) -> E. l e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = l } )
147 138 146 r19.29a 
 |-  ( ( ph /\ E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } ) -> y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } )
148 147 ex 
 |-  ( ph -> ( E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } -> y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } ) )
149 148 adantr 
 |-  ( ( ph /\ y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } ) -> ( E. k e. { m e. ( 1 ... N ) | m || N } y e. { x e. B | ( ( od ` G ) ` x ) = k } -> y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } ) )
150 60 149 mpd 
 |-  ( ( ph /\ y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } ) -> y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } )
151 150 ex 
 |-  ( ph -> ( y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } -> y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } ) )
152 57 151 impbid 
 |-  ( ph -> ( y e. { x e. B | ( N .^ x ) = ( 0g ` G ) } <-> y e. U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } ) )
153 152 eqrdv 
 |-  ( ph -> { x e. B | ( N .^ x ) = ( 0g ` G ) } = U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } )
154 153 fveq2d 
 |-  ( ph -> ( # ` { x e. B | ( N .^ x ) = ( 0g ` G ) } ) = ( # ` U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } ) )
155 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
156 ssrab2 
 |-  { m e. ( 1 ... N ) | m || N } C_ ( 1 ... N )
157 156 a1i 
 |-  ( ph -> { m e. ( 1 ... N ) | m || N } C_ ( 1 ... N ) )
158 155 157 ssfid 
 |-  ( ph -> { m e. ( 1 ... N ) | m || N } e. Fin )
159 4 adantr 
 |-  ( ( ph /\ k e. { m e. ( 1 ... N ) | m || N } ) -> B e. Fin )
160 ssrab2 
 |-  { x e. B | ( ( od ` G ) ` x ) = k } C_ B
161 160 a1i 
 |-  ( ( ph /\ k e. { m e. ( 1 ... N ) | m || N } ) -> { x e. B | ( ( od ` G ) ` x ) = k } C_ B )
162 159 161 ssfid 
 |-  ( ( ph /\ k e. { m e. ( 1 ... N ) | m || N } ) -> { x e. B | ( ( od ` G ) ` x ) = k } e. Fin )
163 animorrl 
 |-  ( ( ( ( ph /\ k e. { m e. ( 1 ... N ) | m || N } ) /\ i e. { m e. ( 1 ... N ) | m || N } ) /\ k = i ) -> ( k = i \/ ( { x e. B | ( ( od ` G ) ` x ) = k } i^i { x e. B | ( ( od ` G ) ` x ) = i } ) = (/) ) )
164 inrab 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = k } i^i { x e. B | ( ( od ` G ) ` x ) = i } ) = { x e. B | ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i ) }
165 164 a1i 
 |-  ( -. k = i -> ( { x e. B | ( ( od ` G ) ` x ) = k } i^i { x e. B | ( ( od ` G ) ` x ) = i } ) = { x e. B | ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i ) } )
166 rabn0 
 |-  ( { x e. B | ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i ) } =/= (/) <-> E. x e. B ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i ) )
167 166 biimpi 
 |-  ( { x e. B | ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i ) } =/= (/) -> E. x e. B ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i ) )
168 eqtr2 
 |-  ( ( ( ( od ` G ) ` w ) = k /\ ( ( od ` G ) ` w ) = i ) -> k = i )
169 168 adantl 
 |-  ( ( ( E. x e. B ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i ) /\ w e. B ) /\ ( ( ( od ` G ) ` w ) = k /\ ( ( od ` G ) ` w ) = i ) ) -> k = i )
170 nfv 
 |-  F/ w ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i )
171 nfv 
 |-  F/ x ( ( ( od ` G ) ` w ) = k /\ ( ( od ` G ) ` w ) = i )
172 fveqeq2 
 |-  ( x = w -> ( ( ( od ` G ) ` x ) = k <-> ( ( od ` G ) ` w ) = k ) )
173 fveqeq2 
 |-  ( x = w -> ( ( ( od ` G ) ` x ) = i <-> ( ( od ` G ) ` w ) = i ) )
174 172 173 anbi12d 
 |-  ( x = w -> ( ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i ) <-> ( ( ( od ` G ) ` w ) = k /\ ( ( od ` G ) ` w ) = i ) ) )
175 170 171 174 cbvrexw 
 |-  ( E. x e. B ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i ) <-> E. w e. B ( ( ( od ` G ) ` w ) = k /\ ( ( od ` G ) ` w ) = i ) )
176 175 biimpi 
 |-  ( E. x e. B ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i ) -> E. w e. B ( ( ( od ` G ) ` w ) = k /\ ( ( od ` G ) ` w ) = i ) )
177 169 176 r19.29a 
 |-  ( E. x e. B ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i ) -> k = i )
178 167 177 syl 
 |-  ( { x e. B | ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i ) } =/= (/) -> k = i )
179 178 necon1bi 
 |-  ( -. k = i -> { x e. B | ( ( ( od ` G ) ` x ) = k /\ ( ( od ` G ) ` x ) = i ) } = (/) )
180 165 179 eqtrd 
 |-  ( -. k = i -> ( { x e. B | ( ( od ` G ) ` x ) = k } i^i { x e. B | ( ( od ` G ) ` x ) = i } ) = (/) )
181 180 adantl 
 |-  ( ( ( ( ph /\ k e. { m e. ( 1 ... N ) | m || N } ) /\ i e. { m e. ( 1 ... N ) | m || N } ) /\ -. k = i ) -> ( { x e. B | ( ( od ` G ) ` x ) = k } i^i { x e. B | ( ( od ` G ) ` x ) = i } ) = (/) )
182 181 olcd 
 |-  ( ( ( ( ph /\ k e. { m e. ( 1 ... N ) | m || N } ) /\ i e. { m e. ( 1 ... N ) | m || N } ) /\ -. k = i ) -> ( k = i \/ ( { x e. B | ( ( od ` G ) ` x ) = k } i^i { x e. B | ( ( od ` G ) ` x ) = i } ) = (/) ) )
183 163 182 pm2.61dan 
 |-  ( ( ( ph /\ k e. { m e. ( 1 ... N ) | m || N } ) /\ i e. { m e. ( 1 ... N ) | m || N } ) -> ( k = i \/ ( { x e. B | ( ( od ` G ) ` x ) = k } i^i { x e. B | ( ( od ` G ) ` x ) = i } ) = (/) ) )
184 183 ralrimiva 
 |-  ( ( ph /\ k e. { m e. ( 1 ... N ) | m || N } ) -> A. i e. { m e. ( 1 ... N ) | m || N } ( k = i \/ ( { x e. B | ( ( od ` G ) ` x ) = k } i^i { x e. B | ( ( od ` G ) ` x ) = i } ) = (/) ) )
185 184 ralrimiva 
 |-  ( ph -> A. k e. { m e. ( 1 ... N ) | m || N } A. i e. { m e. ( 1 ... N ) | m || N } ( k = i \/ ( { x e. B | ( ( od ` G ) ` x ) = k } i^i { x e. B | ( ( od ` G ) ` x ) = i } ) = (/) ) )
186 eqeq2 
 |-  ( k = i -> ( ( ( od ` G ) ` x ) = k <-> ( ( od ` G ) ` x ) = i ) )
187 186 rabbidv 
 |-  ( k = i -> { x e. B | ( ( od ` G ) ` x ) = k } = { x e. B | ( ( od ` G ) ` x ) = i } )
188 187 disjor 
 |-  ( Disj_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } <-> A. k e. { m e. ( 1 ... N ) | m || N } A. i e. { m e. ( 1 ... N ) | m || N } ( k = i \/ ( { x e. B | ( ( od ` G ) ` x ) = k } i^i { x e. B | ( ( od ` G ) ` x ) = i } ) = (/) ) )
189 185 188 sylibr 
 |-  ( ph -> Disj_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } )
190 158 162 189 hashiun 
 |-  ( ph -> ( # ` U_ k e. { m e. ( 1 ... N ) | m || N } { x e. B | ( ( od ` G ) ` x ) = k } ) = sum_ k e. { m e. ( 1 ... N ) | m || N } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) )
191 154 190 eqtr2d 
 |-  ( ph -> sum_ k e. { m e. ( 1 ... N ) | m || N } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( # ` { x e. B | ( N .^ x ) = ( 0g ` G ) } ) )