Metamath Proof Explorer

Theorem unitscyglem2

Description: Lemma for unitscyg. (Contributed by metakunt, 13-Jul-2025)

Ref Expression
Hypotheses unitscyglem1.1 
|- B = ( Base ` G )
unitscyglem1.2 
|- .^ = ( .g ` G )
unitscyglem1.3 
|- ( ph -> G e. Grp )
unitscyglem1.4 
|- ( ph -> B e. Fin )
unitscyglem1.5 
|- ( ph -> A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n )
unitscyglem2.1 
|- ( ph -> D e. NN )
unitscyglem2.2 
|- ( ph -> D || ( # ` B ) )
unitscyglem2.3 
|- ( ph -> A e. B )
unitscyglem2.4 
|- ( ph -> ( ( od ` G ) ` A ) = D )
unitscyglem2.5 
|- ( ph -> A. c e. NN ( c < D -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) )
Assertion unitscyglem2 
|- ( ph -> ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) = ( phi ` D ) )

Proof

Step Hyp Ref Expression
1 unitscyglem1.1 
 |-  B = ( Base ` G )
2 unitscyglem1.2 
 |-  .^ = ( .g ` G )
3 unitscyglem1.3 
 |-  ( ph -> G e. Grp )
4 unitscyglem1.4 
 |-  ( ph -> B e. Fin )
5 unitscyglem1.5 
 |-  ( ph -> A. n e. NN ( # ` { x e. B | ( n .^ x ) = ( 0g ` G ) } ) <_ n )
6 unitscyglem2.1 
 |-  ( ph -> D e. NN )
7 unitscyglem2.2 
 |-  ( ph -> D || ( # ` B ) )
8 unitscyglem2.3 
 |-  ( ph -> A e. B )
9 unitscyglem2.4 
 |-  ( ph -> ( ( od ` G ) ` A ) = D )
10 unitscyglem2.5 
 |-  ( ph -> A. c e. NN ( c < D -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) )
11 breq1 
 |-  ( a = k -> ( a || D <-> k || D ) )
12 11 elrab 
 |-  ( k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } <-> ( k e. ( 1 ... ( D - 1 ) ) /\ k || D ) )
13 12 biimpi 
 |-  ( k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } -> ( k e. ( 1 ... ( D - 1 ) ) /\ k || D ) )
14 13 adantl 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( k e. ( 1 ... ( D - 1 ) ) /\ k || D ) )
15 14 simpld 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> k e. ( 1 ... ( D - 1 ) ) )
16 15 elfzelzd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> k e. ZZ )
17 6 adantr 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> D e. NN )
18 17 nnzd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> D e. ZZ )
19 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
20 4 19 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
21 20 adantr 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( # ` B ) e. NN0 )
22 21 nn0zd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( # ` B ) e. ZZ )
23 14 simprd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> k || D )
24 7 adantr 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> D || ( # ` B ) )
25 16 18 22 23 24 dvdstrd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> k || ( # ` B ) )
26 simpl 
 |-  ( ( ph /\ ( k e. ( 1 ... ( D - 1 ) ) /\ k || D ) ) -> ph )
27 12 15 sylan2br 
 |-  ( ( ph /\ ( k e. ( 1 ... ( D - 1 ) ) /\ k || D ) ) -> k e. ( 1 ... ( D - 1 ) ) )
28 26 27 jca 
 |-  ( ( ph /\ ( k e. ( 1 ... ( D - 1 ) ) /\ k || D ) ) -> ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) )
29 12 23 sylan2br 
 |-  ( ( ph /\ ( k e. ( 1 ... ( D - 1 ) ) /\ k || D ) ) -> k || D )
30 28 29 jca 
 |-  ( ( ph /\ ( k e. ( 1 ... ( D - 1 ) ) /\ k || D ) ) -> ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) )
31 fveqeq2 
 |-  ( x = ( ( D / k ) .^ A ) -> ( ( ( od ` G ) ` x ) = k <-> ( ( od ` G ) ` ( ( D / k ) .^ A ) ) = k ) )
32 3 ad4antr 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> G e. Grp )
33 simpr 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( l x. k ) = D )
34 33 eqcomd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> D = ( l x. k ) )
35 34 oveq1d 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( D / k ) = ( ( l x. k ) / k ) )
36 simplr 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> l e. NN )
37 36 nncnd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> l e. CC )
38 elfzelz 
 |-  ( k e. ( 1 ... ( D - 1 ) ) -> k e. ZZ )
