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 = {Poly}_{1} (R)$
	ply1degltlss.d	$⊢ D = \deg_{1} (R)$
	ply1degltlss.1	$⊢ S = D^{-1} [[−∞, N)]$
	ply1degltlss.3	$⊢ φ \to N \in ℕ_{0}$
	ply1degltlss.2	$⊢ φ \to R \in Ring$
Assertion	ply1degltlss	$⊢ φ \to S \in LSubSp (P)$

Proof

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

Metamath Proof Explorer

Theorem ply1degltlss

Proof