This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ply1degltlss

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

Ref Expression
Hypotheses ply1degltlss.p 
|- P = ( Poly1 ` R )
ply1degltlss.d 
|- D = ( deg1 ` R )
ply1degltlss.1 
|- S = ( `' D " ( -oo [,) N ) )
ply1degltlss.3 
|- ( ph -> N e. NN0 )
ply1degltlss.2 
|- ( ph -> R e. Ring )
Assertion ply1degltlss 
|- ( ph -> S e. ( LSubSp ` P ) )

Proof

Step Hyp Ref Expression
1 ply1degltlss.p 
 |-  P = ( Poly1 ` R )
2 ply1degltlss.d 
 |-  D = ( deg1 ` R )
3 ply1degltlss.1 
 |-  S = ( `' D " ( -oo [,) N ) )
4 ply1degltlss.3 
 |-  ( ph -> N e. NN0 )
5 ply1degltlss.2 
 |-  ( ph -> R e. Ring )
6 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
7 5 6 syl 
 |-  ( ph -> R = ( Scalar ` P ) )
8 eqidd 
 |-  ( ph -> ( Base ` R ) = ( Base ` R ) )
9 eqidd 
 |-  ( ph -> ( Base ` P ) = ( Base ` P ) )
10 eqidd 
 |-  ( ph -> ( +g ` P ) = ( +g ` P ) )
11 eqidd 
 |-  ( ph -> ( .s ` P ) = ( .s ` P ) )
12 eqidd 
 |-  ( ph -> ( LSubSp ` P ) = ( LSubSp ` P ) )
13 cnvimass 
 |-  ( `' D " ( -oo [,) N ) ) C_ dom D
14 3 13 eqsstri 
 |-  S C_ dom D
15 eqid 
 |-  ( Base ` P ) = ( Base ` P )
16 2 1 15 deg1xrf 
 |-  D : ( Base ` P ) --> RR*
17 16 fdmi 
 |-  dom D = ( Base ` P )
18 14 17 sseqtri 
 |-  S C_ ( Base ` P )
19 18 a1i 
 |-  ( ph -> S C_ ( Base ` P ) )
20 16 a1i 
 |-  ( ph -> D : ( Base ` P ) --> RR* )
21 20 ffnd 
 |-  ( ph -> D Fn ( Base ` P ) )
22 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
23 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
24 15 23 ring0cl 
 |-  ( P e. Ring -> ( 0g ` P ) e. ( Base ` P ) )
25 5 22 24 3syl 
 |-  ( ph -> ( 0g ` P ) e. ( Base ` P ) )
26 2 1 23 deg1z 
 |-  ( R e. Ring -> ( D ` ( 0g ` P ) ) = -oo )
27 5 26 syl 
 |-  ( ph -> ( D ` ( 0g ` P ) ) = -oo )
28 mnfxr 
 |-  -oo e. RR*
29 28 a1i 
 |-  ( ph -> -oo e. RR* )
30 4 nn0red 
 |-  ( ph -> N e. RR )
31 30 rexrd 
 |-  ( ph -> N e. RR* )
32 29 xrleidd 
 |-  ( ph -> -oo <_ -oo )
33 30 mnfltd 
 |-  ( ph -> -oo < N )
34 29 31 29 32 33 elicod 
 |-  ( ph -> -oo e. ( -oo [,) N ) )
35 27 34 eqeltrd 
 |-  ( ph -> ( D ` ( 0g ` P ) ) e. ( -oo [,) N ) )
36 21 25 35 elpreimad 
 |-  ( ph -> ( 0g ` P ) e. ( `' D " ( -oo [,) N ) ) )
37 36 3 eleqtrrdi 
 |-  ( ph -> ( 0g ` P ) e. S )
38 37 ne0d 
 |-  ( ph -> S =/= (/) )
39 simpl 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> ph )
40 eqid 
 |-  ( +g ` P ) = ( +g ` P )
41 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
42 5 41 syl 
 |-  ( ph -> P e. LMod )
43 42 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> P e. LMod )
44 43 lmodgrpd 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> P e. Grp )
45 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> x e. ( Base ` R ) )
46 7 fveq2d 
 |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
47 46 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
48 45 47 eleqtrd 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> x e. ( Base ` ( Scalar ` P ) ) )
49 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> a e. S )
50 18 49 sselid 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> a e. ( Base ` P ) )
51 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
52 eqid 
 |-  ( .s ` P ) = ( .s ` P )
