This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 
|- 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 ) )