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

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 ⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
ply1annidl.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
ply1annidl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ply1annidl.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
ply1annidl.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
ply1annidl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
ply1annidl.0 ⊢ 0 = ( 0g ‘ 𝑅 )
ply1annidl.q ⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
ply1annnr.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
ply1annnr.1 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
Assertion ply1annnr ( 𝜑 → 𝑄 ≠ 𝑈 )

Proof

Step Hyp Ref Expression
1 ply1annidl.o ⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
2 ply1annidl.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
3 ply1annidl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 ply1annidl.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
5 ply1annidl.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
6 ply1annidl.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7 ply1annidl.0 ⊢ 0 = ( 0g ‘ 𝑅 )
8 ply1annidl.q ⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
9 ply1annnr.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
10 ply1annnr.1 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
11 8 a1i ⊢ ( 𝜑 → 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
12 4 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
13 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
14 13 subrg1cl ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
15 5 14 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
16 3 subrgss ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ⊆ 𝐵 )
17 5 16 syl ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
18 eqid ⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
19 18 3 13 ress1r ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) )
20 12 15 17 19 syl3anc ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) )
21 20 fveq2d ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
22 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
23 eqid ⊢ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) )
24 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
25 18 subrgring ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
26 5 25 syl ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
27 2 22 23 24 26 ply1ascl1 ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( 1r ‘ 𝑃 ) )
28 21 27 eqtrd ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
29 2 ply1ring ⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ Ring → 𝑃 ∈ Ring )
30 9 24 ringidcl ⊢ ( 𝑃 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ 𝑈 )
31 26 29 30 3syl ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) ∈ 𝑈 )
32 28 31 eqeltrd ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝑈 )
33 1 2 18 3 22 4 5 15 6 evls1scafv ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) = ( 1r ‘ 𝑅 ) )
34 13 7 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ 0 )
35 10 34 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ 0 )
36 33 35 eqnetrd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) ≠ 0 )
37 36 neneqd ⊢ ( 𝜑 → ¬ ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) = 0 )
38 fveq2 ⊢ ( 𝑞 = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) → ( 𝑂 ‘ 𝑞 ) = ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
39 38 fveq1d ⊢ ( 𝑞 = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) → ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) )
40 39 eqeq1d ⊢ ( 𝑞 = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) → ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 ↔ ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) = 0 ) )
41 40 elrab ⊢ ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ↔ ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ dom 𝑂 ∧ ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) = 0 ) )
42 41 simprbi ⊢ ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝐴 ) = 0 )
43 37 42 nsyl ⊢ ( 𝜑 → ¬ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
44 nelne1 ⊢ ( ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝑈 ∧ ¬ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) → 𝑈 ≠ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
45 32 43 44 syl2anc ⊢ ( 𝜑 → 𝑈 ≠ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
46 45 necomd ⊢ ( 𝜑 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ≠ 𝑈 )
47 11 46 eqnetrd ⊢ ( 𝜑 → 𝑄 ≠ 𝑈 )