39 38 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) -> k e. ZZ )
40 39 ad3antrrr 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> k e. ZZ )
41 40 zcnd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> k e. CC )
42 elfzle1 
 |-  ( k e. ( 1 ... ( D - 1 ) ) -> 1 <_ k )
43 42 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) -> 1 <_ k )
44 39 43 jca 
 |-  ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) -> ( k e. ZZ /\ 1 <_ k ) )
45 elnnz1 
 |-  ( k e. NN <-> ( k e. ZZ /\ 1 <_ k ) )
46 44 45 sylibr 
 |-  ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) -> k e. NN )
47 46 adantr 
 |-  ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) -> k e. NN )
48 47 ad2antrr 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> k e. NN )
49 48 nnne0d 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> k =/= 0 )
50 37 41 49 divcan4d 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( l x. k ) / k ) = l )
51 35 50 eqtrd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( D / k ) = l )
52 51 36 eqeltrd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( D / k ) e. NN )
53 52 nnnn0d 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( D / k ) e. NN0 )
54 53 nn0zd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( D / k ) e. ZZ )
55 8 ad4antr 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> A e. B )
56 1 2 32 54 55 mulgcld 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( D / k ) .^ A ) e. B )
57 6 ad2antrr 
 |-  ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) -> D e. NN )
58 57 ad2antrr 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> D e. NN )
59 58 nncnd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> D e. CC )
60 59 41 49 divcan1d 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( D / k ) x. k ) = D )
61 9 ad4antr 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( od ` G ) ` A ) = D )
62 61 eqcomd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> D = ( ( od ` G ) ` A ) )
63 eqid 
 |-  ( od ` G ) = ( od ` G )
64 1 63 2 odmulg 
 |-  ( ( G e. Grp /\ A e. B /\ ( D / k ) e. ZZ ) -> ( ( od ` G ) ` A ) = ( ( ( D / k ) gcd ( ( od ` G ) ` A ) ) x. ( ( od ` G ) ` ( ( D / k ) .^ A ) ) ) )
65 32 55 54 64 syl3anc 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( od ` G ) ` A ) = ( ( ( D / k ) gcd ( ( od ` G ) ` A ) ) x. ( ( od ` G ) ` ( ( D / k ) .^ A ) ) ) )
66 62 65 eqtrd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> D = ( ( ( D / k ) gcd ( ( od ` G ) ` A ) ) x. ( ( od ` G ) ` ( ( D / k ) .^ A ) ) ) )
67 61 oveq2d 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( D / k ) gcd ( ( od ` G ) ` A ) ) = ( ( D / k ) gcd D ) )
68 59 41 49 divcan2d 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( k x. ( D / k ) ) = D )
69 68 eqcomd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> D = ( k x. ( D / k ) ) )
70 69 oveq2d 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( D / k ) gcd D ) = ( ( D / k ) gcd ( k x. ( D / k ) ) ) )
71 53 40 gcdmultipled 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( D / k ) gcd ( k x. ( D / k ) ) ) = ( D / k ) )
72 70 71 eqtrd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( D / k ) gcd D ) = ( D / k ) )
73 67 72 eqtrd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( D / k ) gcd ( ( od ` G ) ` A ) ) = ( D / k ) )
74 73 oveq1d 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( ( D / k ) gcd ( ( od ` G ) ` A ) ) x. ( ( od ` G ) ` ( ( D / k ) .^ A ) ) ) = ( ( D / k ) x. ( ( od ` G ) ` ( ( D / k ) .^ A ) ) ) )
75 66 74 eqtrd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> D = ( ( D / k ) x. ( ( od ` G ) ` ( ( D / k ) .^ A ) ) ) )
76 60 75 eqtr2d 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( D / k ) x. ( ( od ` G ) ` ( ( D / k ) .^ A ) ) ) = ( ( D / k ) x. k ) )
77 1 63 56 odcld 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( od ` G ) ` ( ( D / k ) .^ A ) ) e. NN0 )
78 77 nn0cnd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( od ` G ) ` ( ( D / k ) .^ A ) ) e. CC )
79 54 zcnd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( D / k ) e. CC )
80 58 nnne0d 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> D =/= 0 )
81 59 41 80 49 divne0d 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( D / k ) =/= 0 )
82 78 41 79 81 mulcand 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( ( D / k ) x. ( ( od ` G ) ` ( ( D / k ) .^ A ) ) ) = ( ( D / k ) x. k ) <-> ( ( od ` G ) ` ( ( D / k ) .^ A ) ) = k ) )
83 76 82 mpbid 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( od ` G ) ` ( ( D / k ) .^ A ) ) = k )
84 31 56 83 elrabd 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> ( ( D / k ) .^ A ) e. { x e. B | ( ( od ` G ) ` x ) = k } )
85 84 ne0d 
 |-  ( ( ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) /\ l e. NN ) /\ ( l x. k ) = D ) -> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) )
