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 {evalSub}_{1} S$
	ply1annidl.p	$⊢ P = {Poly}_{1} (R ↾_{𝑠} S)$
	ply1annidl.b	$⊢ B = {Base}_{R}$
	ply1annidl.r	$⊢ φ \to R \in CRing$
	ply1annidl.s	$⊢ φ \to S \in SubRing (R)$
	ply1annidl.a	$⊢ φ \to A \in B$
	ply1annidl.0	$⊢ \underset{˙}{0} = 0_{R}$
	ply1annidl.q	$⊢ Q = \{q \in dom O \| O (q) (A) = \underset{˙}{0}\}$
	ply1annnr.u	$⊢ U = {Base}_{P}$
	ply1annnr.1	$⊢ φ \to R \in NzRing$
Assertion	ply1annnr	$⊢ φ \to Q \neq U$

Proof

Step	Hyp	Ref	Expression
1		ply1annidl.o	$⊢ O = R {evalSub}_{1} S$
2		ply1annidl.p	$⊢ P = {Poly}_{1} (R ↾_{𝑠} S)$
3		ply1annidl.b	$⊢ B = {Base}_{R}$
4		ply1annidl.r	$⊢ φ \to R \in CRing$
5		ply1annidl.s	$⊢ φ \to S \in SubRing (R)$
6		ply1annidl.a	$⊢ φ \to A \in B$
7		ply1annidl.0	$⊢ \underset{˙}{0} = 0_{R}$
8		ply1annidl.q	$⊢ Q = \{q \in dom O \| O (q) (A) = \underset{˙}{0}\}$
9		ply1annnr.u	$⊢ U = {Base}_{P}$
10		ply1annnr.1	$⊢ φ \to R \in NzRing$
11	8	a1i	$⊢ φ \to Q = \{q \in dom O \| O (q) (A) = \underset{˙}{0}\}$
12	4	crngringd	$⊢ φ \to R \in Ring$
13		eqid	$⊢ 1_{R} = 1_{R}$
14	13	subrg1cl	$⊢ S \in SubRing (R) \to 1_{R} \in S$
15	5 14	syl	$⊢ φ \to 1_{R} \in S$
16	3	subrgss	$⊢ S \in SubRing (R) \to S \subseteq B$
17	5 16	syl	$⊢ φ \to S \subseteq B$
18		eqid	$⊢ R ↾_{𝑠} S = R ↾_{𝑠} S$
19	18 3 13	ress1r	$⊢ (R \in Ring \land 1_{R} \in S \land S \subseteq B) \to 1_{R} = 1_{(R ↾_{𝑠} S)}$
20	12 15 17 19	syl3anc	$⊢ φ \to 1_{R} = 1_{(R ↾_{𝑠} S)}$
21	20	fveq2d	$⊢ φ \to algSc (P) (1_{R}) = algSc (P) (1_{(R ↾_{𝑠} S)})$
22		eqid	$⊢ algSc (P) = algSc (P)$
23		eqid	$⊢ 1_{(R ↾_{𝑠} S)} = 1_{(R ↾_{𝑠} S)}$
24		eqid	$⊢ 1_{P} = 1_{P}$
25	18	subrgring	$⊢ S \in SubRing (R) \to R ↾_{𝑠} S \in Ring$
26	5 25	syl	$⊢ φ \to R ↾_{𝑠} S \in Ring$
27	2 22 23 24 26	ply1ascl1	$⊢ φ \to algSc (P) (1_{(R ↾_{𝑠} S)}) = 1_{P}$
28	21 27	eqtrd	$⊢ φ \to algSc (P) (1_{R}) = 1_{P}$
29	2	ply1ring	$⊢ R ↾_{𝑠} S \in Ring \to P \in Ring$
30	9 24	ringidcl	$⊢ P \in Ring \to 1_{P} \in U$
31	26 29 30	3syl	$⊢ φ \to 1_{P} \in U$
32	28 31	eqeltrd	$⊢ φ \to algSc (P) (1_{R}) \in U$
33	1 2 18 3 22 4 5 15 6	evls1scafv	$⊢ φ \to O (algSc (P) (1_{R})) (A) = 1_{R}$
34	13 7	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq \underset{˙}{0}$
35	10 34	syl	$⊢ φ \to 1_{R} \neq \underset{˙}{0}$
36	33 35	eqnetrd	$⊢ φ \to O (algSc (P) (1_{R})) (A) \neq \underset{˙}{0}$
37	36	neneqd	$⊢ φ \to \neg O (algSc (P) (1_{R})) (A) = \underset{˙}{0}$
38		fveq2	$⊢ q = algSc (P) (1_{R}) \to O (q) = O (algSc (P) (1_{R}))$
39	38	fveq1d	$⊢ q = algSc (P) (1_{R}) \to O (q) (A) = O (algSc (P) (1_{R})) (A)$
40	39	eqeq1d	$⊢ q = algSc (P) (1_{R}) \to (O (q) (A) = \underset{˙}{0} \leftrightarrow O (algSc (P) (1_{R})) (A) = \underset{˙}{0})$
41	40	elrab	$⊢ algSc (P) (1_{R}) \in \{q \in dom O \| O (q) (A) = \underset{˙}{0}\} \leftrightarrow (algSc (P) (1_{R}) \in dom O \land O (algSc (P) (1_{R})) (A) = \underset{˙}{0})$
42	41	simprbi	$⊢ algSc (P) (1_{R}) \in \{q \in dom O \| O (q) (A) = \underset{˙}{0}\} \to O (algSc (P) (1_{R})) (A) = \underset{˙}{0}$
43	37 42	nsyl	$⊢ φ \to \neg algSc (P) (1_{R}) \in \{q \in dom O \| O (q) (A) = \underset{˙}{0}\}$
44		nelne1	$⊢ (algSc (P) (1_{R}) \in U \land \neg algSc (P) (1_{R}) \in \{q \in dom O \| O (q) (A) = \underset{˙}{0}\}) \to U \neq \{q \in dom O \| O (q) (A) = \underset{˙}{0}\}$
45	32 43 44	syl2anc	$⊢ φ \to U \neq \{q \in dom O \| O (q) (A) = \underset{˙}{0}\}$
46	45	necomd	$⊢ φ \to \{q \in dom O \| O (q) (A) = \underset{˙}{0}\} \neq U$
47	11 46	eqnetrd	$⊢ φ \to Q \neq U$

Metamath Proof Explorer

Theorem ply1annnr

Proof