Theorem algextdeglem7

Description: Lemma for algextdeg . (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	algextdeg.k	$$⊢K=E{\upharpoonright }_{𝑠}F$$
	algextdeg.l	No typesetting found for |- L = ( E |`s ( E fldGen ( F u. { A } ) ) ) with typecode |-
	algextdeg.d	$$⊢D={\mathrm{deg}}_1\left(E\right)$$
	algextdeg.m	No typesetting found for |- M = ( E minPoly F ) with typecode |-
	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)$$
	algextdeglem.r	$$⊢R={rem}_{\mathrm{1p}}\left(K\right)$$
	algextdeglem.h	$$⊢H=\left(p\in U⟼pRM\left(A\right)\right)$$
	algextdeglem.t	$$⊢T={{\mathrm{deg}}_1\left(K\right)}^{-1}\left[\left[\mathrm{-\infty },D\left(M\left(A\right)\right)\right)\right]$$
	algextdeglem.x	$$⊢\phi \to X\in U$$
Assertion	algextdeglem7	$$⊢\phi \to \left(X\in T\leftrightarrow H\left(X\right)=X\right)$$

Proof

Step	Hyp	Ref	Expression
1		algextdeg.k	$$⊢K=E{\upharpoonright }_{𝑠}F$$
2		algextdeg.l	Could not format L = ( E |`s ( E fldGen ( F u. { A } ) ) ) : No typesetting found for |- L = ( E |`s ( E fldGen ( F u. { A } ) ) ) with typecode |-
3		algextdeg.d	$$⊢D={\mathrm{deg}}_1\left(E\right)$$
4		algextdeg.m	Could not format M = ( E minPoly F ) : No typesetting found for |- M = ( E minPoly F ) with typecode |-
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		algextdeglem.r	$$⊢R={rem}_{\mathrm{1p}}\left(K\right)$$
17		algextdeglem.h	$$⊢H=\left(p\in U⟼pRM\left(A\right)\right)$$
18		algextdeglem.t	$$⊢T={{\mathrm{deg}}_1\left(K\right)}^{-1}\left[\left[\mathrm{-\infty },D\left(M\left(A\right)\right)\right)\right]$$
19		algextdeglem.x	$$⊢\phi \to X\in U$$
20	1	fveq2i	$$⊢{\mathrm{Poly}}_1\left(K\right)={\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
21	9 20	eqtri	$$⊢P={\mathrm{Poly}}_1\left(E{\upharpoonright }_{𝑠}F\right)$$
22		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
23		eqid	$$⊢0_E=0_E$$
24	5	fldcrngd	$$⊢\phi \to E\in \mathrm{CRing}$$
25		sdrgsubrg	$$⊢F\in \mathrm{SubDRing}\left(E\right)\to F\in \mathrm{SubRing}\left(E\right)$$
26	6 25	syl	$$⊢\phi \to F\in \mathrm{SubRing}\left(E\right)$$
27	8 1 22 23 24 26	irngssv	$$⊢\phi \to E\mathrm{IntgRing}F\subseteq {\mathrm{Base}}_E$$
28	27 7	sseldd	$$⊢\phi \to A\in {\mathrm{Base}}_E$$
29		eqid	$$⊢\left\{p\in \mathrm{dom}O|O\left(p\right)\left(A\right)=0_E\right\}=\left\{p\in \mathrm{dom}O|O\left(p\right)\left(A\right)=0_E\right\}$$
30		eqid	$$⊢\mathrm{RSpan}\left(P\right)=\mathrm{RSpan}\left(P\right)$$
31		eqid	$$⊢{idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)={idlGen}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
32	8 21 22 5 6 28 23 29 30 31 4	minplycl	$$⊢\phi \to M\left(A\right)\in {\mathrm{Base}}_P$$
33	32 10	eleqtrrdi	$$⊢\phi \to M\left(A\right)\in U$$
34	1 3 9 10 33 26	ressdeg1	$$⊢\phi \to D\left(M\left(A\right)\right)={\mathrm{deg}}_1\left(K\right)\left(M\left(A\right)\right)$$
35	34	breq2d	$$⊢\phi \to \left({\mathrm{deg}}_1\left(K\right)\left(X\right)<D\left(M\left(A\right)\right)\leftrightarrow {\mathrm{deg}}_1\left(K\right)\left(X\right)<{\mathrm{deg}}_1\left(K\right)\left(M\left(A\right)\right)\right)$$
36		eqid	$$⊢{\mathrm{deg}}_1\left(K\right)={\mathrm{deg}}_1\left(K\right)$$
37	5	flddrngd	$$⊢\phi \to E\in \mathrm{DivRing}$$
38	37	drngringd	$$⊢\phi \to E\in \mathrm{Ring}$$
39		eqid	$$⊢{\mathrm{Poly}}_1\left(E\right)={\mathrm{Poly}}_1\left(E\right)$$
40		eqid	$$⊢{\mathrm{PwSer}}_1\left(K\right)={\mathrm{PwSer}}_1\left(K\right)$$
41		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(K\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(K\right)}$$
42		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E\right)}$$
43	39 1 9 10 26 40 41 42	ressply1bas2	$$⊢\phi \to U={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(K\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E\right)}$$
44		inss2	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(K\right)}\cap {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E\right)}\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E\right)}$$
45	43 44	eqsstrdi	$$⊢\phi \to U\subseteq {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E\right)}$$
46	45 33	sseldd	$$⊢\phi \to M\left(A\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E\right)}$$
47		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(E\right)}=0_{{\mathrm{Poly}}_1\left(E\right)}$$
48	47 5 6 4 7	irngnminplynz	$$⊢\phi \to M\left(A\right)\ne 0_{{\mathrm{Poly}}_1\left(E\right)}$$
49	3 39 47 42	deg1nn0cl	$$⊢\left(E\in \mathrm{Ring}\wedge M\left(A\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(E\right)}\wedge M\left(A\right)\ne 0_{{\mathrm{Poly}}_1\left(E\right)}\right)\to D\left(M\left(A\right)\right)\in {\mathbb{N}}_0$$
50	38 46 48 49	syl3anc	$$⊢\phi \to D\left(M\left(A\right)\right)\in {\mathbb{N}}_0$$
51		fldsdrgfld	$$⊢\left(E\in \mathrm{Field}\wedge F\in \mathrm{SubDRing}\left(E\right)\right)\to E{\upharpoonright }_{𝑠}F\in \mathrm{Field}$$
52	5 6 51	syl2anc	$$⊢\phi \to E{\upharpoonright }_{𝑠}F\in \mathrm{Field}$$
53	1 52	eqeltrid	$$⊢\phi \to K\in \mathrm{Field}$$
54		fldidom	$$⊢K\in \mathrm{Field}\to K\in \mathrm{IDomn}$$
55	53 54	syl	$$⊢\phi \to K\in \mathrm{IDomn}$$
56	55	idomringd	$$⊢\phi \to K\in \mathrm{Ring}$$
57	9 36 18 50 56 10	ply1degleel	$$⊢\phi \to \left(X\in T\leftrightarrow \left(X\in U\wedge {\mathrm{deg}}_1\left(K\right)\left(X\right)<D\left(M\left(A\right)\right)\right)\right)$$
58	19 57	mpbirand	$$⊢\phi \to \left(X\in T\leftrightarrow {\mathrm{deg}}_1\left(K\right)\left(X\right)<D\left(M\left(A\right)\right)\right)$$
59		eqid	$$⊢{Unic}_{\mathrm{1p}}\left(K\right)={Unic}_{\mathrm{1p}}\left(K\right)$$
60	1	fveq2i	$$⊢{Monic}_{\mathrm{1p}}\left(K\right)={Monic}_{\mathrm{1p}}\left(E{\upharpoonright }_{𝑠}F\right)$$
61	47 5 6 4 7 60	minplym1p	$$⊢\phi \to M\left(A\right)\in {Monic}_{\mathrm{1p}}\left(K\right)$$
62		eqid	$$⊢{Monic}_{\mathrm{1p}}\left(K\right)={Monic}_{\mathrm{1p}}\left(K\right)$$
63	59 62	mon1puc1p	$$⊢\left(K\in \mathrm{Ring}\wedge M\left(A\right)\in {Monic}_{\mathrm{1p}}\left(K\right)\right)\to M\left(A\right)\in {Unic}_{\mathrm{1p}}\left(K\right)$$
64	56 61 63	syl2anc	$$⊢\phi \to M\left(A\right)\in {Unic}_{\mathrm{1p}}\left(K\right)$$
65	9 10 59 16 55 36 19 64	r1pid2	$$⊢\phi \to \left(XRM\left(A\right)=X\leftrightarrow {\mathrm{deg}}_1\left(K\right)\left(X\right)<{\mathrm{deg}}_1\left(K\right)\left(M\left(A\right)\right)\right)$$
66	35 58 65	3bitr4d	$$⊢\phi \to \left(X\in T\leftrightarrow XRM\left(A\right)=X\right)$$
67		oveq1	$$⊢p=X\to pRM\left(A\right)=XRM\left(A\right)$$
68		ovexd	$$⊢\phi \to XRM\left(A\right)\in \mathrm{V}$$
69	17 67 19 68	fvmptd3	$$⊢\phi \to H\left(X\right)=XRM\left(A\right)$$
70	69	eqeq1d	$$⊢\phi \to \left(H\left(X\right)=X\leftrightarrow XRM\left(A\right)=X\right)$$
71	66 70	bitr4d	$$⊢\phi \to \left(X\in T\leftrightarrow H\left(X\right)=X\right)$$