Metamath Proof Explorer

Theorem ply1degltdim

Description: The space S of the univariate polynomials of degree less than N has dimension N . (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses ply1degltdim.p 
|- P = ( Poly1 ` R )
ply1degltdim.d 
|- D = ( deg1 ` R )
ply1degltdim.s 
|- S = ( `' D " ( -oo [,) N ) )
ply1degltdim.n 
|- ( ph -> N e. NN0 )
ply1degltdim.r 
|- ( ph -> R e. DivRing )
ply1degltdim.e 
|- E = ( P |`s S )
Assertion ply1degltdim 
|- ( ph -> ( dim ` E ) = N )

Proof

Step Hyp Ref Expression
1 ply1degltdim.p 
 |-  P = ( Poly1 ` R )
2 ply1degltdim.d 
 |-  D = ( deg1 ` R )
3 ply1degltdim.s 
 |-  S = ( `' D " ( -oo [,) N ) )
4 ply1degltdim.n 
 |-  ( ph -> N e. NN0 )
5 ply1degltdim.r 
 |-  ( ph -> R e. DivRing )
6 ply1degltdim.e 
 |-  E = ( P |`s S )
7 1 5 ply1lvec 
 |-  ( ph -> P e. LVec )
8 5 drngringd 
 |-  ( ph -> R e. Ring )
9 1 2 3 4 8 ply1degltlss 
 |-  ( ph -> S e. ( LSubSp ` P ) )
10 eqid 
 |-  ( LSubSp ` P ) = ( LSubSp ` P )
11 6 10 lsslvec 
 |-  ( ( P e. LVec /\ S e. ( LSubSp ` P ) ) -> E e. LVec )
12 7 9 11 syl2anc 
 |-  ( ph -> E e. LVec )
13 oveq1 
 |-  ( k = n -> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
14 13 cbvmptv 
 |-  ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) = ( n e. ( 0 ..^ N ) |-> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
15 1 2 3 4 5 6 14 ply1degltdimlem 
 |-  ( ph -> ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. ( LBasis ` E ) )
16 eqid 
 |-  ( Base ` P ) = ( Base ` P )
17 2 1 16 deg1xrf 
 |-  D : ( Base ` P ) --> RR*
18 ffn 
 |-  ( D : ( Base ` P ) --> RR* -> D Fn ( Base ` P ) )
19 17 18 mp1i 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> D Fn ( Base ` P ) )
20 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
21 20 16 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
22 eqid 
 |-  ( .g ` ( mulGrp ` P ) ) = ( .g ` ( mulGrp ` P ) )
23 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
24 20 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
25 8 23 24 3syl 
 |-  ( ph -> ( mulGrp ` P ) e. Mnd )
26 25 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( mulGrp ` P ) e. Mnd )
27 elfzonn0 
 |-  ( n e. ( 0 ..^ N ) -> n e. NN0 )
28 27 adantl 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> n e. NN0 )
29 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
30 29 1 16 vr1cl 
 |-  ( R e. Ring -> ( var1 ` R ) e. ( Base ` P ) )
31 8 30 syl 
 |-  ( ph -> ( var1 ` R ) e. ( Base ` P ) )
32 31 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( var1 ` R ) e. ( Base ` P ) )
33 21 22 26 28 32 mulgnn0cld 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) )
34 mnfxr 
 |-  -oo e. RR*
35 34 a1i 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> -oo e. RR* )
36 4 nn0red 
 |-  ( ph -> N e. RR )
37 36 rexrd 
 |-  ( ph -> N e. RR* )
38 37 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> N e. RR* )
39 2 1 16 deg1xrcl 
 |-  ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` P ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. RR* )
40 33 39 syl 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. RR* )
41 40 mnfled 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> -oo <_ ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) )
42 27 nn0red 
 |-  ( n e. ( 0 ..^ N ) -> n e. RR )
43 42 rexrd 
 |-  ( n e. ( 0 ..^ N ) -> n e. RR* )
44 43 adantl 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> n e. RR* )
45 2 1 29 20 22 deg1pwle 
 |-  ( ( R e. Ring /\ n e. NN0 ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) <_ n )
46 8 27 45 syl2an 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) <_ n )
47 elfzolt2 
 |-  ( n e. ( 0 ..^ N ) -> n < N )
48 47 adantl 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> n < N )
49 40 44 38 46 48 xrlelttrd 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) < N )
50 35 38 40 41 49 elicod 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( D ` ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. ( -oo [,) N ) )
51 19 33 50 elpreimad 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( `' D " ( -oo [,) N ) ) )
52 51 3 eleqtrrdi 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. S )
53 16 10 lssss 
 |-  ( S e. ( LSubSp ` P ) -> S C_ ( Base ` P ) )
54 6 16 ressbas2 
 |-  ( S C_ ( Base ` P ) -> S = ( Base ` E ) )
55 9 53 54 3syl 
 |-  ( ph -> S = ( Base ` E ) )