53 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
54 15 51 52 53 lmodvscl 
 |-  ( ( P e. LMod /\ x e. ( Base ` ( Scalar ` P ) ) /\ a e. ( Base ` P ) ) -> ( x ( .s ` P ) a ) e. ( Base ` P ) )
55 43 48 50 54 syl3anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> ( x ( .s ` P ) a ) e. ( Base ` P ) )
56 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> b e. S )
57 18 56 sselid 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> b e. ( Base ` P ) )
58 15 40 44 55 57 grpcld 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> ( ( x ( .s ` P ) a ) ( +g ` P ) b ) e. ( Base ` P ) )
59 5 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> R e. Ring )
60 1red 
 |-  ( ph -> 1 e. RR )
61 30 60 resubcld 
 |-  ( ph -> ( N - 1 ) e. RR )
62 61 rexrd 
 |-  ( ph -> ( N - 1 ) e. RR* )
63 62 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> ( N - 1 ) e. RR* )
64 16 a1i 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> D : ( Base ` P ) --> RR* )
65 64 55 ffvelcdmd 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> ( D ` ( x ( .s ` P ) a ) ) e. RR* )
66 64 50 ffvelcdmd 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> ( D ` a ) e. RR* )
67 eqid 
 |-  ( Base ` R ) = ( Base ` R )
68 1 2 59 15 67 52 45 50 deg1vscale 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> ( D ` ( x ( .s ` P ) a ) ) <_ ( D ` a ) )
69 1 2 3 4 5 15 ply1degltel 
 |-  ( ph -> ( a e. S <-> ( a e. ( Base ` P ) /\ ( D ` a ) <_ ( N - 1 ) ) ) )
70 69 simplbda 
 |-  ( ( ph /\ a e. S ) -> ( D ` a ) <_ ( N - 1 ) )
71 49 70 syldan 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> ( D ` a ) <_ ( N - 1 ) )
72 65 66 63 68 71 xrletrd 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> ( D ` ( x ( .s ` P ) a ) ) <_ ( N - 1 ) )
73 1 2 3 4 5 15 ply1degltel 
 |-  ( ph -> ( b e. S <-> ( b e. ( Base ` P ) /\ ( D ` b ) <_ ( N - 1 ) ) ) )
74 73 simplbda 
 |-  ( ( ph /\ b e. S ) -> ( D ` b ) <_ ( N - 1 ) )
75 56 74 syldan 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> ( D ` b ) <_ ( N - 1 ) )
76 1 2 59 15 40 55 57 63 72 75 deg1addle2 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> ( D ` ( ( x ( .s ` P ) a ) ( +g ` P ) b ) ) <_ ( N - 1 ) )
77 1 2 3 4 5 15 ply1degltel 
 |-  ( ph -> ( ( ( x ( .s ` P ) a ) ( +g ` P ) b ) e. S <-> ( ( ( x ( .s ` P ) a ) ( +g ` P ) b ) e. ( Base ` P ) /\ ( D ` ( ( x ( .s ` P ) a ) ( +g ` P ) b ) ) <_ ( N - 1 ) ) ) )
78 77 biimpar 
 |-  ( ( ph /\ ( ( ( x ( .s ` P ) a ) ( +g ` P ) b ) e. ( Base ` P ) /\ ( D ` ( ( x ( .s ` P ) a ) ( +g ` P ) b ) ) <_ ( N - 1 ) ) ) -> ( ( x ( .s ` P ) a ) ( +g ` P ) b ) e. S )
79 39 58 76 78 syl12anc 
 |-  ( ( ph /\ ( x e. ( Base ` R ) /\ a e. S /\ b e. S ) ) -> ( ( x ( .s ` P ) a ) ( +g ` P ) b ) e. S )
80 7 8 9 10 11 12 19 38 79 islssd 
 |-  ( ph -> S e. ( LSubSp ` P ) )