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 ) )