86 nndivides 
 |-  ( ( k e. NN /\ D e. NN ) -> ( k || D <-> E. l e. NN ( l x. k ) = D ) )
87 47 57 86 syl2anc 
 |-  ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) -> ( k || D <-> E. l e. NN ( l x. k ) = D ) )
88 87 biimpd 
 |-  ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) -> ( k || D -> E. l e. NN ( l x. k ) = D ) )
89 88 syldbl2 
 |-  ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) -> E. l e. NN ( l x. k ) = D )
90 85 89 r19.29a 
 |-  ( ( ( ph /\ k e. ( 1 ... ( D - 1 ) ) ) /\ k || D ) -> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) )
91 30 90 syl 
 |-  ( ( ph /\ ( k e. ( 1 ... ( D - 1 ) ) /\ k || D ) ) -> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) )
92 91 ex 
 |-  ( ph -> ( ( k e. ( 1 ... ( D - 1 ) ) /\ k || D ) -> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) )
93 92 adantr 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( ( k e. ( 1 ... ( D - 1 ) ) /\ k || D ) -> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) )
94 14 93 mpd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) )
95 25 94 jca 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( k || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) )
96 15 42 syl 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> 1 <_ k )
97 16 96 jca 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( k e. ZZ /\ 1 <_ k ) )
98 97 45 sylibr 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> k e. NN )
99 98 nnred 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> k e. RR )
100 17 nnred 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> D e. RR )
101 1red 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> 1 e. RR )
102 100 101 resubcld 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( D - 1 ) e. RR )
103 elfzle2 
 |-  ( k e. ( 1 ... ( D - 1 ) ) -> k <_ ( D - 1 ) )
104 15 103 syl 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> k <_ ( D - 1 ) )
105 100 ltm1d 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( D - 1 ) < D )
106 99 102 100 104 105 lelttrd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> k < D )
107 breq1 
 |-  ( c = k -> ( c < D <-> k < D ) )
