Metamath Proof Explorer

Theorem hashscontpowcl

Description: Closure of E for https://www3.nd.edu/%7eandyp/notes/AKS.pdf Theorem 6.1. (Contributed by metakunt, 28-Apr-2025)

Ref Expression
Hypotheses hashscontpowcl.1 
|- ( ph -> N e. NN )
hashscontpowcl.2 
|- ( ph -> P e. Prime )
hashscontpowcl.3 
|- ( ph -> P || N )
hashscontpowcl.4 
|- ( ph -> R e. NN )
hashscontpowcl.5 
|- ( ph -> ( N gcd R ) = 1 )
hashscontpowcl.6 
|- E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
hashscontpowcl.7 
|- L = ( ZRHom ` Y )
hashscontpowcl.8 
|- Y = ( Z/nZ ` R )
Assertion hashscontpowcl 
|- ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 )

Proof

Step Hyp Ref Expression
1 hashscontpowcl.1 
 |-  ( ph -> N e. NN )
2 hashscontpowcl.2 
 |-  ( ph -> P e. Prime )
3 hashscontpowcl.3 
 |-  ( ph -> P || N )
4 hashscontpowcl.4 
 |-  ( ph -> R e. NN )
5 hashscontpowcl.5 
 |-  ( ph -> ( N gcd R ) = 1 )
6 hashscontpowcl.6 
 |-  E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
7 hashscontpowcl.7 
 |-  L = ( ZRHom ` Y )
8 hashscontpowcl.8 
 |-  Y = ( Z/nZ ` R )
9 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
10 8 9 znfi 
 |-  ( R e. NN -> ( Base ` Y ) e. Fin )
11 4 10 syl 
 |-  ( ph -> ( Base ` Y ) e. Fin )
12 4 nnnn0d 
 |-  ( ph -> R e. NN0 )
13 8 zncrng 
 |-  ( R e. NN0 -> Y e. CRing )
14 12 13 syl 
 |-  ( ph -> Y e. CRing )
15 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
16 14 15 syl 
 |-  ( ph -> Y e. Ring )
17 7 zrhrhm 
 |-  ( Y e. Ring -> L e. ( ZZring RingHom Y ) )
18 zringbas 
 |-  ZZ = ( Base ` ZZring )
19 18 9 rhmf 
 |-  ( L e. ( ZZring RingHom Y ) -> L : ZZ --> ( Base ` Y ) )
20 fimass 
 |-  ( L : ZZ --> ( Base ` Y ) -> ( L " ( E " ( NN0 X. NN0 ) ) ) C_ ( Base ` Y ) )
21 16 17 19 20 4syl 
 |-  ( ph -> ( L " ( E " ( NN0 X. NN0 ) ) ) C_ ( Base ` Y ) )
22 11 21 ssfid 
 |-  ( ph -> ( L " ( E " ( NN0 X. NN0 ) ) ) e. Fin )
23 hashcl 
 |-  ( ( L " ( E " ( NN0 X. NN0 ) ) ) e. Fin -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 )
24 22 23 syl 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 )