Theorem algextdeglem7

Description: Lemma for algextdeg . The polynomials X of lower degree than the minimal polynomial are left unchanged when taking the remainder of the division by that minimal polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	algextdeg.k	⊢ 𝐾 = ( 𝐸 ↾s 𝐹 )
	algextdeg.l	⊢ 𝐿 = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
	algextdeg.d	⊢ 𝐷 = ( deg1 ‘ 𝐸 )
	algextdeg.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
	algextdeg.f	⊢ ( 𝜑 → 𝐸 ∈ Field )
	algextdeg.e	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	algextdeg.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐸 IntgRing 𝐹 ) )
	algextdeglem.o	⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
	algextdeglem.y	⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
	algextdeglem.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	algextdeglem.g	⊢ 𝐺 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
	algextdeglem.n	⊢ 𝑁 = ( 𝑥 ∈ 𝑈 ↦ [ 𝑥 ] ( 𝑃 ~QG 𝑍 ) )
	algextdeglem.z	⊢ 𝑍 = ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } )
	algextdeglem.q	⊢ 𝑄 = ( 𝑃 /s ( 𝑃 ~QG 𝑍 ) )
	algextdeglem.j	⊢ 𝐽 = ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐺 “ 𝑝 ) )
	algextdeglem.r	⊢ 𝑅 = ( rem1p ‘ 𝐾 )
	algextdeglem.h	⊢ 𝐻 = ( 𝑝 ∈ 𝑈 ↦ ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) )
	algextdeglem.t	⊢ 𝑇 = ( ◡ ( deg1 ‘ 𝐾 ) “ ( -∞ [,) ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
	algextdeglem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
Assertion	algextdeglem7	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑇 ↔ ( 𝐻 ‘ 𝑋 ) = 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		algextdeg.k	⊢ 𝐾 = ( 𝐸 ↾s 𝐹 )
2		algextdeg.l	⊢ 𝐿 = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
3		algextdeg.d	⊢ 𝐷 = ( deg1 ‘ 𝐸 )
4		algextdeg.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
5		algextdeg.f	⊢ ( 𝜑 → 𝐸 ∈ Field )
6		algextdeg.e	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
7		algextdeg.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐸 IntgRing 𝐹 ) )
8		algextdeglem.o	⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
9		algextdeglem.y	⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
10		algextdeglem.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
11		algextdeglem.g	⊢ 𝐺 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
12		algextdeglem.n	⊢ 𝑁 = ( 𝑥 ∈ 𝑈 ↦ [ 𝑥 ] ( 𝑃 ~QG 𝑍 ) )
13		algextdeglem.z	⊢ 𝑍 = ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } )
14		algextdeglem.q	⊢ 𝑄 = ( 𝑃 /s ( 𝑃 ~QG 𝑍 ) )
15		algextdeglem.j	⊢ 𝐽 = ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐺 “ 𝑝 ) )
16		algextdeglem.r	⊢ 𝑅 = ( rem1p ‘ 𝐾 )
17		algextdeglem.h	⊢ 𝐻 = ( 𝑝 ∈ 𝑈 ↦ ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) )
18		algextdeglem.t	⊢ 𝑇 = ( ◡ ( deg1 ‘ 𝐾 ) “ ( -∞ [,) ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
19		algextdeglem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
20	1	fveq2i	⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
21	9 20	eqtri	⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
22		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
23		eqid	⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
24	5	fldcrngd	⊢ ( 𝜑 → 𝐸 ∈ CRing )
25		sdrgsubrg	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
26	6 25	syl	⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
27	8 1 22 23 24 26	irngssv	⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
28	27 7	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐸 ) )
29		eqid	⊢ { 𝑝 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } = { 𝑝 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) }
30		eqid	⊢ ( RSpan ‘ 𝑃 ) = ( RSpan ‘ 𝑃 )
31		eqid	⊢ ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
32	8 21 22 5 6 28 23 29 30 31 4	minplycl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ 𝑃 ) )
33	32 10	eleqtrrdi	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑈 )
34	1 3 9 10 33 26	ressdeg1	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝐴 ) ) )
35	34	breq2d	⊢ ( 𝜑 → ( ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) < ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ↔ ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) < ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
36		eqid	⊢ ( deg1 ‘ 𝐾 ) = ( deg1 ‘ 𝐾 )
37	5	flddrngd	⊢ ( 𝜑 → 𝐸 ∈ DivRing )
38	37	drngringd	⊢ ( 𝜑 → 𝐸 ∈ Ring )
39		eqid	⊢ ( Poly1 ‘ 𝐸 ) = ( Poly1 ‘ 𝐸 )
40		eqid	⊢ ( PwSer1 ‘ 𝐾 ) = ( PwSer1 ‘ 𝐾 )
41		eqid	⊢ ( Base ‘ ( PwSer1 ‘ 𝐾 ) ) = ( Base ‘ ( PwSer1 ‘ 𝐾 ) )
42		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) = ( Base ‘ ( Poly1 ‘ 𝐸 ) )
43	39 1 9 10 26 40 41 42	ressply1bas2	⊢ ( 𝜑 → 𝑈 = ( ( Base ‘ ( PwSer1 ‘ 𝐾 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) ) )
44		inss2	⊢ ( ( Base ‘ ( PwSer1 ‘ 𝐾 ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) ) ⊆ ( Base ‘ ( Poly1 ‘ 𝐸 ) )
45	43 44	eqsstrdi	⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) )
46	45 33	sseldd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) )
47		eqid	⊢ ( 0g ‘ ( Poly1 ‘ 𝐸 ) ) = ( 0g ‘ ( Poly1 ‘ 𝐸 ) )
48	47 5 6 4 7	irngnminplynz	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐸 ) ) )
49	3 39 47 42	deg1nn0cl	⊢ ( ( 𝐸 ∈ Ring ∧ ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐸 ) ) ∧ ( 𝑀 ‘ 𝐴 ) ≠ ( 0g ‘ ( Poly1 ‘ 𝐸 ) ) ) → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ∈ ℕ0 )
50	38 46 48 49	syl3anc	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ∈ ℕ0 )
51		fldsdrgfld	⊢ ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ) → ( 𝐸 ↾s 𝐹 ) ∈ Field )
52	5 6 51	syl2anc	⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ Field )
53	1 52	eqeltrid	⊢ ( 𝜑 → 𝐾 ∈ Field )
54		fldidom	⊢ ( 𝐾 ∈ Field → 𝐾 ∈ IDomn )
55	53 54	syl	⊢ ( 𝜑 → 𝐾 ∈ IDomn )
56	55	idomringd	⊢ ( 𝜑 → 𝐾 ∈ Ring )
57	9 36 18 50 56 10	ply1degleel	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑇 ↔ ( 𝑋 ∈ 𝑈 ∧ ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) < ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ) ) )
58	19 57	mpbirand	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑇 ↔ ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) < ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
59		eqid	⊢ ( Unic1p ‘ 𝐾 ) = ( Unic1p ‘ 𝐾 )
60	55	idomdomd	⊢ ( 𝜑 → 𝐾 ∈ Domn )
61	1	fveq2i	⊢ ( Monic1p ‘ 𝐾 ) = ( Monic1p ‘ ( 𝐸 ↾s 𝐹 ) )
62	47 5 6 4 7 61	minplym1p	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Monic1p ‘ 𝐾 ) )
63		eqid	⊢ ( Monic1p ‘ 𝐾 ) = ( Monic1p ‘ 𝐾 )
64	59 63	mon1puc1p	⊢ ( ( 𝐾 ∈ Ring ∧ ( 𝑀 ‘ 𝐴 ) ∈ ( Monic1p ‘ 𝐾 ) ) → ( 𝑀 ‘ 𝐴 ) ∈ ( Unic1p ‘ 𝐾 ) )
65	56 62 64	syl2anc	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Unic1p ‘ 𝐾 ) )
66	9 10 59 16 36 60 19 65	r1pid2	⊢ ( 𝜑 → ( ( 𝑋 𝑅 ( 𝑀 ‘ 𝐴 ) ) = 𝑋 ↔ ( ( deg1 ‘ 𝐾 ) ‘ 𝑋 ) < ( ( deg1 ‘ 𝐾 ) ‘ ( 𝑀 ‘ 𝐴 ) ) ) )
67	35 58 66	3bitr4d	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑇 ↔ ( 𝑋 𝑅 ( 𝑀 ‘ 𝐴 ) ) = 𝑋 ) )
68		oveq1	⊢ ( 𝑝 = 𝑋 → ( 𝑝 𝑅 ( 𝑀 ‘ 𝐴 ) ) = ( 𝑋 𝑅 ( 𝑀 ‘ 𝐴 ) ) )
69		ovexd	⊢ ( 𝜑 → ( 𝑋 𝑅 ( 𝑀 ‘ 𝐴 ) ) ∈ V )
70	17 68 19 69	fvmptd3	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑋 ) = ( 𝑋 𝑅 ( 𝑀 ‘ 𝐴 ) ) )
71	70	eqeq1d	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑋 ) = 𝑋 ↔ ( 𝑋 𝑅 ( 𝑀 ‘ 𝐴 ) ) = 𝑋 ) )
72	67 71	bitr4d	⊢ ( 𝜑 → ( 𝑋 ∈ 𝑇 ↔ ( 𝐻 ‘ 𝑋 ) = 𝑋 ) )