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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1degltlss.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
ply1degltlss.1 ⊢ 𝑆 = ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) )
ply1degltlss.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
ply1degltlss.2 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion ply1degltlss ( 𝜑 → 𝑆 ∈ ( LSubSp ‘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 ply1degltlss.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1degltlss.d ⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3 ply1degltlss.1 ⊢ 𝑆 = ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) )
4 ply1degltlss.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 ply1degltlss.2 ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 1 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
7 5 6 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
8 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
9 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) )
10 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 ) )
11 eqidd ⊢ ( 𝜑 → ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 ) )
12 eqidd ⊢ ( 𝜑 → ( LSubSp ‘ 𝑃 ) = ( LSubSp ‘ 𝑃 ) )
13 cnvimass ⊢ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) ⊆ dom 𝐷
14 3 13 eqsstri ⊢ 𝑆 ⊆ dom 𝐷
15 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
16 2 1 15 deg1xrf ⊢ 𝐷 : ( Base ‘ 𝑃 ) ⟶ ℝ*
17 16 fdmi ⊢ dom 𝐷 = ( Base ‘ 𝑃 )
18 14 17 sseqtri ⊢ 𝑆 ⊆ ( Base ‘ 𝑃 )
19 18 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝑃 ) )
20 16 a1i ⊢ ( 𝜑 → 𝐷 : ( Base ‘ 𝑃 ) ⟶ ℝ* )
21 20 ffnd ⊢ ( 𝜑 → 𝐷 Fn ( Base ‘ 𝑃 ) )
22 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
23 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
24 15 23 ring0cl ⊢ ( 𝑃 ∈ Ring → ( 0g ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
25 5 22 24 3syl ⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
26 2 1 23 deg1z ⊢ ( 𝑅 ∈ Ring → ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
27 5 26 syl ⊢ ( 𝜑 → ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
28 mnfxr ⊢ -∞ ∈ ℝ*
29 28 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
30 4 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
31 30 rexrd ⊢ ( 𝜑 → 𝑁 ∈ ℝ* )
32 29 xrleidd ⊢ ( 𝜑 → -∞ ≤ -∞ )
33 30 mnfltd ⊢ ( 𝜑 → -∞ < 𝑁 )
34 29 31 29 32 33 elicod ⊢ ( 𝜑 → -∞ ∈ ( -∞ [,) 𝑁 ) )
35 27 34 eqeltrd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) ∈ ( -∞ [,) 𝑁 ) )
36 21 25 35 elpreimad ⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) )
37 36 3 eleqtrrdi ⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ 𝑆 )
38 37 ne0d ⊢ ( 𝜑 → 𝑆 ≠ ∅ )
39 simpl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → 𝜑 )
40 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
41 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
42 5 41 syl ⊢ ( 𝜑 → 𝑃 ∈ LMod )
43 42 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → 𝑃 ∈ LMod )
44 43 lmodgrpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → 𝑃 ∈ Grp )
45 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
46 7 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
48 45 47 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
49 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → 𝑎 ∈ 𝑆 )
50 18 49 sselid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → 𝑎 ∈ ( Base ‘ 𝑃 ) )
51 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
52 eqid ⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
53 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
54 15 51 52 53 lmodvscl ⊢ ( ( 𝑃 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ∈ ( Base ‘ 𝑃 ) )
55 43 48 50 54 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ∈ ( Base ‘ 𝑃 ) )
56 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → 𝑏 ∈ 𝑆 )
57 18 56 sselid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → 𝑏 ∈ ( Base ‘ 𝑃 ) )
58 15 40 44 55 57 grpcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ( +g ‘ 𝑃 ) 𝑏 ) ∈ ( Base ‘ 𝑃 ) )
59 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → 𝑅 ∈ Ring )
60 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
61 30 60 resubcld ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
62 61 rexrd ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ* )
63 62 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑁 − 1 ) ∈ ℝ* )
64 16 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → 𝐷 : ( Base ‘ 𝑃 ) ⟶ ℝ* )
65 64 55 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝐷 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ) ∈ ℝ* )
66 64 50 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝐷 ‘ 𝑎 ) ∈ ℝ* )
67 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
68 1 2 59 15 67 52 45 50 deg1vscale ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝐷 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ) ≤ ( 𝐷 ‘ 𝑎 ) )
69 1 2 3 4 5 15 ply1degltel ⊢ ( 𝜑 → ( 𝑎 ∈ 𝑆 ↔ ( 𝑎 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐷 ‘ 𝑎 ) ≤ ( 𝑁 − 1 ) ) ) )
70 69 simplbda ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) → ( 𝐷 ‘ 𝑎 ) ≤ ( 𝑁 − 1 ) )
71 49 70 syldan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝐷 ‘ 𝑎 ) ≤ ( 𝑁 − 1 ) )
72 65 66 63 68 71 xrletrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝐷 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ) ≤ ( 𝑁 − 1 ) )
73 1 2 3 4 5 15 ply1degltel ⊢ ( 𝜑 → ( 𝑏 ∈ 𝑆 ↔ ( 𝑏 ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐷 ‘ 𝑏 ) ≤ ( 𝑁 − 1 ) ) ) )
74 73 simplbda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑆 ) → ( 𝐷 ‘ 𝑏 ) ≤ ( 𝑁 − 1 ) )
75 56 74 syldan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝐷 ‘ 𝑏 ) ≤ ( 𝑁 − 1 ) )
76 1 2 59 15 40 55 57 63 72 75 deg1addle2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝐷 ‘ ( ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ( +g ‘ 𝑃 ) 𝑏 ) ) ≤ ( 𝑁 − 1 ) )
77 1 2 3 4 5 15 ply1degltel ⊢ ( 𝜑 → ( ( ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ( +g ‘ 𝑃 ) 𝑏 ) ∈ 𝑆 ↔ ( ( ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ( +g ‘ 𝑃 ) 𝑏 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐷 ‘ ( ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ( +g ‘ 𝑃 ) 𝑏 ) ) ≤ ( 𝑁 − 1 ) ) ) )
78 77 biimpar ⊢ ( ( 𝜑 ∧ ( ( ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ( +g ‘ 𝑃 ) 𝑏 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐷 ‘ ( ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ( +g ‘ 𝑃 ) 𝑏 ) ) ≤ ( 𝑁 − 1 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ( +g ‘ 𝑃 ) 𝑏 ) ∈ 𝑆 )
79 39 58 76 78 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑃 ) 𝑎 ) ( +g ‘ 𝑃 ) 𝑏 ) ∈ 𝑆 )
80 7 8 9 10 11 12 19 38 79 islssd ⊢ ( 𝜑 → 𝑆 ∈ ( LSubSp ‘ 𝑃 ) )