Metamath Proof Explorer

Theorem minplycl

Description: The minimal polynomial is a polynomial. (Contributed by Thierry Arnoux, 22-Mar-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 )
ply1annig1p.0 
|- .0. = ( 0g ` E )
ply1annig1p.q 
|- Q = { q e. dom O | ( ( O ` q ) ` A ) = .0. }
ply1annig1p.k 
|- K = ( RSpan ` P )
ply1annig1p.g 
|- G = ( idlGen1p ` ( E |`s F ) )
minplyval.1 
|- M = ( E minPoly F )
Assertion minplycl 
|- ( ph -> ( M ` A ) e. ( Base ` P ) )

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 ply1annig1p.0 
 |-  .0. = ( 0g ` E )
8 ply1annig1p.q 
 |-  Q = { q e. dom O | ( ( O ` q ) ` A ) = .0. }
9 ply1annig1p.k 
 |-  K = ( RSpan ` P )
10 ply1annig1p.g 
 |-  G = ( idlGen1p ` ( E |`s F ) )
11 minplyval.1 
 |-  M = ( E minPoly F )
12 1 2 3 4 5 6 7 8 9 10 11 minplyval 
 |-  ( ph -> ( M ` A ) = ( G ` Q ) )
13 4 fldcrngd 
 |-  ( ph -> E e. CRing )
14 issdrg 
 |-  ( F e. ( SubDRing ` E ) <-> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
15 5 14 sylib 
 |-  ( ph -> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
16 15 simp2d 
 |-  ( ph -> F e. ( SubRing ` E ) )
17 1 2 3 13 16 6 7 8 ply1annidl 
 |-  ( ph -> Q e. ( LIdeal ` P ) )
18 eqid 
 |-  ( Base ` P ) = ( Base ` P )
19 eqid 
 |-  ( LIdeal ` P ) = ( LIdeal ` P )
20 18 19 lidlss 
 |-  ( Q e. ( LIdeal ` P ) -> Q C_ ( Base ` P ) )
21 17 20 syl 
 |-  ( ph -> Q C_ ( Base ` P ) )
22 15 simp3d 
 |-  ( ph -> ( E |`s F ) e. DivRing )
23 2 10 19 ig1pcl 
 |-  ( ( ( E |`s F ) e. DivRing /\ Q e. ( LIdeal ` P ) ) -> ( G ` Q ) e. Q )
24 22 17 23 syl2anc 
 |-  ( ph -> ( G ` Q ) e. Q )
25 21 24 sseldd 
 |-  ( ph -> ( G ` Q ) e. ( Base ` P ) )
26 12 25 eqeltrd 
 |-  ( ph -> ( M ` A ) e. ( Base ` P ) )