Metamath Proof Explorer

Theorem ply1annnr

Description: The set Q of polynomials annihilating an element A is not the whole polynomial ring. (Contributed by Thierry Arnoux, 22-Mar-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. }
ply1annnr.u 
|- U = ( Base ` P )
ply1annnr.1 
|- ( ph -> R e. NzRing )
Assertion ply1annnr 
|- ( ph -> Q =/= U )

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 ply1annnr.u 
 |-  U = ( Base ` P )
10 ply1annnr.1 
 |-  ( ph -> R e. NzRing )
11 8 a1i 
 |-  ( ph -> Q = { q e. dom O | ( ( O ` q ) ` A ) = .0. } )
12 4 crngringd 
 |-  ( ph -> R e. Ring )
13 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
14 13 subrg1cl 
 |-  ( S e. ( SubRing ` R ) -> ( 1r ` R ) e. S )
15 5 14 syl 
 |-  ( ph -> ( 1r ` R ) e. S )
16 3 subrgss 
 |-  ( S e. ( SubRing ` R ) -> S C_ B )
17 5 16 syl 
 |-  ( ph -> S C_ B )
18 eqid 
 |-  ( R |`s S ) = ( R |`s S )
19 18 3 13 ress1r 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. S /\ S C_ B ) -> ( 1r ` R ) = ( 1r ` ( R |`s S ) ) )
20 12 15 17 19 syl3anc 
 |-  ( ph -> ( 1r ` R ) = ( 1r ` ( R |`s S ) ) )
21 20 fveq2d 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( ( algSc ` P ) ` ( 1r ` ( R |`s S ) ) ) )
22 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
23 eqid 
 |-  ( 1r ` ( R |`s S ) ) = ( 1r ` ( R |`s S ) )
24 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
25 18 subrgring 
 |-  ( S e. ( SubRing ` R ) -> ( R |`s S ) e. Ring )
26 5 25 syl 
 |-  ( ph -> ( R |`s S ) e. Ring )
27 2 22 23 24 26 ply1ascl1 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` ( R |`s S ) ) ) = ( 1r ` P ) )
28 21 27 eqtrd 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
29 2 ply1ring 
 |-  ( ( R |`s S ) e. Ring -> P e. Ring )
30 9 24 ringidcl 
 |-  ( P e. Ring -> ( 1r ` P ) e. U )
31 26 29 30 3syl 
 |-  ( ph -> ( 1r ` P ) e. U )
32 28 31 eqeltrd 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) e. U )
33 1 2 18 3 22 4 5 15 6 evls1scafv 
 |-  ( ph -> ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) = ( 1r ` R ) )
34 13 7 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= .0. )
35 10 34 syl 
 |-  ( ph -> ( 1r ` R ) =/= .0. )
36 33 35 eqnetrd 
 |-  ( ph -> ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) =/= .0. )
37 36 neneqd 
 |-  ( ph -> -. ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) = .0. )
38 fveq2 
 |-  ( q = ( ( algSc ` P ) ` ( 1r ` R ) ) -> ( O ` q ) = ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) )
39 38 fveq1d 
 |-  ( q = ( ( algSc ` P ) ` ( 1r ` R ) ) -> ( ( O ` q ) ` A ) = ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) )
40 39 eqeq1d 
 |-  ( q = ( ( algSc ` P ) ` ( 1r ` R ) ) -> ( ( ( O ` q ) ` A ) = .0. <-> ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) = .0. ) )
41 40 elrab 
 |-  ( ( ( algSc ` P ) ` ( 1r ` R ) ) e. { q e. dom O | ( ( O ` q ) ` A ) = .0. } <-> ( ( ( algSc ` P ) ` ( 1r ` R ) ) e. dom O /\ ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) = .0. ) )
42 41 simprbi 
 |-  ( ( ( algSc ` P ) ` ( 1r ` R ) ) e. { q e. dom O | ( ( O ` q ) ` A ) = .0. } -> ( ( O ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` A ) = .0. )
43 37 42 nsyl 
 |-  ( ph -> -. ( ( algSc ` P ) ` ( 1r ` R ) ) e. { q e. dom O | ( ( O ` q ) ` A ) = .0. } )
44 nelne1 
 |-  ( ( ( ( algSc ` P ) ` ( 1r ` R ) ) e. U /\ -. ( ( algSc ` P ) ` ( 1r ` R ) ) e. { q e. dom O | ( ( O ` q ) ` A ) = .0. } ) -> U =/= { q e. dom O | ( ( O ` q ) ` A ) = .0. } )
45 32 43 44 syl2anc 
 |-  ( ph -> U =/= { q e. dom O | ( ( O ` q ) ` A ) = .0. } )
46 45 necomd 
 |-  ( ph -> { q e. dom O | ( ( O ` q ) ` A ) = .0. } =/= U )
47 11 46 eqnetrd 
 |-  ( ph -> Q =/= U )