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