56 55 adantr 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> S = ( Base ` E ) )
57 52 56 eleqtrd 
 |-  ( ( ph /\ n e. ( 0 ..^ N ) ) -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` E ) )
58 57 14 fmptd 
 |-  ( ph -> ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) : ( 0 ..^ N ) --> ( Base ` E ) )
59 58 ffnd 
 |-  ( ph -> ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) Fn ( 0 ..^ N ) )
60 hashfn 
 |-  ( ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) Fn ( 0 ..^ N ) -> ( # ` ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( # ` ( 0 ..^ N ) ) )
61 59 60 syl 
 |-  ( ph -> ( # ` ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( # ` ( 0 ..^ N ) ) )
62 ovexd 
 |-  ( ph -> ( 0 ..^ N ) e. _V )
63 57 ralrimiva 
 |-  ( ph -> A. n e. ( 0 ..^ N ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` E ) )
64 drngnzr 
 |-  ( R e. DivRing -> R e. NzRing )
65 5 64 syl 
 |-  ( ph -> R e. NzRing )
66 65 ad2antrr 
 |-  ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> R e. NzRing )
67 28 adantr 
 |-  ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> n e. NN0 )
68 elfzonn0 
 |-  ( i e. ( 0 ..^ N ) -> i e. NN0 )
69 68 adantl 
 |-  ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> i e. NN0 )
70 1 29 22 66 67 69 ply1moneq 
 |-  ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) <-> n = i ) )
71 70 biimpd 
 |-  ( ( ( ph /\ n e. ( 0 ..^ N ) ) /\ i e. ( 0 ..^ N ) ) -> ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) -> n = i ) )
72 71 anasss 
 |-  ( ( ph /\ ( n e. ( 0 ..^ N ) /\ i e. ( 0 ..^ N ) ) ) -> ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) -> n = i ) )
73 72 ralrimivva 
 |-  ( ph -> A. n e. ( 0 ..^ N ) A. i e. ( 0 ..^ N ) ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) -> n = i ) )
74 oveq1 
 |-  ( n = i -> ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) )
75 14 74 f1mpt 
 |-  ( ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) : ( 0 ..^ N ) -1-1-> ( Base ` E ) <-> ( A. n e. ( 0 ..^ N ) ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) e. ( Base ` E ) /\ A. n e. ( 0 ..^ N ) A. i e. ( 0 ..^ N ) ( ( n ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) = ( i ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) -> n = i ) ) )
76 63 73 75 sylanbrc 
 |-  ( ph -> ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) : ( 0 ..^ N ) -1-1-> ( Base ` E ) )
77 hashf1rn 
 |-  ( ( ( 0 ..^ N ) e. _V /\ ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) : ( 0 ..^ N ) -1-1-> ( Base ` E ) ) -> ( # ` ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( # ` ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) )
78 62 76 77 syl2anc 
 |-  ( ph -> ( # ` ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = ( # ` ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) )
79 hashfzo0 
 |-  ( N e. NN0 -> ( # ` ( 0 ..^ N ) ) = N )
80 4 79 syl 
 |-  ( ph -> ( # ` ( 0 ..^ N ) ) = N )
81 61 78 80 3eqtr3d 
 |-  ( ph -> ( # ` ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = N )
82 hashvnfin 
 |-  ( ( ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. ( LBasis ` E ) /\ N e. NN0 ) -> ( ( # ` ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = N -> ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. Fin ) )
83 82 imp 
 |-  ( ( ( ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. ( LBasis ` E ) /\ N e. NN0 ) /\ ( # ` ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) = N ) -> ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. Fin )
84 15 4 81 83 syl21anc 
 |-  ( ph -> ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. Fin )
85 eqid 
 |-  ( LBasis ` E ) = ( LBasis ` E )
86 85 dimvalfi 
 |-  ( ( E e. LVec /\ ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. ( LBasis ` E ) /\ ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) e. Fin ) -> ( dim ` E ) = ( # ` ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) )
87 12 15 84 86 syl3anc 
 |-  ( ph -> ( dim ` E ) = ( # ` ran ( k e. ( 0 ..^ N ) |-> ( k ( .g ` ( mulGrp ` P ) ) ( var1 ` R ) ) ) ) )
88 87 81 eqtrd 
 |-  ( ph -> ( dim ` E ) = N )