Theorem algextdeglem3

Description: Lemma for algextdeg . The quotient P / Z of the vector space P of polynomials by the subspace Z of polynomials annihilating A is itself a vector space. (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	algextdeg.k	$$⊢K=E{\upharpoonright }_{𝑠}F$$
	algextdeg.l	$$⊢L=E{\upharpoonright }_{𝑠}\left(E\mathrm{fldGen}\left(F\cup \left\{A\right\}\right)\right)$$
	algextdeg.d	$$⊢D={\mathrm{deg}}_1\left(E\right)$$
	algextdeg.m	$$⊢M=E\mathrm{minPoly}F$$
	algextdeg.f	$$⊢\phi \to E\in \mathrm{Field}$$
	algextdeg.e	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
	algextdeg.a	$$⊢\phi \to A\in \left(E\mathrm{IntgRing}F\right)$$
	algextdeglem.o	$$⊢O=E{\mathrm{evalSub}}_{1}F$$
	algextdeglem.y	$$⊢P={\mathrm{Poly}}_1\left(K\right)$$
	algextdeglem.u	$$⊢U={\mathrm{Base}}_P$$
	algextdeglem.g	$$⊢G=\left(p\in U⟼O\left(p\right)\left(A\right)\right)$$
	algextdeglem.n	$$⊢N=\left(x\in U⟼\left[x\right]\left(P{~}_{\mathit{QG}}Z\right)\right)$$
	algextdeglem.z	$$⊢Z=G^{-1}\left[\left\{0_L\right\}\right]$$
	algextdeglem.q	$$⊢Q=P{/}_{𝑠}\left(P{~}_{\mathit{QG}}Z\right)$$
	algextdeglem.j	$$⊢J=\left(p\in {\mathrm{Base}}_Q⟼\bigcup G\left[p\right]\right)$$
Assertion	algextdeglem3	$$⊢\phi \to Q\in \mathrm{LVec}$$

Proof

Step	Hyp	Ref	Expression
1		algextdeg.k	$$⊢K=E{\upharpoonright }_{𝑠}F$$
2		algextdeg.l	$$⊢L=E{\upharpoonright }_{𝑠}\left(E\mathrm{fldGen}\left(F\cup \left\{A\right\}\right)\right)$$
3		algextdeg.d	$$⊢D={\mathrm{deg}}_1\left(E\right)$$
4		algextdeg.m	$$⊢M=E\mathrm{minPoly}F$$
5		algextdeg.f	$$⊢\phi \to E\in \mathrm{Field}$$
6		algextdeg.e	$$⊢\phi \to F\in \mathrm{SubDRing}\left(E\right)$$
7		algextdeg.a	$$⊢\phi \to A\in \left(E\mathrm{IntgRing}F\right)$$
8		algextdeglem.o	$$⊢O=E{\mathrm{evalSub}}_{1}F$$
9		algextdeglem.y	$$⊢P={\mathrm{Poly}}_1\left(K\right)$$
10		algextdeglem.u	$$⊢U={\mathrm{Base}}_P$$
11		algextdeglem.g	$$⊢G=\left(p\in U⟼O\left(p\right)\left(A\right)\right)$$
12		algextdeglem.n	$$⊢N=\left(x\in U⟼\left[x\right]\left(P{~}_{\mathit{QG}}Z\right)\right)$$
13		algextdeglem.z	$$⊢Z=G^{-1}\left[\left\{0_L\right\}\right]$$
14		algextdeglem.q	$$⊢Q=P{/}_{𝑠}\left(P{~}_{\mathit{QG}}Z\right)$$
15		algextdeglem.j	$$⊢J=\left(p\in {\mathrm{Base}}_Q⟼\bigcup G\left[p\right]\right)$$
16	1	fveq2i	$$⊢{\mathrm{Poly}}_1\left(K\right)={\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
17	9 16	eqtri	$$⊢P={\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
18		issdrg	$$⊢F\in \mathrm{SubDRing}\left(E\right)\leftrightarrow \left(E\in \mathrm{DivRing}\wedge F\in \mathrm{SubRing}\left(E\right)\wedge E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}\right)$$
19	6 18	sylib	$$⊢\phi \to \left(E\in \mathrm{DivRing}\wedge F\in \mathrm{SubRing}\left(E\right)\wedge E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}\right)$$
20	19	simp3d	$$⊢\phi \to E{\upharpoonright }_{𝑠}F\in \mathrm{DivRing}$$
21	17 20	ply1lvec	$$⊢\phi \to P\in \mathrm{LVec}$$
22		eqidd	$$⊢\phi \to \mathrm{subringAlg}\left(L\right)\left(F\right)=\mathrm{subringAlg}\left(L\right)\left(F\right)$$
23		eqidd	$$⊢\phi \to 0_L=0_L$$
24		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
25	5	flddrngd	$$⊢\phi \to E\in \mathrm{DivRing}$$
26	19	simp2d	$$⊢\phi \to F\in \mathrm{SubRing}\left(E\right)$$
27		subrgsubg	$$⊢F\in \mathrm{SubRing}\left(E\right)\to F\in \mathrm{SubGrp}\left(E\right)$$
28	24	subgss	$$⊢F\in \mathrm{SubGrp}\left(E\right)\to F\subseteq {\mathrm{Base}}_E$$
29	26 27 28	3syl	$$⊢\phi \to F\subseteq {\mathrm{Base}}_E$$
30		eqid	$$⊢0_E=0_E$$
31	5	fldcrngd	$$⊢\phi \to E\in \mathrm{CRing}$$
32	8 1 24 30 31 26	irngssv	$$⊢\phi \to E\mathrm{IntgRing}F\subseteq {\mathrm{Base}}_E$$
33	32 7	sseldd	$$⊢\phi \to A\in {\mathrm{Base}}_E$$
34	33	snssd	$$⊢\phi \to \left\{A\right\}\subseteq {\mathrm{Base}}_E$$
35	29 34	unssd	$$⊢\phi \to F\cup \left\{A\right\}\subseteq {\mathrm{Base}}_E$$
36	24 25 35	fldgenssid	$$⊢\phi \to F\cup \left\{A\right\}\subseteq E\mathrm{fldGen}\left(F\cup \left\{A\right\}\right)$$
37	36	unssad	$$⊢\phi \to F\subseteq E\mathrm{fldGen}\left(F\cup \left\{A\right\}\right)$$
38	24 25 35	fldgenssv	$$⊢\phi \to E\mathrm{fldGen}\left(F\cup \left\{A\right\}\right)\subseteq {\mathrm{Base}}_E$$
39	2 24	ressbas2	$$⊢E\mathrm{fldGen}\left(F\cup \left\{A\right\}\right)\subseteq {\mathrm{Base}}_E\to E\mathrm{fldGen}\left(F\cup \left\{A\right\}\right)={\mathrm{Base}}_L$$
40	38 39	syl	$$⊢\phi \to E\mathrm{fldGen}\left(F\cup \left\{A\right\}\right)={\mathrm{Base}}_L$$
41	37 40	sseqtrd	$$⊢\phi \to F\subseteq {\mathrm{Base}}_L$$
42	22 23 41	sralmod0	$$⊢\phi \to 0_L=0_{\mathrm{subringAlg}\left(L\right)\left(F\right)}$$
43	42	sneqd	$$⊢\phi \to \left\{0_L\right\}=\left\{0_{\mathrm{subringAlg}\left(L\right)\left(F\right)}\right\}$$
44	43	imaeq2d	$$⊢\phi \to G^{-1}\left[\left\{0_L\right\}\right]=G^{-1}\left[\left\{0_{\mathrm{subringAlg}\left(L\right)\left(F\right)}\right\}\right]$$
45	13 44	eqtrid	$$⊢\phi \to Z=G^{-1}\left[\left\{0_{\mathrm{subringAlg}\left(L\right)\left(F\right)}\right\}\right]$$
46	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	algextdeglem2	$$⊢\phi \to G\in \left(P\mathrm{LMHom}\mathrm{subringAlg}\left(L\right)\left(F\right)\right)$$
47		eqid	$$⊢G^{-1}\left[\left\{0_{\mathrm{subringAlg}\left(L\right)\left(F\right)}\right\}\right]=G^{-1}\left[\left\{0_{\mathrm{subringAlg}\left(L\right)\left(F\right)}\right\}\right]$$
48		eqid	$$⊢0_{\mathrm{subringAlg}\left(L\right)\left(F\right)}=0_{\mathrm{subringAlg}\left(L\right)\left(F\right)}$$
49		eqid	$$⊢\mathrm{LSubSp}\left(P\right)=\mathrm{LSubSp}\left(P\right)$$
50	47 48 49	lmhmkerlss	$$⊢G\in \left(P\mathrm{LMHom}\mathrm{subringAlg}\left(L\right)\left(F\right)\right)\to G^{-1}\left[\left\{0_{\mathrm{subringAlg}\left(L\right)\left(F\right)}\right\}\right]\in \mathrm{LSubSp}\left(P\right)$$
51	46 50	syl	$$⊢\phi \to G^{-1}\left[\left\{0_{\mathrm{subringAlg}\left(L\right)\left(F\right)}\right\}\right]\in \mathrm{LSubSp}\left(P\right)$$
52	45 51	eqeltrd	$$⊢\phi \to Z\in \mathrm{LSubSp}\left(P\right)$$
53	14 21 52	quslvec	$$⊢\phi \to Q\in \mathrm{LVec}$$