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 = Poly 1 ⁡ R
ply1degltdim.d ⊢ D = deg 1 ⁡ R
ply1degltdim.s ⊢ S = D -1 −∞ N
ply1degltdim.n ⊢ φ → N ∈ ℕ 0
ply1degltdim.r ⊢ φ → R ∈ DivRing
ply1degltdim.e ⊢ E = P ↾ 𝑠 S
Assertion ply1degltdim ⊢ φ → dim ⁡ E = N

Proof

Step Hyp Ref Expression
1 ply1degltdim.p ⊢ P = Poly 1 ⁡ R
2 ply1degltdim.d ⊢ D = deg 1 ⁡ R
3 ply1degltdim.s ⊢ S = D -1 −∞ N
4 ply1degltdim.n ⊢ φ → N ∈ ℕ 0
5 ply1degltdim.r ⊢ φ → R ∈ DivRing
6 ply1degltdim.e ⊢ E = P ↾ 𝑠 S
7 1 5 ply1lvec ⊢ φ → P ∈ LVec
8 5 drngringd ⊢ φ → R ∈ Ring
9 1 2 3 4 8 ply1degltlss ⊢ φ → S ∈ LSubSp ⁡ P
10 eqid ⊢ LSubSp ⁡ P = LSubSp ⁡ P
11 6 10 lsslvec ⊢ P ∈ LVec ∧ S ∈ LSubSp ⁡ P → E ∈ LVec
12 7 9 11 syl2anc ⊢ φ → E ∈ LVec
13 oveq1 ⊢ k = n → k ⋅ mulGrp P var 1 ⁡ R = n ⋅ mulGrp P var 1 ⁡ R
14 13 cbvmptv ⊢ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R = n ∈ 0 ..^ N ⟼ n ⋅ mulGrp P var 1 ⁡ R
15 1 2 3 4 5 6 14 ply1degltdimlem ⊢ φ → ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R ∈ LBasis ⁡ E
16 eqid ⊢ Base P = Base P
17 2 1 16 deg1xrf ⊢ D : Base P ⟶ ℝ *
18 ffn ⊢ D : Base P ⟶ ℝ * → D Fn Base P
19 17 18 mp1i ⊢ φ ∧ n ∈ 0 ..^ N → D Fn Base P
20 eqid ⊢ mulGrp P = mulGrp P
21 20 16 mgpbas ⊢ Base P = Base mulGrp P
22 eqid ⊢ ⋅ mulGrp P = ⋅ mulGrp P
23 1 ply1ring ⊢ R ∈ Ring → P ∈ Ring
24 20 ringmgp ⊢ P ∈ Ring → mulGrp P ∈ Mnd
25 8 23 24 3syl ⊢ φ → mulGrp P ∈ Mnd
26 25 adantr ⊢ φ ∧ n ∈ 0 ..^ N → mulGrp P ∈ Mnd
27 elfzonn0 ⊢ n ∈ 0 ..^ N → n ∈ ℕ 0
28 27 adantl ⊢ φ ∧ n ∈ 0 ..^ N → n ∈ ℕ 0
29 eqid ⊢ var 1 ⁡ R = var 1 ⁡ R
30 29 1 16 vr1cl ⊢ R ∈ Ring → var 1 ⁡ R ∈ Base P
31 8 30 syl ⊢ φ → var 1 ⁡ R ∈ Base P
32 31 adantr ⊢ φ ∧ n ∈ 0 ..^ N → var 1 ⁡ R ∈ Base P
33 21 22 26 28 32 mulgnn0cld ⊢ φ ∧ n ∈ 0 ..^ N → n ⋅ mulGrp P var 1 ⁡ R ∈ Base P
34 mnfxr ⊢ −∞ ∈ ℝ *
35 34 a1i ⊢ φ ∧ n ∈ 0 ..^ N → −∞ ∈ ℝ *
36 4 nn0red ⊢ φ → N ∈ ℝ
37 36 rexrd ⊢ φ → N ∈ ℝ *
38 37 adantr ⊢ φ ∧ n ∈ 0 ..^ N → N ∈ ℝ *
39 2 1 16 deg1xrcl ⊢ n ⋅ mulGrp P var 1 ⁡ R ∈ Base P → D ⁡ n ⋅ mulGrp P var 1 ⁡ R ∈ ℝ *
40 33 39 syl ⊢ φ ∧ n ∈ 0 ..^ N → D ⁡ n ⋅ mulGrp P var 1 ⁡ R ∈ ℝ *
41 40 mnfled ⊢ φ ∧ n ∈ 0 ..^ N → −∞ ≤ D ⁡ n ⋅ mulGrp P var 1 ⁡ R
42 27 nn0red ⊢ n ∈ 0 ..^ N → n ∈ ℝ
43 42 rexrd ⊢ n ∈ 0 ..^ N → n ∈ ℝ *
44 43 adantl ⊢ φ ∧ n ∈ 0 ..^ N → n ∈ ℝ *
45 2 1 29 20 22 deg1pwle ⊢ R ∈ Ring ∧ n ∈ ℕ 0 → D ⁡ n ⋅ mulGrp P var 1 ⁡ R ≤ n
46 8 27 45 syl2an ⊢ φ ∧ n ∈ 0 ..^ N → D ⁡ n ⋅ mulGrp P var 1 ⁡ R ≤ n
47 elfzolt2 ⊢ n ∈ 0 ..^ N → n < N
48 47 adantl ⊢ φ ∧ n ∈ 0 ..^ N → n < N
49 40 44 38 46 48 xrlelttrd ⊢ φ ∧ n ∈ 0 ..^ N → D ⁡ n ⋅ mulGrp P var 1 ⁡ R < N
50 35 38 40 41 49 elicod ⊢ φ ∧ n ∈ 0 ..^ N → D ⁡ n ⋅ mulGrp P var 1 ⁡ R ∈ −∞ N
51 19 33 50 elpreimad ⊢ φ ∧ n ∈ 0 ..^ N → n ⋅ mulGrp P var 1 ⁡ R ∈ D -1 −∞ N
52 51 3 eleqtrrdi ⊢ φ ∧ n ∈ 0 ..^ N → n ⋅ mulGrp P var 1 ⁡ R ∈ S
53 16 10 lssss ⊢ S ∈ LSubSp ⁡ P → S ⊆ Base P
54 6 16 ressbas2 ⊢ S ⊆ Base P → S = Base E
55 9 53 54 3syl ⊢ φ → S = Base E
56 55 adantr ⊢ φ ∧ n ∈ 0 ..^ N → S = Base E
57 52 56 eleqtrd ⊢ φ ∧ n ∈ 0 ..^ N → n ⋅ mulGrp P var 1 ⁡ R ∈ Base E
58 57 14 fmptd ⊢ φ → k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R : 0 ..^ N ⟶ Base E
59 58 ffnd ⊢ φ → k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R Fn 0 ..^ N
60 hashfn ⊢ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R Fn 0 ..^ N → k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R = 0 ..^ N
61 59 60 syl ⊢ φ → k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R = 0 ..^ N
62 ovexd ⊢ φ → 0 ..^ N ∈ V
63 57 ralrimiva ⊢ φ → ∀ n ∈ 0 ..^ N n ⋅ mulGrp P var 1 ⁡ R ∈ Base E
64 drngnzr ⊢ R ∈ DivRing → R ∈ NzRing
65 5 64 syl ⊢ φ → R ∈ NzRing
66 65 ad2antrr ⊢ φ ∧ n ∈ 0 ..^ N ∧ i ∈ 0 ..^ N → R ∈ NzRing
67 28 adantr ⊢ φ ∧ n ∈ 0 ..^ N ∧ i ∈ 0 ..^ N → n ∈ ℕ 0
68 elfzonn0 ⊢ i ∈ 0 ..^ N → i ∈ ℕ 0
69 68 adantl ⊢ φ ∧ n ∈ 0 ..^ N ∧ i ∈ 0 ..^ N → i ∈ ℕ 0
70 1 29 22 66 67 69 ply1moneq ⊢ φ ∧ n ∈ 0 ..^ N ∧ i ∈ 0 ..^ N → n ⋅ mulGrp P var 1 ⁡ R = i ⋅ mulGrp P var 1 ⁡ R ↔ n = i
71 70 biimpd ⊢ φ ∧ n ∈ 0 ..^ N ∧ i ∈ 0 ..^ N → n ⋅ mulGrp P var 1 ⁡ R = i ⋅ mulGrp P var 1 ⁡ R → n = i
72 71 anasss ⊢ φ ∧ n ∈ 0 ..^ N ∧ i ∈ 0 ..^ N → n ⋅ mulGrp P var 1 ⁡ R = i ⋅ mulGrp P var 1 ⁡ R → n = i
73 72 ralrimivva ⊢ φ → ∀ n ∈ 0 ..^ N ∀ i ∈ 0 ..^ N n ⋅ mulGrp P var 1 ⁡ R = i ⋅ mulGrp P var 1 ⁡ R → n = i
74 oveq1 ⊢ n = i → n ⋅ mulGrp P var 1 ⁡ R = i ⋅ mulGrp P var 1 ⁡ R
75 14 74 f1mpt ⊢ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R : 0 ..^ N ⟶ 1-1 Base E ↔ ∀ n ∈ 0 ..^ N n ⋅ mulGrp P var 1 ⁡ R ∈ Base E ∧ ∀ n ∈ 0 ..^ N ∀ i ∈ 0 ..^ N n ⋅ mulGrp P var 1 ⁡ R = i ⋅ mulGrp P var 1 ⁡ R → n = i
76 63 73 75 sylanbrc ⊢ φ → k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R : 0 ..^ N ⟶ 1-1 Base E
77 hashf1rn ⊢ 0 ..^ N ∈ V ∧ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R : 0 ..^ N ⟶ 1-1 Base E → k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R = ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R
78 62 76 77 syl2anc ⊢ φ → k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R = ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R
79 hashfzo0 ⊢ N ∈ ℕ 0 → 0 ..^ N = N
80 4 79 syl ⊢ φ → 0 ..^ N = N
81 61 78 80 3eqtr3d ⊢ φ → ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R = N
82 hashvnfin ⊢ ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R ∈ LBasis ⁡ E ∧ N ∈ ℕ 0 → ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R = N → ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R ∈ Fin
83 82 imp ⊢ ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R ∈ LBasis ⁡ E ∧ N ∈ ℕ 0 ∧ ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R = N → ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R ∈ Fin
84 15 4 81 83 syl21anc ⊢ φ → ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R ∈ Fin
85 eqid ⊢ LBasis ⁡ E = LBasis ⁡ E
86 85 dimvalfi ⊢ E ∈ LVec ∧ ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R ∈ LBasis ⁡ E ∧ ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R ∈ Fin → dim ⁡ E = ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R
87 12 15 84 86 syl3anc ⊢ φ → dim ⁡ E = ran ⁡ k ∈ 0 ..^ N ⟼ k ⋅ mulGrp P var 1 ⁡ R
88 87 81 eqtrd ⊢ φ → dim ⁡ E = N