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	\|- K = ( E \|`s F )
	algextdeg.l	\|- L = ( E \|`s ( E fldGen ( F u. { A } ) ) )
	algextdeg.d	\|- D = ( deg1 ` E )
	algextdeg.m	\|- M = ( E minPoly F )
	algextdeg.f	\|- ( ph -> E e. Field )
	algextdeg.e	\|- ( ph -> F e. ( SubDRing ` E ) )
	algextdeg.a	\|- ( ph -> A e. ( E IntgRing F ) )
	algextdeglem.o	\|- O = ( E evalSub1 F )
	algextdeglem.y	\|- P = ( Poly1 ` K )
	algextdeglem.u	\|- U = ( Base ` P )
	algextdeglem.g	\|- G = ( p e. U \|-> ( ( O ` p ) ` A ) )
	algextdeglem.n	\|- N = ( x e. U \|-> [ x ] ( P ~QG Z ) )
	algextdeglem.z	\|- Z = ( `' G " { ( 0g ` L ) } )
	algextdeglem.q	\|- Q = ( P /s ( P ~QG Z ) )
	algextdeglem.j	\|- J = ( p e. ( Base ` Q ) \|-> U. ( G " p ) )
	algextdeglem.r	\|- R = ( rem1p ` K )
	algextdeglem.h	\|- H = ( p e. U \|-> ( p R ( M ` A ) ) )
	algextdeglem.t	\|- T = ( `' ( deg1 ` K ) " ( -oo [,) ( D ` ( M ` A ) ) ) )
	algextdeglem.x	\|- ( ph -> X e. U )
Assertion	algextdeglem7	\|- ( ph -> ( X e. T <-> ( H ` X ) = X ) )

Proof

Step	Hyp	Ref	Expression
1		algextdeg.k	\|- K = ( E \|`s F )
2		algextdeg.l	\|- L = ( E \|`s ( E fldGen ( F u. { A } ) ) )
3		algextdeg.d	\|- D = ( deg1 ` E )
4		algextdeg.m	\|- M = ( E minPoly F )
5		algextdeg.f	\|- ( ph -> E e. Field )
6		algextdeg.e	\|- ( ph -> F e. ( SubDRing ` E ) )
7		algextdeg.a	\|- ( ph -> A e. ( E IntgRing F ) )
8		algextdeglem.o	\|- O = ( E evalSub1 F )
9		algextdeglem.y	\|- P = ( Poly1 ` K )
10		algextdeglem.u	\|- U = ( Base ` P )
11		algextdeglem.g	\|- G = ( p e. U \|-> ( ( O ` p ) ` A ) )
12		algextdeglem.n	\|- N = ( x e. U \|-> [ x ] ( P ~QG Z ) )
13		algextdeglem.z	\|- Z = ( `' G " { ( 0g ` L ) } )
14		algextdeglem.q	\|- Q = ( P /s ( P ~QG Z ) )
15		algextdeglem.j	\|- J = ( p e. ( Base ` Q ) \|-> U. ( G " p ) )
16		algextdeglem.r	\|- R = ( rem1p ` K )
17		algextdeglem.h	\|- H = ( p e. U \|-> ( p R ( M ` A ) ) )
18		algextdeglem.t	\|- T = ( `' ( deg1 ` K ) " ( -oo [,) ( D ` ( M ` A ) ) ) )
19		algextdeglem.x	\|- ( ph -> X e. U )
20	1	fveq2i	\|- ( Poly1 ` K ) = ( Poly1 ` ( E \|`s F ) )
21	9 20	eqtri	\|- P = ( Poly1 ` ( E \|`s F ) )
22		eqid	\|- ( Base ` E ) = ( Base ` E )
23		eqid	\|- ( 0g ` E ) = ( 0g ` E )
24	5	fldcrngd	\|- ( ph -> E e. CRing )
25		sdrgsubrg	\|- ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
26	6 25	syl	\|- ( ph -> F e. ( SubRing ` E ) )
27	8 1 22 23 24 26	irngssv	\|- ( ph -> ( E IntgRing F ) C_ ( Base ` E ) )
28	27 7	sseldd	\|- ( ph -> A e. ( Base ` E ) )
29		eqid	\|- { p e. dom O \| ( ( O ` p ) ` A ) = ( 0g ` E ) } = { p e. dom O \| ( ( O ` p ) ` A ) = ( 0g ` E ) }
30		eqid	\|- ( RSpan ` P ) = ( RSpan ` P )
31		eqid	\|- ( idlGen1p ` ( E \|`s F ) ) = ( idlGen1p ` ( E \|`s F ) )
32	8 21 22 5 6 28 23 29 30 31 4	minplycl	\|- ( ph -> ( M ` A ) e. ( Base ` P ) )
33	32 10	eleqtrrdi	\|- ( ph -> ( M ` A ) e. U )
34	1 3 9 10 33 26	ressdeg1	\|- ( ph -> ( D ` ( M ` A ) ) = ( ( deg1 ` K ) ` ( M ` A ) ) )
35	34	breq2d	\|- ( ph -> ( ( ( deg1 ` K ) ` X ) < ( D ` ( M ` A ) ) <-> ( ( deg1 ` K ) ` X ) < ( ( deg1 ` K ) ` ( M ` A ) ) ) )
36		eqid	\|- ( deg1 ` K ) = ( deg1 ` K )
37	5	flddrngd	\|- ( ph -> E e. DivRing )
38	37	drngringd	\|- ( ph -> E e. Ring )
39		eqid	\|- ( Poly1 ` E ) = ( Poly1 ` E )
40		eqid	\|- ( PwSer1 ` K ) = ( PwSer1 ` K )
41		eqid	\|- ( Base ` ( PwSer1 ` K ) ) = ( Base ` ( PwSer1 ` K ) )
42		eqid	\|- ( Base ` ( Poly1 ` E ) ) = ( Base ` ( Poly1 ` E ) )
43	39 1 9 10 26 40 41 42	ressply1bas2	\|- ( ph -> U = ( ( Base ` ( PwSer1 ` K ) ) i^i ( Base ` ( Poly1 ` E ) ) ) )
44		inss2	\|- ( ( Base ` ( PwSer1 ` K ) ) i^i ( Base ` ( Poly1 ` E ) ) ) C_ ( Base ` ( Poly1 ` E ) )
45	43 44	eqsstrdi	\|- ( ph -> U C_ ( Base ` ( Poly1 ` E ) ) )
46	45 33	sseldd	\|- ( ph -> ( M ` A ) e. ( Base ` ( Poly1 ` E ) ) )
47		eqid	\|- ( 0g ` ( Poly1 ` E ) ) = ( 0g ` ( Poly1 ` E ) )
48	47 5 6 4 7	irngnminplynz	\|- ( ph -> ( M ` A ) =/= ( 0g ` ( Poly1 ` E ) ) )
49	3 39 47 42	deg1nn0cl	\|- ( ( E e. Ring /\ ( M ` A ) e. ( Base ` ( Poly1 ` E ) ) /\ ( M ` A ) =/= ( 0g ` ( Poly1 ` E ) ) ) -> ( D ` ( M ` A ) ) e. NN0 )
50	38 46 48 49	syl3anc	\|- ( ph -> ( D ` ( M ` A ) ) e. NN0 )
51		fldsdrgfld	\|- ( ( E e. Field /\ F e. ( SubDRing ` E ) ) -> ( E \|`s F ) e. Field )
52	5 6 51	syl2anc	\|- ( ph -> ( E \|`s F ) e. Field )
53	1 52	eqeltrid	\|- ( ph -> K e. Field )
54		fldidom	\|- ( K e. Field -> K e. IDomn )
55	53 54	syl	\|- ( ph -> K e. IDomn )
56	55	idomringd	\|- ( ph -> K e. Ring )
57	9 36 18 50 56 10	ply1degleel	\|- ( ph -> ( X e. T <-> ( X e. U /\ ( ( deg1 ` K ) ` X ) < ( D ` ( M ` A ) ) ) ) )
58	19 57	mpbirand	\|- ( ph -> ( X e. T <-> ( ( deg1 ` K ) ` X ) < ( D ` ( M ` A ) ) ) )
59		eqid	\|- ( Unic1p ` K ) = ( Unic1p ` K )
60	55	idomdomd	\|- ( ph -> K e. Domn )
61	1	fveq2i	\|- ( Monic1p ` K ) = ( Monic1p ` ( E \|`s F ) )
62	47 5 6 4 7 61	minplym1p	\|- ( ph -> ( M ` A ) e. ( Monic1p ` K ) )
63		eqid	\|- ( Monic1p ` K ) = ( Monic1p ` K )
64	59 63	mon1puc1p	\|- ( ( K e. Ring /\ ( M ` A ) e. ( Monic1p ` K ) ) -> ( M ` A ) e. ( Unic1p ` K ) )
65	56 62 64	syl2anc	\|- ( ph -> ( M ` A ) e. ( Unic1p ` K ) )
66	9 10 59 16 36 60 19 65	r1pid2	\|- ( ph -> ( ( X R ( M ` A ) ) = X <-> ( ( deg1 ` K ) ` X ) < ( ( deg1 ` K ) ` ( M ` A ) ) ) )
67	35 58 66	3bitr4d	\|- ( ph -> ( X e. T <-> ( X R ( M ` A ) ) = X ) )
68		oveq1	\|- ( p = X -> ( p R ( M ` A ) ) = ( X R ( M ` A ) ) )
69		ovexd	\|- ( ph -> ( X R ( M ` A ) ) e. _V )
70	17 68 19 69	fvmptd3	\|- ( ph -> ( H ` X ) = ( X R ( M ` A ) ) )
71	70	eqeq1d	\|- ( ph -> ( ( H ` X ) = X <-> ( X R ( M ` A ) ) = X ) )
72	67 71	bitr4d	\|- ( ph -> ( X e. T <-> ( H ` X ) = X ) )

Metamath Proof Explorer

Theorem algextdeglem7

Proof