108 breq1 
 |-  ( c = k -> ( c || ( # ` B ) <-> k || ( # ` B ) ) )
109 eqeq2 
 |-  ( c = k -> ( ( ( od ` G ) ` x ) = c <-> ( ( od ` G ) ` x ) = k ) )
110 109 rabbidv 
 |-  ( c = k -> { x e. B | ( ( od ` G ) ` x ) = c } = { x e. B | ( ( od ` G ) ` x ) = k } )
111 110 neeq1d 
 |-  ( c = k -> ( { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) <-> { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) )
112 108 111 anbi12d 
 |-  ( c = k -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) <-> ( k || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) ) )
113 110 fveq2d 
 |-  ( c = k -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) )
114 fveq2 
 |-  ( c = k -> ( phi ` c ) = ( phi ` k ) )
115 113 114 eqeq12d 
 |-  ( c = k -> ( ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) <-> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( phi ` k ) ) )
116 112 115 imbi12d 
 |-  ( c = k -> ( ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) <-> ( ( k || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( phi ` k ) ) ) )
117 107 116 imbi12d 
 |-  ( c = k -> ( ( c < D -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) <-> ( k < D -> ( ( k || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( phi ` k ) ) ) ) )
118 10 adantr 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> A. c e. NN ( c < D -> ( ( c || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = c } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = c } ) = ( phi ` c ) ) ) )
119 117 118 98 rspcdva 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( k < D -> ( ( k || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( phi ` k ) ) ) )
120 106 119 mpd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( ( k || ( # ` B ) /\ { x e. B | ( ( od ` G ) ` x ) = k } =/= (/) ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( phi ` k ) ) )
121 95 120 mpd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( phi ` k ) )
122 121 sumeq2dv 
 |-  ( ph -> sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( phi ` k ) )
123 122 eqcomd 
 |-  ( ph -> sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( phi ` k ) = sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) )
124 123 oveq1d 
 |-  ( ph -> ( sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( phi ` k ) + ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) ) = ( sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) + ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) ) )
125 elun 
 |-  ( y e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) <-> ( y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } \/ y e. { D } ) )
126 125 biimpi 
 |-  ( y e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) -> ( y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } \/ y e. { D } ) )
127 126 adantl 
 |-  ( ( ph /\ y e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ) -> ( y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } \/ y e. { D } ) )
128 1zzd 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> 1 e. ZZ )
129 6 adantr 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> D e. NN )
130 129 nnzd 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> D e. ZZ )
131 elfzelz 
 |-  ( a e. ( 1 ... ( D - 1 ) ) -> a e. ZZ )
132 131 adantr 
 |-  ( ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) -> a e. ZZ )
133 132 adantl 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> a e. ZZ )
134 elfzle1 
 |-  ( a e. ( 1 ... ( D - 1 ) ) -> 1 <_ a )
135 134 adantr 
 |-  ( ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) -> 1 <_ a )
136 135 adantl 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> 1 <_ a )
137 133 zred 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> a e. RR )
138 129 nnred 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> D e. RR )
139 1red 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> 1 e. RR )
140 138 139 resubcld 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> ( D - 1 ) e. RR )
141 elfzle2 
 |-  ( a e. ( 1 ... ( D - 1 ) ) -> a <_ ( D - 1 ) )
142 141 adantr 
 |-  ( ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) -> a <_ ( D - 1 ) )
143 142 adantl 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> a <_ ( D - 1 ) )
144 138 ltm1d 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> ( D - 1 ) < D )
145 137 140 138 143 144 lelttrd 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> a < D )
146 137 138 145 ltled 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> a <_ D )
147 128 130 133 136 146 elfzd 
 |-  ( ( ph /\ ( a e. ( 1 ... ( D - 1 ) ) /\ a || D ) ) -> a e. ( 1 ... D ) )
148 147 rabss3d 
 |-  ( ph -> { a e. ( 1 ... ( D - 1 ) ) | a || D } C_ { a e. ( 1 ... D ) | a || D } )
149 148 sseld 
 |-  ( ph -> ( y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } -> y e. { a e. ( 1 ... D ) | a || D } ) )
150 149 imp 
 |-  ( ( ph /\ y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> y e. { a e. ( 1 ... D ) | a || D } )
151 elsni 
 |-  ( y e. { D } -> y = D )
152 151 adantl 
 |-  ( ( ph /\ y e. { D } ) -> y = D )
153 simpr 
 |-  ( ( ph /\ y = D ) -> y = D )
154 breq1 
 |-  ( a = D -> ( a || D <-> D || D ) )
155 1zzd 
 |-  ( ph -> 1 e. ZZ )
156 6 nnzd 
 |-  ( ph -> D e. ZZ )
157 6 nnge1d 
 |-  ( ph -> 1 <_ D )
158 6 nnred 
 |-  ( ph -> D e. RR )
159 158 leidd 
 |-  ( ph -> D <_ D )
160 155 156 156 157 159 elfzd 
 |-  ( ph -> D e. ( 1 ... D ) )
161 iddvds 
 |-  ( D e. ZZ -> D || D )
162 156 161 syl 
 |-  ( ph -> D || D )
163 154 160 162 elrabd 
 |-  ( ph -> D e. { a e. ( 1 ... D ) | a || D } )
164 163 adantr 
 |-  ( ( ph /\ y = D ) -> D e. { a e. ( 1 ... D ) | a || D } )
165 153 164 eqeltrd 
 |-  ( ( ph /\ y = D ) -> y e. { a e. ( 1 ... D ) | a || D } )
166 165 ex 
 |-  ( ph -> ( y = D -> y e. { a e. ( 1 ... D ) | a || D } ) )
167 166 adantr 
 |-  ( ( ph /\ y e. { D } ) -> ( y = D -> y e. { a e. ( 1 ... D ) | a || D } ) )
168 152 167 mpd 
 |-  ( ( ph /\ y e. { D } ) -> y e. { a e. ( 1 ... D ) | a || D } )
169 150 168 jaodan 
 |-  ( ( ph /\ ( y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } \/ y e. { D } ) ) -> y e. { a e. ( 1 ... D ) | a || D } )
170 169 ex 
 |-  ( ph -> ( ( y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } \/ y e. { D } ) -> y e. { a e. ( 1 ... D ) | a || D } ) )
171 170 adantr 
 |-  ( ( ph /\ y e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ) -> ( ( y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } \/ y e. { D } ) -> y e. { a e. ( 1 ... D ) | a || D } ) )
172 127 171 mpd 
 |-  ( ( ph /\ y e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ) -> y e. { a e. ( 1 ... D ) | a || D } )
173 172 ex 
 |-  ( ph -> ( y e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) -> y e. { a e. ( 1 ... D ) | a || D } ) )
174 simpr 
 |-  ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ y = D ) -> y = D )
175 eqidd 
 |-  ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ y = D ) -> D = D )
176 6 ad2antrr 
 |-  ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ y = D ) -> D e. NN )
177 elsng 
 |-  ( D e. NN -> ( D e. { D } <-> D = D ) )
178 176 177 syl 
 |-  ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ y = D ) -> ( D e. { D } <-> D = D ) )
179 175 178 mpbird 
 |-  ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ y = D ) -> D e. { D } )
180 174 179 eqeltrd 
 |-  ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ y = D ) -> y e. { D } )
181 180 olcd 
 |-  ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ y = D ) -> ( y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } \/ y e. { D } ) )
182 breq1 
 |-  ( a = y -> ( a || D <-> y || D ) )
183 182 elrab 
 |-  ( y e. { a e. ( 1 ... D ) | a || D } <-> ( y e. ( 1 ... D ) /\ y || D ) )
184 183 biimpi 
 |-  ( y e. { a e. ( 1 ... D ) | a || D } -> ( y e. ( 1 ... D ) /\ y || D ) )
185 184 adantl 
 |-  ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) -> ( y e. ( 1 ... D ) /\ y || D ) )
186 185 adantr 
 |-  ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) -> ( y e. ( 1 ... D ) /\ y || D ) )
187 1zzd 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> 1 e. ZZ )
188 156 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> D e. ZZ )
189 188 187 zsubcld 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> ( D - 1 ) e. ZZ )
190 elfzelz 
 |-  ( y e. ( 1 ... D ) -> y e. ZZ )
191 190 adantr 
 |-  ( ( y e. ( 1 ... D ) /\ y || D ) -> y e. ZZ )
192 191 adantl 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> y e. ZZ )
193 elfzle1 
 |-  ( y e. ( 1 ... D ) -> 1 <_ y )
194 193 adantr 
 |-  ( ( y e. ( 1 ... D ) /\ y || D ) -> 1 <_ y )
195 194 adantl 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> 1 <_ y )
196 elfzle2 
 |-  ( y e. ( 1 ... D ) -> y <_ D )
197 196 adantr 
 |-  ( ( y e. ( 1 ... D ) /\ y || D ) -> y <_ D )
198 197 adantl 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> y <_ D )
199 neqne 
 |-  ( -. y = D -> y =/= D )
200 199 adantl 
 |-  ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) -> y =/= D )
201 200 necomd 
 |-  ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) -> D =/= y )
202 201 adantr 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> D =/= y )
203 198 202 jca 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> ( y <_ D /\ D =/= y ) )
204 192 zred 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> y e. RR )
205 158 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> D e. RR )
206 204 205 ltlend 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> ( y < D <-> ( y <_ D /\ D =/= y ) ) )
207 203 206 mpbird 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> y < D )
208 6 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> D e. NN )
209 208 nnzd 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> D e. ZZ )
210 192 209 zltlem1d 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> ( y < D <-> y <_ ( D - 1 ) ) )
211 207 210 mpbid 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> y <_ ( D - 1 ) )
212 187 189 192 195 211 elfzd 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> y e. ( 1 ... ( D - 1 ) ) )
213 simprr 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> y || D )
214 182 212 213 elrabd 
 |-  ( ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) /\ ( y e. ( 1 ... D ) /\ y || D ) ) -> y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } )
215 214 ex 
 |-  ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) -> ( ( y e. ( 1 ... D ) /\ y || D ) -> y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) )
216 186 215 mpd 
 |-  ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) -> y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } )
217 216 orcd 
 |-  ( ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) /\ -. y = D ) -> ( y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } \/ y e. { D } ) )
218 181 217 pm2.61dan 
 |-  ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) -> ( y e. { a e. ( 1 ... ( D - 1 ) ) | a || D } \/ y e. { D } ) )
219 218 125 sylibr 
 |-  ( ( ph /\ y e. { a e. ( 1 ... D ) | a || D } ) -> y e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) )
220 219 ex 
 |-  ( ph -> ( y e. { a e. ( 1 ... D ) | a || D } -> y e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ) )
221 173 220 impbid 
 |-  ( ph -> ( y e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) <-> y e. { a e. ( 1 ... D ) | a || D } ) )
222 221 eqrdv 
 |-  ( ph -> ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) = { a e. ( 1 ... D ) | a || D } )
223 222 sumeq1d 
 |-  ( ph -> sum_ k e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ( phi ` k ) = sum_ k e. { a e. ( 1 ... D ) | a || D } ( phi ` k ) )
224 phisum 
 |-  ( D e. NN -> sum_ k e. { a e. NN | a || D } ( phi ` k ) = D )
225 6 224 syl 
 |-  ( ph -> sum_ k e. { a e. NN | a || D } ( phi ` k ) = D )
226 eqcom 
 |-  ( ( ( od ` G ) ` A ) = D <-> D = ( ( od ` G ) ` A ) )
227 226 imbi2i 
 |-  ( ( ph -> ( ( od ` G ) ` A ) = D ) <-> ( ph -> D = ( ( od ` G ) ` A ) ) )
228 9 227 mpbi 
 |-  ( ph -> D = ( ( od ` G ) ` A ) )
229 228 oveq1d 
 |-  ( ph -> ( D .^ x ) = ( ( ( od ` G ) ` A ) .^ x ) )
230 229 eqeq1d 
 |-  ( ph -> ( ( D .^ x ) = ( 0g ` G ) <-> ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) ) )
