Metamath Proof Explorer

Theorem minplyval

Description: Expand the value of the minimal polynomial ( MA ) for a given element A . It is defined as the unique monic polynomial of minimal degree which annihilates A . By ply1annig1p , that polynomial generates the ideal of the annihilators of A . (Contributed by Thierry Arnoux, 9-Feb-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 minplyval 
|- ( ph -> ( M ` A ) = ( G ` Q ) )

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 4 elexd 
 |-  ( ph -> E e. _V )
13 5 elexd 
 |-  ( ph -> F e. _V )
14 3 fvexi 
 |-  B e. _V
15 14 a1i 
 |-  ( ph -> B e. _V )
16 15 mptexd 
 |-  ( ph -> ( x e. B |-> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) ) e. _V )
17 fveq2 
 |-  ( e = E -> ( Base ` e ) = ( Base ` E ) )
18 17 3 eqtr4di 
 |-  ( e = E -> ( Base ` e ) = B )
19 18 adantr 
 |-  ( ( e = E /\ f = F ) -> ( Base ` e ) = B )
20 oveq12 
 |-  ( ( e = E /\ f = F ) -> ( e |`s f ) = ( E |`s F ) )
21 20 fveq2d 
 |-  ( ( e = E /\ f = F ) -> ( idlGen1p ` ( e |`s f ) ) = ( idlGen1p ` ( E |`s F ) ) )
22 21 10 eqtr4di 
 |-  ( ( e = E /\ f = F ) -> ( idlGen1p ` ( e |`s f ) ) = G )
23 oveq12 
 |-  ( ( e = E /\ f = F ) -> ( e evalSub1 f ) = ( E evalSub1 F ) )
24 23 1 eqtr4di 
 |-  ( ( e = E /\ f = F ) -> ( e evalSub1 f ) = O )
25 24 dmeqd 
 |-  ( ( e = E /\ f = F ) -> dom ( e evalSub1 f ) = dom O )
26 24 fveq1d 
 |-  ( ( e = E /\ f = F ) -> ( ( e evalSub1 f ) ` q ) = ( O ` q ) )
27 26 fveq1d 
 |-  ( ( e = E /\ f = F ) -> ( ( ( e evalSub1 f ) ` q ) ` x ) = ( ( O ` q ) ` x ) )
28 fveq2 
 |-  ( e = E -> ( 0g ` e ) = ( 0g ` E ) )
29 28 adantr 
 |-  ( ( e = E /\ f = F ) -> ( 0g ` e ) = ( 0g ` E ) )
30 29 7 eqtr4di 
 |-  ( ( e = E /\ f = F ) -> ( 0g ` e ) = .0. )
31 27 30 eqeq12d 
 |-  ( ( e = E /\ f = F ) -> ( ( ( ( e evalSub1 f ) ` q ) ` x ) = ( 0g ` e ) <-> ( ( O ` q ) ` x ) = .0. ) )
32 25 31 rabeqbidv 
 |-  ( ( e = E /\ f = F ) -> { q e. dom ( e evalSub1 f ) | ( ( ( e evalSub1 f ) ` q ) ` x ) = ( 0g ` e ) } = { q e. dom O | ( ( O ` q ) ` x ) = .0. } )
33 22 32 fveq12d 
 |-  ( ( e = E /\ f = F ) -> ( ( idlGen1p ` ( e |`s f ) ) ` { q e. dom ( e evalSub1 f ) | ( ( ( e evalSub1 f ) ` q ) ` x ) = ( 0g ` e ) } ) = ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) )
34 19 33 mpteq12dv 
 |-  ( ( e = E /\ f = F ) -> ( x e. ( Base ` e ) |-> ( ( idlGen1p ` ( e |`s f ) ) ` { q e. dom ( e evalSub1 f ) | ( ( ( e evalSub1 f ) ` q ) ` x ) = ( 0g ` e ) } ) ) = ( x e. B |-> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) ) )
35 df-minply 
 |-  minPoly = ( e e. _V , f e. _V |-> ( x e. ( Base ` e ) |-> ( ( idlGen1p ` ( e |`s f ) ) ` { q e. dom ( e evalSub1 f ) | ( ( ( e evalSub1 f ) ` q ) ` x ) = ( 0g ` e ) } ) ) )
36 34 35 ovmpoga 
 |-  ( ( E e. _V /\ F e. _V /\ ( x e. B |-> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) ) e. _V ) -> ( E minPoly F ) = ( x e. B |-> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) ) )
37 12 13 16 36 syl3anc 
 |-  ( ph -> ( E minPoly F ) = ( x e. B |-> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) ) )
38 11 37 eqtrid 
 |-  ( ph -> M = ( x e. B |-> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) ) )
39 fveqeq2 
 |-  ( x = A -> ( ( ( O ` q ) ` x ) = .0. <-> ( ( O ` q ) ` A ) = .0. ) )
40 39 rabbidv 
 |-  ( x = A -> { q e. dom O | ( ( O ` q ) ` x ) = .0. } = { q e. dom O | ( ( O ` q ) ` A ) = .0. } )
41 40 8 eqtr4di 
 |-  ( x = A -> { q e. dom O | ( ( O ` q ) ` x ) = .0. } = Q )
42 41 fveq2d 
 |-  ( x = A -> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) = ( G ` Q ) )
43 42 adantl 
 |-  ( ( ph /\ x = A ) -> ( G ` { q e. dom O | ( ( O ` q ) ` x ) = .0. } ) = ( G ` Q ) )
44 fvexd 
 |-  ( ph -> ( G ` Q ) e. _V )
45 38 43 6 44 fvmptd 
 |-  ( ph -> ( M ` A ) = ( G ` Q ) )