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

Metamath Proof Explorer

Theorem ply1degltdim

Proof