231 230 rabbidv 
 |-  ( ph -> { x e. B | ( D .^ x ) = ( 0g ` G ) } = { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } )
232 231 fveq2d 
 |-  ( ph -> ( # ` { x e. B | ( D .^ x ) = ( 0g ` G ) } ) = ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) )
233 1 2 3 4 5 8 unitscyglem1 
 |-  ( ph -> ( # ` { x e. B | ( ( ( od ` G ) ` A ) .^ x ) = ( 0g ` G ) } ) = ( ( od ` G ) ` A ) )
234 232 233 eqtrd 
 |-  ( ph -> ( # ` { x e. B | ( D .^ x ) = ( 0g ` G ) } ) = ( ( od ` G ) ` A ) )
235 234 9 eqtr2d 
 |-  ( ph -> D = ( # ` { x e. B | ( D .^ x ) = ( 0g ` G ) } ) )
236 1 2 3 4 6 grpods 
 |-  ( ph -> sum_ k e. { a e. ( 1 ... D ) | a || D } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( # ` { x e. B | ( D .^ x ) = ( 0g ` G ) } ) )
237 235 236 eqtr4d 
 |-  ( ph -> D = sum_ k e. { a e. ( 1 ... D ) | a || D } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) )
238 222 eqcomd 
 |-  ( ph -> { a e. ( 1 ... D ) | a || D } = ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) )
239 238 sumeq1d 
 |-  ( ph -> sum_ k e. { a e. ( 1 ... D ) | a || D } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = sum_ k e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) )
240 237 239 eqtrd 
 |-  ( ph -> D = sum_ k e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) )
241 225 240 eqtr2d 
 |-  ( ph -> sum_ k e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = sum_ k e. { a e. NN | a || D } ( phi ` k ) )
242 1zzd 
 |-  ( ( ph /\ y e. { a e. NN | a || D } ) -> 1 e. ZZ )
243 156 adantr 
 |-  ( ( ph /\ y e. { a e. NN | a || D } ) -> D e. ZZ )
244 182 elrab 
 |-  ( y e. { a e. NN | a || D } <-> ( y e. NN /\ y || D ) )
245 244 biimpi 
 |-  ( y e. { a e. NN | a || D } -> ( y e. NN /\ y || D ) )
246 245 adantl 
 |-  ( ( ph /\ y e. { a e. NN | a || D } ) -> ( y e. NN /\ y || D ) )
247 246 simpld 
 |-  ( ( ph /\ y e. { a e. NN | a || D } ) -> y e. NN )
248 247 nnzd 
 |-  ( ( ph /\ y e. { a e. NN | a || D } ) -> y e. ZZ )
249 247 nnge1d 
 |-  ( ( ph /\ y e. { a e. NN | a || D } ) -> 1 <_ y )
250 246 simprd 
 |-  ( ( ph /\ y e. { a e. NN | a || D } ) -> y || D )
251 6 adantr 
 |-  ( ( ph /\ y e. { a e. NN | a || D } ) -> D e. NN )
252 dvdsle 
 |-  ( ( y e. ZZ /\ D e. NN ) -> ( y || D -> y <_ D ) )
253 248 251 252 syl2anc 
 |-  ( ( ph /\ y e. { a e. NN | a || D } ) -> ( y || D -> y <_ D ) )
254 250 253 mpd 
 |-  ( ( ph /\ y e. { a e. NN | a || D } ) -> y <_ D )
255 242 243 248 249 254 elfzd 
 |-  ( ( ph /\ y e. { a e. NN | a || D } ) -> y e. ( 1 ... D ) )
256 182 255 250 elrabd 
 |-  ( ( ph /\ y e. { a e. NN | a || D } ) -> y e. { a e. ( 1 ... D ) | a || D } )
257 256 ex 
 |-  ( ph -> ( y e. { a e. NN | a || D } -> y e. { a e. ( 1 ... D ) | a || D } ) )
258 elfzelz 
 |-  ( a e. ( 1 ... D ) -> a e. ZZ )
259 elfzle1 
 |-  ( a e. ( 1 ... D ) -> 1 <_ a )
260 258 259 jca 
 |-  ( a e. ( 1 ... D ) -> ( a e. ZZ /\ 1 <_ a ) )
261 260 adantr 
 |-  ( ( a e. ( 1 ... D ) /\ a || D ) -> ( a e. ZZ /\ 1 <_ a ) )
262 261 adantl 
 |-  ( ( ph /\ ( a e. ( 1 ... D ) /\ a || D ) ) -> ( a e. ZZ /\ 1 <_ a ) )
263 elnnz1 
 |-  ( a e. NN <-> ( a e. ZZ /\ 1 <_ a ) )
264 262 263 sylibr 
 |-  ( ( ph /\ ( a e. ( 1 ... D ) /\ a || D ) ) -> a e. NN )
265 264 rabss3d 
 |-  ( ph -> { a e. ( 1 ... D ) | a || D } C_ { a e. NN | a || D } )
266 265 sseld 
 |-  ( ph -> ( y e. { a e. ( 1 ... D ) | a || D } -> y e. { a e. NN | a || D } ) )
267 257 266 impbid 
 |-  ( ph -> ( y e. { a e. NN | a || D } <-> y e. { a e. ( 1 ... D ) | a || D } ) )
268 267 eqrdv 
 |-  ( ph -> { a e. NN | a || D } = { a e. ( 1 ... D ) | a || D } )
269 268 sumeq1d 
 |-  ( ph -> sum_ k e. { a e. NN | a || D } ( phi ` k ) = sum_ k e. { a e. ( 1 ... D ) | a || D } ( phi ` k ) )
270 241 269 eqtr2d 
 |-  ( ph -> sum_ k e. { a e. ( 1 ... D ) | a || D } ( phi ` k ) = sum_ k e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) )
271 223 270 eqtrd 
 |-  ( ph -> sum_ k e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ( phi ` k ) = sum_ k e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) )
272 nfv 
 |-  F/ k ph
273 nfcv 
 |-  F/_ k ( # ` { x e. B | ( ( od ` G ) ` x ) = D } )
274 fzfid 
 |-  ( ph -> ( 1 ... ( D - 1 ) ) e. Fin )
275 ssrab2 
 |-  { a e. ( 1 ... ( D - 1 ) ) | a || D } C_ ( 1 ... ( D - 1 ) )
276 275 a1i 
 |-  ( ph -> { a e. ( 1 ... ( D - 1 ) ) | a || D } C_ ( 1 ... ( D - 1 ) ) )
277 274 276 ssfid 
 |-  ( ph -> { a e. ( 1 ... ( D - 1 ) ) | a || D } e. Fin )
278 154 elrab 
 |-  ( D e. { a e. ( 1 ... ( D - 1 ) ) | a || D } <-> ( D e. ( 1 ... ( D - 1 ) ) /\ D || D ) )
279 278 biimpi 
 |-  ( D e. { a e. ( 1 ... ( D - 1 ) ) | a || D } -> ( D e. ( 1 ... ( D - 1 ) ) /\ D || D ) )
280 279 simpld 
 |-  ( D e. { a e. ( 1 ... ( D - 1 ) ) | a || D } -> D e. ( 1 ... ( D - 1 ) ) )
281 280 adantl 
 |-  ( ( ph /\ D e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> D e. ( 1 ... ( D - 1 ) ) )
282 elfzle2 
 |-  ( D e. ( 1 ... ( D - 1 ) ) -> D <_ ( D - 1 ) )
283 281 282 syl 
 |-  ( ( ph /\ D e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> D <_ ( D - 1 ) )
284 158 ltm1d 
 |-  ( ph -> ( D - 1 ) < D )
285 1red 
 |-  ( ph -> 1 e. RR )
286 158 285 resubcld 
 |-  ( ph -> ( D - 1 ) e. RR )
287 286 158 ltnled 
 |-  ( ph -> ( ( D - 1 ) < D <-> -. D <_ ( D - 1 ) ) )
288 284 287 mpbid 
 |-  ( ph -> -. D <_ ( D - 1 ) )
289 288 adantr 
 |-  ( ( ph /\ D e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> -. D <_ ( D - 1 ) )
290 283 289 pm2.21dd 
 |-  ( ( ph /\ D e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> -. D e. { a e. ( 1 ... ( D - 1 ) ) | a || D } )
291 simpr 
 |-  ( ( ph /\ -. D e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> -. D e. { a e. ( 1 ... ( D - 1 ) ) | a || D } )
292 290 291 pm2.61dan 
 |-  ( ph -> -. D e. { a e. ( 1 ... ( D - 1 ) ) | a || D } )
293 4 adantr 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> B e. Fin )
294 ssrab2 
 |-  { x e. B | ( ( od ` G ) ` x ) = k } C_ B
295 294 a1i 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> { x e. B | ( ( od ` G ) ` x ) = k } C_ B )
296 293 295 ssfid 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> { x e. B | ( ( od ` G ) ` x ) = k } e. Fin )
297 hashcl 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = k } e. Fin -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. NN0 )
298 296 297 syl 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. NN0 )
299 298 nn0cnd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) e. CC )
300 eqeq2 
 |-  ( k = D -> ( ( ( od ` G ) ` x ) = k <-> ( ( od ` G ) ` x ) = D ) )
301 300 rabbidv 
 |-  ( k = D -> { x e. B | ( ( od ` G ) ` x ) = k } = { x e. B | ( ( od ` G ) ` x ) = D } )
302 301 fveq2d 
 |-  ( k = D -> ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) )
303 ssrab2 
 |-  { x e. B | ( ( od ` G ) ` x ) = D } C_ B
304 303 a1i 
 |-  ( ph -> { x e. B | ( ( od ` G ) ` x ) = D } C_ B )
305 4 304 ssfid 
 |-  ( ph -> { x e. B | ( ( od ` G ) ` x ) = D } e. Fin )
306 hashcl 
 |-  ( { x e. B | ( ( od ` G ) ` x ) = D } e. Fin -> ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) e. NN0 )
307 305 306 syl 
 |-  ( ph -> ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) e. NN0 )
308 307 nn0cnd 
 |-  ( ph -> ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) e. CC )
309 272 273 277 6 292 299 302 308 fsumsplitsn 
 |-  ( ph -> sum_ k e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) = ( sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) + ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) ) )
310 271 309 eqtr2d 
 |-  ( ph -> ( sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) + ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) ) = sum_ k e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ( phi ` k ) )
311 nfcv 
 |-  F/_ k ( phi ` D )
312 121 299 eqeltrrd 
 |-  ( ( ph /\ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ) -> ( phi ` k ) e. CC )
313 fveq2 
 |-  ( k = D -> ( phi ` k ) = ( phi ` D ) )
314 6 phicld 
 |-  ( ph -> ( phi ` D ) e. NN )
315 314 nncnd 
 |-  ( ph -> ( phi ` D ) e. CC )
316 272 311 277 6 292 312 313 315 fsumsplitsn 
 |-  ( ph -> sum_ k e. ( { a e. ( 1 ... ( D - 1 ) ) | a || D } u. { D } ) ( phi ` k ) = ( sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( phi ` k ) + ( phi ` D ) ) )
317 310 316 eqtrd 
 |-  ( ph -> ( sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( # ` { x e. B | ( ( od ` G ) ` x ) = k } ) + ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) ) = ( sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( phi ` k ) + ( phi ` D ) ) )
318 124 317 eqtrd 
 |-  ( ph -> ( sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( phi ` k ) + ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) ) = ( sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( phi ` k ) + ( phi ` D ) ) )
319 277 312 fsumcl 
 |-  ( ph -> sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( phi ` k ) e. CC )
320 319 308 315 addcand 
 |-  ( ph -> ( ( sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( phi ` k ) + ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) ) = ( sum_ k e. { a e. ( 1 ... ( D - 1 ) ) | a || D } ( phi ` k ) + ( phi ` D ) ) <-> ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) = ( phi ` D ) ) )
321 318 320 mpbid 
 |-  ( ph -> ( # ` { x e. B | ( ( od ` G ) ` x ) = D } ) = ( phi ` D ) )