Metamath Proof Explorer

Theorem aks6d1c7lem3

Description: Remove lots of hypotheses now that we have the AKS contradiction. (Contributed by metakunt, 16-May-2025)

Ref Expression
Hypotheses aks6d1c7.1 
|- .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
aks6d1c7.2 
|- P = ( chr ` K )
aks6d1c7.3 
|- ( ph -> K e. Field )
aks6d1c7.4 
|- ( ph -> P e. Prime )
aks6d1c7.5 
|- ( ph -> R e. NN )
aks6d1c7.6 
|- ( ph -> N e. ( ZZ>= ` 3 ) )
aks6d1c7.7 
|- ( ph -> P || N )
aks6d1c7.8 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c7.9 
|- A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
aks6d1c7.10 
|- ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
aks6d1c7.11 
|- ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
aks6d1c7.12 
|- ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
aks6d1c7.13 
|- ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
aks6d1c7.14 
|- ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
aks6d1c7lem3.1 
|- ( ph -> ( Q e. Prime /\ Q || N ) )
Assertion aks6d1c7lem3 
|- ( ph -> P = Q )

Proof

Step Hyp Ref Expression
1 aks6d1c7.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
2 aks6d1c7.2 
 |-  P = ( chr ` K )
3 aks6d1c7.3 
 |-  ( ph -> K e. Field )
4 aks6d1c7.4 
 |-  ( ph -> P e. Prime )
5 aks6d1c7.5 
 |-  ( ph -> R e. NN )
6 aks6d1c7.6 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
7 aks6d1c7.7 
 |-  ( ph -> P || N )
8 aks6d1c7.8 
 |-  ( ph -> ( N gcd R ) = 1 )
9 aks6d1c7.9 
 |-  A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
10 aks6d1c7.10 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
11 aks6d1c7.11 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
12 aks6d1c7.12 
 |-  ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
13 aks6d1c7.13 
 |-  ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
14 aks6d1c7.14 
 |-  ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
15 aks6d1c7lem3.1 
 |-  ( ph -> ( Q e. Prime /\ Q || N ) )
16 nfcv 
 |-  F/_ k ( ( P ^ i ) x. ( ( N / P ) ^ j ) )
17 nfcv 
 |-  F/_ l ( ( P ^ i ) x. ( ( N / P ) ^ j ) )
18 nfcv 
 |-  F/_ i ( ( P ^ k ) x. ( ( N / P ) ^ l ) )
19 nfcv 
 |-  F/_ j ( ( P ^ k ) x. ( ( N / P ) ^ l ) )
20 simpl 
 |-  ( ( i = k /\ j = l ) -> i = k )
21 20 oveq2d 
 |-  ( ( i = k /\ j = l ) -> ( P ^ i ) = ( P ^ k ) )
22 simpr 
 |-  ( ( i = k /\ j = l ) -> j = l )
23 22 oveq2d 
 |-  ( ( i = k /\ j = l ) -> ( ( N / P ) ^ j ) = ( ( N / P ) ^ l ) )
24 21 23 oveq12d 
 |-  ( ( i = k /\ j = l ) -> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) = ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
25 16 17 18 19 24 cbvmpo 
 |-  ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
26 eqid 
 |-  ( ZRHom ` ( Z/nZ ` R ) ) = ( ZRHom ` ( Z/nZ ` R ) )
27 eqid 
 |-  ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) ) = ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) )
28 nfcv 
 |-  F/_ v ( ( ( eval1 ` K ) ` ( ( m e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) ) ) ` w ) ) ` M )
29 nfcv 
 |-  F/_ w ( ( ( eval1 ` K ) ` ( ( m e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) ) ) ` v ) ) ` M )
30 2fveq3 
 |-  ( w = v -> ( ( eval1 ` K ) ` ( ( m e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) ) ) ` w ) ) = ( ( eval1 ` K ) ` ( ( m e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) ) ) ` v ) ) )
31 30 fveq1d 
 |-  ( w = v -> ( ( ( eval1 ` K ) ` ( ( m e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) ) ) ` w ) ) ` M ) = ( ( ( eval1 ` K ) ` ( ( m e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) ) ) ` v ) ) ` M ) )
32 28 29 31 cbvmpt 
 |-  ( w e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( ( m e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) ) ) ` w ) ) ` M ) ) = ( v e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( ( m e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) ) ) ` v ) ) ` M ) )
33 eqid 
 |-  ( |_ ` ( sqrt ` ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) ) ) ) = ( |_ ` ( sqrt ` ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) ) ) )
34 eqid 
 |-  ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( ( 0 ... ( |_ ` ( sqrt ` ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) ) ) ) ) X. ( 0 ... ( |_ ` ( sqrt ` ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) ) ) ) ) ) ) = ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( ( 0 ... ( |_ ` ( sqrt ` ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) ) ) ) ) X. ( 0 ... ( |_ ` ( sqrt ` ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) ) ) ) ) ) )
35 nfcv 
 |-  F/_ g ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) )
36 nfcv 
 |-  F/_ m ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( h e. ( 0 ... A ) |-> ( ( g ` h ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) ) ) ) )
37 nfcv 
 |-  F/_ h ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) )
38 nfcv 
 |-  F/_ n ( ( m ` h ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) ) )
39 fveq2 
 |-  ( n = h -> ( m ` n ) = ( m ` h ) )
40 2fveq3 
 |-  ( n = h -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) = ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) )
41 40 oveq2d 
 |-  ( n = h -> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) = ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) ) )
42 39 41 oveq12d 
 |-  ( n = h -> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) = ( ( m ` h ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) ) ) )
