Theorem algextdeg

Description: The degree of an algebraic field extension (noted [ L : K ] ) is the degree of the minimal polynomial M ( A ) , whereas L is the field generated by K and the algebraic element A . (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)$$
Assertion	algextdeg	$$⊢\phi \to L\left[.:.\right]K=D\left(M\left(A\right)\right)$$

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		eqid	$$⊢E{\mathrm{evalSub}}_{1}F=E{\mathrm{evalSub}}_{1}F$$
9		eqid	$$⊢{\mathrm{Poly}}_1\left(K\right)={\mathrm{Poly}}_1\left(K\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}$$
11		fveq2	$$⊢q=p\to \left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)=\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)$$
12	11	fveq1d	$$⊢q=p\to \left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)=\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(A\right)$$
13	12	cbvmptv	$$⊢\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)=\left(p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(p\right)\left(A\right)\right)$$
14		eceq1	$$⊢y=x\to \left[y\right]\left({\mathrm{Poly}}_1\left(K\right){~}_{\mathit{QG}}{\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)}^{-1}\left[\left\{0_L\right\}\right]\right)=\left[x\right]\left({\mathrm{Poly}}_1\left(K\right){~}_{\mathit{QG}}{\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)}^{-1}\left[\left\{0_L\right\}\right]\right)$$
15	14	cbvmptv	$$⊢\left(y\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left[y\right]\left({\mathrm{Poly}}_1\left(K\right){~}_{\mathit{QG}}{\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)}^{-1}\left[\left\{0_L\right\}\right]\right)\right)=\left(x\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left[x\right]\left({\mathrm{Poly}}_1\left(K\right){~}_{\mathit{QG}}{\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)}^{-1}\left[\left\{0_L\right\}\right]\right)\right)$$
16		eqid	$$⊢{\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)}^{-1}\left[\left\{0_L\right\}\right]={\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)}^{-1}\left[\left\{0_L\right\}\right]$$
17		eqid	$$⊢{\mathrm{Poly}}_1\left(K\right){/}_{𝑠}\left({\mathrm{Poly}}_1\left(K\right){~}_{\mathit{QG}}{\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)}^{-1}\left[\left\{0_L\right\}\right]\right)={\mathrm{Poly}}_1\left(K\right){/}_{𝑠}\left({\mathrm{Poly}}_1\left(K\right){~}_{\mathit{QG}}{\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)}^{-1}\left[\left\{0_L\right\}\right]\right)$$
18		imaeq2	$$⊢r=p\to \left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)\left[r\right]=\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)\left[p\right]$$
19	18	unieqd	$$⊢r=p\to \bigcup \left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)\left[r\right]=\bigcup \left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)\left[p\right]$$
20	19	cbvmptv	$$⊢\left(r\in {\mathrm{Base}}_{\left({\mathrm{Poly}}_1\left(K\right){/}_{𝑠}\left({\mathrm{Poly}}_1\left(K\right){~}_{\mathit{QG}}{\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)}^{-1}\left[\left\{0_L\right\}\right]\right)\right)}⟼\bigcup \left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)\left[r\right]\right)=\left(p\in {\mathrm{Base}}_{\left({\mathrm{Poly}}_1\left(K\right){/}_{𝑠}\left({\mathrm{Poly}}_1\left(K\right){~}_{\mathit{QG}}{\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)}^{-1}\left[\left\{0_L\right\}\right]\right)\right)}⟼\bigcup \left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)\left[p\right]\right)$$
21		eqid	$$⊢{rem}_{\mathrm{1p}}\left(K\right)={rem}_{\mathrm{1p}}\left(K\right)$$
22		oveq1	$$⊢q=p\to q{rem}_{\mathrm{1p}}\left(K\right)M\left(A\right)=p{rem}_{\mathrm{1p}}\left(K\right)M\left(A\right)$$
23	22	cbvmptv	$$⊢\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼q{rem}_{\mathrm{1p}}\left(K\right)M\left(A\right)\right)=\left(p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼p{rem}_{\mathrm{1p}}\left(K\right)M\left(A\right)\right)$$
24	1 2 3 4 5 6 7 8 9 10 13 15 16 17 20 21 23	algextdeglem6	$$⊢\phi \to \dim \left({\mathrm{Poly}}_1\left(K\right){/}_{𝑠}\left({\mathrm{Poly}}_1\left(K\right){~}_{\mathit{QG}}{\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)}^{-1}\left[\left\{0_L\right\}\right]\right)\right)=\dim \left(\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼q{rem}_{\mathrm{1p}}\left(K\right)M\left(A\right)\right){“}_{𝑠}{\mathrm{Poly}}_1\left(K\right)\right)$$
25	1 2 3 4 5 6 7 8 9 10 13 15 16 17 20	algextdeglem4	$$⊢\phi \to \dim \left({\mathrm{Poly}}_1\left(K\right){/}_{𝑠}\left({\mathrm{Poly}}_1\left(K\right){~}_{\mathit{QG}}{\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼\left(E{\mathrm{evalSub}}_{1}F\right)\left(q\right)\left(A\right)\right)}^{-1}\left[\left\{0_L\right\}\right]\right)\right)=L\left[.:.\right]K$$
26		eqid	$$⊢{{\mathrm{deg}}_1\left(K\right)}^{-1}\left[\left[\mathrm{-\infty },D\left(M\left(A\right)\right)\right)\right]={{\mathrm{deg}}_1\left(K\right)}^{-1}\left[\left[\mathrm{-\infty },D\left(M\left(A\right)\right)\right)\right]$$
27	1 2 3 4 5 6 7 8 9 10 13 15 16 17 20 21 23 26	algextdeglem8	$$⊢\phi \to \dim \left(\left(q\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(K\right)}⟼q{rem}_{\mathrm{1p}}\left(K\right)M\left(A\right)\right){“}_{𝑠}{\mathrm{Poly}}_1\left(K\right)\right)=D\left(M\left(A\right)\right)$$
28	24 25 27	3eqtr3d	$$⊢\phi \to L\left[.:.\right]K=D\left(M\left(A\right)\right)$$