Metamath Proof Explorer

Theorem ply1annidllem

Description: Write the set Q of polynomials annihilating an element A as the kernel of the ring homomorphism F mapping polynomials p to their subring evaluation at a given point A . (Contributed by Thierry Arnoux, 9-Feb-2025)

Ref Expression
Hypotheses ply1annidl.o 
|- O = ( R evalSub1 S )
ply1annidl.p 
|- P = ( Poly1 ` ( R |`s S ) )
ply1annidl.b 
|- B = ( Base ` R )
ply1annidl.r 
|- ( ph -> R e. CRing )
ply1annidl.s 
|- ( ph -> S e. ( SubRing ` R ) )
ply1annidl.a 
|- ( ph -> A e. B )
ply1annidl.0 
|- .0. = ( 0g ` R )
ply1annidl.q 
|- Q = { q e. dom O | ( ( O ` q ) ` A ) = .0. }
ply1annidllem.f 
|- F = ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) )
Assertion ply1annidllem 
|- ( ph -> Q = ( `' F " { .0. } ) )

Proof

Step Hyp Ref Expression
1 ply1annidl.o 
 |-  O = ( R evalSub1 S )
2 ply1annidl.p 
 |-  P = ( Poly1 ` ( R |`s S ) )
3 ply1annidl.b 
 |-  B = ( Base ` R )
4 ply1annidl.r 
 |-  ( ph -> R e. CRing )
5 ply1annidl.s 
 |-  ( ph -> S e. ( SubRing ` R ) )
6 ply1annidl.a 
 |-  ( ph -> A e. B )
7 ply1annidl.0 
 |-  .0. = ( 0g ` R )
8 ply1annidl.q 
 |-  Q = { q e. dom O | ( ( O ` q ) ` A ) = .0. }
9 ply1annidllem.f 
 |-  F = ( p e. ( Base ` P ) |-> ( ( O ` p ) ` A ) )
10 nfv 
 |-  F/ p ph
11 fvexd 
 |-  ( ( ph /\ p e. ( Base ` P ) ) -> ( ( O ` p ) ` A ) e. _V )
12 10 11 9 fnmptd 
 |-  ( ph -> F Fn ( Base ` P ) )
13 eqid 
 |-  ( Base ` P ) = ( Base ` P )
14 1 2 13 4 5 evls1fn 
 |-  ( ph -> O Fn ( Base ` P ) )
15 14 fndmd 
 |-  ( ph -> dom O = ( Base ` P ) )
16 15 fneq2d 
 |-  ( ph -> ( F Fn dom O <-> F Fn ( Base ` P ) ) )
17 12 16 mpbird 
 |-  ( ph -> F Fn dom O )
18 fniniseg2 
 |-  ( F Fn dom O -> ( `' F " { .0. } ) = { q e. dom O | ( F ` q ) = .0. } )
19 17 18 syl 
 |-  ( ph -> ( `' F " { .0. } ) = { q e. dom O | ( F ` q ) = .0. } )
20 fveq2 
 |-  ( p = q -> ( O ` p ) = ( O ` q ) )
21 20 fveq1d 
 |-  ( p = q -> ( ( O ` p ) ` A ) = ( ( O ` q ) ` A ) )
22 15 eleq2d 
 |-  ( ph -> ( q e. dom O <-> q e. ( Base ` P ) ) )
23 22 biimpa 
 |-  ( ( ph /\ q e. dom O ) -> q e. ( Base ` P ) )
24 fvexd 
 |-  ( ( ph /\ q e. dom O ) -> ( ( O ` q ) ` A ) e. _V )
25 9 21 23 24 fvmptd3 
 |-  ( ( ph /\ q e. dom O ) -> ( F ` q ) = ( ( O ` q ) ` A ) )
26 25 eqeq1d 
 |-  ( ( ph /\ q e. dom O ) -> ( ( F ` q ) = .0. <-> ( ( O ` q ) ` A ) = .0. ) )
27 26 rabbidva 
 |-  ( ph -> { q e. dom O | ( F ` q ) = .0. } = { q e. dom O | ( ( O ` q ) ` A ) = .0. } )
28 19 27 eqtr2d 
 |-  ( ph -> { q e. dom O | ( ( O ` q ) ` A ) = .0. } = ( `' F " { .0. } ) )
29 8 28 eqtrid 
 |-  ( ph -> Q = ( `' F " { .0. } ) )