43 37 38 42 cbvmpt 
 |-  ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) = ( h e. ( 0 ... A ) |-> ( ( m ` h ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) ) ) )
44 43 a1i 
 |-  ( m = g -> ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) = ( h e. ( 0 ... A ) |-> ( ( m ` h ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) ) ) ) )
45 simpl 
 |-  ( ( m = g /\ h e. ( 0 ... A ) ) -> m = g )
46 45 fveq1d 
 |-  ( ( m = g /\ h e. ( 0 ... A ) ) -> ( m ` h ) = ( g ` h ) )
47 46 oveq1d 
 |-  ( ( m = g /\ h e. ( 0 ... A ) ) -> ( ( m ` h ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) ) ) = ( ( g ` h ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) ) ) )
48 47 mpteq2dva 
 |-  ( m = g -> ( h e. ( 0 ... A ) |-> ( ( m ` h ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) ) ) ) = ( h e. ( 0 ... A ) |-> ( ( g ` h ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) ) ) ) )
49 44 48 eqtrd 
 |-  ( m = g -> ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) = ( h e. ( 0 ... A ) |-> ( ( g ` h ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) ) ) ) )
50 49 oveq2d 
 |-  ( m = g -> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) ) = ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( h e. ( 0 ... A ) |-> ( ( g ` h ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) ) ) ) ) )
51 35 36 50 cbvmpt 
 |-  ( m e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( n e. ( 0 ... A ) |-> ( ( m ` n ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` n ) ) ) ) ) ) ) = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( h e. ( 0 ... A ) |-> ( ( g ` h ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` h ) ) ) ) ) ) )
52 nfcv 
 |-  F/_ u ( NN0 ^m ( 0 ... A ) )
53 nfcv 
 |-  F/_ o ( NN0 ^m ( 0 ... A ) )
54 nfv 
 |-  F/ o sum_ q e. ( 0 ... A ) ( u ` q ) <_ ( ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) " ( NN0 X. NN0 ) ) ) ) - 1 )
55 nfv 
 |-  F/ u sum_ p e. ( 0 ... A ) ( o ` p ) <_ ( ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) ) - 1 )
56 simpl 
 |-  ( ( u = o /\ q e. ( 0 ... A ) ) -> u = o )
57 56 fveq1d 
 |-  ( ( u = o /\ q e. ( 0 ... A ) ) -> ( u ` q ) = ( o ` q ) )
58 57 sumeq2dv 
 |-  ( u = o -> sum_ q e. ( 0 ... A ) ( u ` q ) = sum_ q e. ( 0 ... A ) ( o ` q ) )
59 fveq2 
 |-  ( q = p -> ( o ` q ) = ( o ` p ) )
60 nfcv 
 |-  F/_ p ( o ` q )
61 nfcv 
 |-  F/_ q ( o ` p )
62 59 60 61 cbvsum 
 |-  sum_ q e. ( 0 ... A ) ( o ` q ) = sum_ p e. ( 0 ... A ) ( o ` p )
63 62 a1i 
 |-  ( u = o -> sum_ q e. ( 0 ... A ) ( o ` q ) = sum_ p e. ( 0 ... A ) ( o ` p ) )
64 58 63 eqtrd 
 |-  ( u = o -> sum_ q e. ( 0 ... A ) ( u ` q ) = sum_ p e. ( 0 ... A ) ( o ` p ) )
65 25 eqcomi 
 |-  ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) = ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) )
66 65 a1i 
 |-  ( u = o -> ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) = ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) )
67 66 imaeq1d 
 |-  ( u = o -> ( ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) " ( NN0 X. NN0 ) ) = ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) )
68 67 imaeq2d 
 |-  ( u = o -> ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) " ( NN0 X. NN0 ) ) ) = ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) )
69 68 fveq2d 
 |-  ( u = o -> ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) " ( NN0 X. NN0 ) ) ) ) = ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) ) )
70 69 oveq1d 
 |-  ( u = o -> ( ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) " ( NN0 X. NN0 ) ) ) ) - 1 ) = ( ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) ) - 1 ) )
71 64 70 breq12d 
 |-  ( u = o -> ( sum_ q e. ( 0 ... A ) ( u ` q ) <_ ( ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) " ( NN0 X. NN0 ) ) ) ) - 1 ) <-> sum_ p e. ( 0 ... A ) ( o ` p ) <_ ( ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) ) - 1 ) ) )
72 52 53 54 55 71 cbvrabw 
 |-  { u e. ( NN0 ^m ( 0 ... A ) ) | sum_ q e. ( 0 ... A ) ( u ` q ) <_ ( ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) ) " ( NN0 X. NN0 ) ) ) ) - 1 ) } = { o e. ( NN0 ^m ( 0 ... A ) ) | sum_ p e. ( 0 ... A ) ( o ` p ) <_ ( ( # ` ( ( ZRHom ` ( Z/nZ ` R ) ) " ( ( i e. NN0 , j e. NN0 |-> ( ( P ^ i ) x. ( ( N / P ) ^ j ) ) ) " ( NN0 X. NN0 ) ) ) ) - 1 ) }
73 1 2 3 4 5 6 7 8 25 26 27 9 10 11 12 32 33 34 15 13 51 14 72 aks6d1c7lem2 
 |-  ( ph -> P = Q )