Metamath Proof Explorer

Theorem minplymindeg

Description: The minimal polynomial of A is minimal among the nonzero annihilators of A with regard to degree. (Contributed by Thierry Arnoux, 22-Jun-2025)

Ref Expression
Hypotheses ply1annig1p.o 
|- O = ( E evalSub1 F )
ply1annig1p.p 
|- P = ( Poly1 ` ( E |`s F ) )
ply1annig1p.b 
|- B = ( Base ` E )
ply1annig1p.e 
|- ( ph -> E e. Field )
ply1annig1p.f 
|- ( ph -> F e. ( SubDRing ` E ) )
ply1annig1p.a 
|- ( ph -> A e. B )
minplymindeg.0 
|- .0. = ( 0g ` E )
minplymindeg.m 
|- M = ( E minPoly F )
minplymindeg.d 
|- D = ( deg1 ` ( E |`s F ) )
minplymindeg.z 
|- Z = ( 0g ` P )
minplymindeg.u 
|- U = ( Base ` P )
minplymindeg.1 
|- ( ph -> ( ( O ` H ) ` A ) = .0. )
minplymindeg.h 
|- ( ph -> H e. U )
minplymindeg.2 
|- ( ph -> H =/= Z )
Assertion minplymindeg 
|- ( ph -> ( D ` ( M ` A ) ) <_ ( D ` H ) )

Proof

Step Hyp Ref Expression
1 ply1annig1p.o 
 |-  O = ( E evalSub1 F )
2 ply1annig1p.p 
 |-  P = ( Poly1 ` ( E |`s F ) )
3 ply1annig1p.b 
 |-  B = ( Base ` E )
4 ply1annig1p.e 
 |-  ( ph -> E e. Field )
5 ply1annig1p.f 
 |-  ( ph -> F e. ( SubDRing ` E ) )
6 ply1annig1p.a 
 |-  ( ph -> A e. B )
7 minplymindeg.0 
 |-  .0. = ( 0g ` E )
8 minplymindeg.m 
 |-  M = ( E minPoly F )
9 minplymindeg.d 
 |-  D = ( deg1 ` ( E |`s F ) )
10 minplymindeg.z 
 |-  Z = ( 0g ` P )
11 minplymindeg.u 
 |-  U = ( Base ` P )
12 minplymindeg.1 
 |-  ( ph -> ( ( O ` H ) ` A ) = .0. )
13 minplymindeg.h 
 |-  ( ph -> H e. U )
14 minplymindeg.2 
 |-  ( ph -> H =/= Z )
15 eqid 
 |-  { q e. dom O | ( ( O ` q ) ` A ) = .0. } = { q e. dom O | ( ( O ` q ) ` A ) = .0. }
16 eqid 
 |-  ( RSpan ` P ) = ( RSpan ` P )
17 eqid 
 |-  ( idlGen1p ` ( E |`s F ) ) = ( idlGen1p ` ( E |`s F ) )
18 1 2 3 4 5 6 7 15 16 17 8 minplyval 
 |-  ( ph -> ( M ` A ) = ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = .0. } ) )
19 18 fveq2d 
 |-  ( ph -> ( D ` ( M ` A ) ) = ( D ` ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = .0. } ) ) )
20 eqid 
 |-  ( E |`s F ) = ( E |`s F )
21 20 sdrgdrng 
 |-  ( F e. ( SubDRing ` E ) -> ( E |`s F ) e. DivRing )
22 5 21 syl 
 |-  ( ph -> ( E |`s F ) e. DivRing )
23 4 fldcrngd 
 |-  ( ph -> E e. CRing )
24 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
25 5 24 syl 
 |-  ( ph -> F e. ( SubRing ` E ) )
26 1 2 3 23 25 6 7 15 ply1annidl 
 |-  ( ph -> { q e. dom O | ( ( O ` q ) ` A ) = .0. } e. ( LIdeal ` P ) )
27 fveq2 
 |-  ( q = H -> ( O ` q ) = ( O ` H ) )
28 27 fveq1d 
 |-  ( q = H -> ( ( O ` q ) ` A ) = ( ( O ` H ) ` A ) )
29 28 eqeq1d 
 |-  ( q = H -> ( ( ( O ` q ) ` A ) = .0. <-> ( ( O ` H ) ` A ) = .0. ) )
30 1 2 11 23 25 evls1dm 
 |-  ( ph -> dom O = U )
31 13 30 eleqtrrd 
 |-  ( ph -> H e. dom O )
32 29 31 12 elrabd 
 |-  ( ph -> H e. { q e. dom O | ( ( O ` q ) ` A ) = .0. } )
33 2 17 11 22 26 9 10 32 14 ig1pmindeg 
 |-  ( ph -> ( D ` ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = .0. } ) ) <_ ( D ` H ) )
34 19 33 eqbrtrd 
 |-  ( ph -> ( D ` ( M ` A ) ) <_ ( D ` H ) )