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

Metamath Proof Explorer

Theorem minplyann

Description: The minimal polynomial for A annihilates A . (Contributed by Thierry Arnoux, 25-Apr-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 )
minplyann.1 
|- .0. = ( 0g ` E )
minplyann.m 
|- M = ( E minPoly F )
Assertion minplyann 
|- ( ph -> ( ( O ` ( M ` A ) ) ` A ) = .0. )

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 minplyann.1 
 |-  .0. = ( 0g ` E )
8 minplyann.m 
 |-  M = ( E minPoly F )
9 eqid 
 |-  { q e. dom O | ( ( O ` q ) ` A ) = .0. } = { q e. dom O | ( ( O ` q ) ` A ) = .0. }
10 eqid 
 |-  ( RSpan ` P ) = ( RSpan ` P )
11 eqid 
 |-  ( idlGen1p ` ( E |`s F ) ) = ( idlGen1p ` ( E |`s F ) )
12 1 2 3 4 5 6 7 9 10 11 8 minplyval 
 |-  ( ph -> ( M ` A ) = ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = .0. } ) )
13 eqid 
 |-  ( E |`s F ) = ( E |`s F )
14 13 sdrgdrng 
 |-  ( F e. ( SubDRing ` E ) -> ( E |`s F ) e. DivRing )
15 5 14 syl 
 |-  ( ph -> ( E |`s F ) e. DivRing )
16 4 fldcrngd 
 |-  ( ph -> E e. CRing )
17 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
18 5 17 syl 
 |-  ( ph -> F e. ( SubRing ` E ) )
19 1 2 3 16 18 6 7 9 ply1annidl 
 |-  ( ph -> { q e. dom O | ( ( O ` q ) ` A ) = .0. } e. ( LIdeal ` P ) )
20 eqid 
 |-  ( LIdeal ` P ) = ( LIdeal ` P )
21 2 11 20 ig1pcl 
 |-  ( ( ( E |`s F ) e. DivRing /\ { q e. dom O | ( ( O ` q ) ` A ) = .0. } e. ( LIdeal ` P ) ) -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = .0. } ) e. { q e. dom O | ( ( O ` q ) ` A ) = .0. } )
22 15 19 21 syl2anc 
 |-  ( ph -> ( ( idlGen1p ` ( E |`s F ) ) ` { q e. dom O | ( ( O ` q ) ` A ) = .0. } ) e. { q e. dom O | ( ( O ` q ) ` A ) = .0. } )
23 12 22 eqeltrd 
 |-  ( ph -> ( M ` A ) e. { q e. dom O | ( ( O ` q ) ` A ) = .0. } )
24 fveq2 
 |-  ( q = ( M ` A ) -> ( O ` q ) = ( O ` ( M ` A ) ) )
25 24 fveq1d 
 |-  ( q = ( M ` A ) -> ( ( O ` q ) ` A ) = ( ( O ` ( M ` A ) ) ` A ) )
26 25 eqeq1d 
 |-  ( q = ( M ` A ) -> ( ( ( O ` q ) ` A ) = .0. <-> ( ( O ` ( M ` A ) ) ` A ) = .0. ) )
27 26 elrab 
 |-  ( ( M ` A ) e. { q e. dom O | ( ( O ` q ) ` A ) = .0. } <-> ( ( M ` A ) e. dom O /\ ( ( O ` ( M ` A ) ) ` A ) = .0. ) )
28 23 27 sylib 
 |-  ( ph -> ( ( M ` A ) e. dom O /\ ( ( O ` ( M ` A ) ) ` A ) = .0. ) )
29 28 simprd 
 |-  ( ph -> ( ( O ` ( M ` A ) ) ` A ) = .0. )