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