Theorem 0ringmon1p

Description: There are no monic polynomials over a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025)

	Ref	Expression
Hypotheses	0ringmon1p.1	$$⊢M={Monic}_{\mathrm{1p}}\left(R\right)$$
	0ringmon1p.2	$$⊢B={\mathrm{Base}}_R$$
	0ringmon1p.3	$$⊢\phi \to R\in \mathrm{Ring}$$
	0ringmon1p.4	$$⊢\phi \to \left|B\right|=1$$
Assertion	0ringmon1p	$$⊢\phi \to M=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0ringmon1p.1	$$⊢M={Monic}_{\mathrm{1p}}\left(R\right)$$
2		0ringmon1p.2	$$⊢B={\mathrm{Base}}_R$$
3		0ringmon1p.3	$$⊢\phi \to R\in \mathrm{Ring}$$
4		0ringmon1p.4	$$⊢\phi \to \left|B\right|=1$$
5		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
6		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
7		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(R\right)}=0_{{\mathrm{Poly}}_1\left(R\right)}$$
8		eqid	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(R\right)$$
9		eqid	$$⊢1_R=1_R$$
10	5 6 7 8 1 9	ismon1p	$$⊢p\in M\leftrightarrow \left(p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge p\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\wedge {\mathrm{coe}}_1\left(p\right)\left({\mathrm{deg}}_1\left(R\right)\left(p\right)\right)=1_R\right)$$
11	10	biimpi	$$⊢p\in M\to \left(p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge p\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\wedge {\mathrm{coe}}_1\left(p\right)\left({\mathrm{deg}}_1\left(R\right)\left(p\right)\right)=1_R\right)$$
12	11	adantl	$$⊢\left(\phi \wedge p\in M\right)\to \left(p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge p\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\wedge {\mathrm{coe}}_1\left(p\right)\left({\mathrm{deg}}_1\left(R\right)\left(p\right)\right)=1_R\right)$$
13	12	simp3d	$$⊢\left(\phi \wedge p\in M\right)\to {\mathrm{coe}}_1\left(p\right)\left({\mathrm{deg}}_1\left(R\right)\left(p\right)\right)=1_R$$
14	3	adantr	$$⊢\left(\phi \wedge p\in M\right)\to R\in \mathrm{Ring}$$
15	12	simp1d	$$⊢\left(\phi \wedge p\in M\right)\to p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
16	12	simp2d	$$⊢\left(\phi \wedge p\in M\right)\to p\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
17		eqid	$$⊢0_R=0_R$$
18		eqid	$$⊢{\mathrm{coe}}_1\left(p\right)={\mathrm{coe}}_1\left(p\right)$$
19	8 5 7 6 17 18	deg1ldg	$$⊢\left(R\in \mathrm{Ring}\wedge p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}\wedge p\ne 0_{{\mathrm{Poly}}_1\left(R\right)}\right)\to {\mathrm{coe}}_1\left(p\right)\left({\mathrm{deg}}_1\left(R\right)\left(p\right)\right)\ne 0_R$$
20	14 15 16 19	syl3anc	$$⊢\left(\phi \wedge p\in M\right)\to {\mathrm{coe}}_1\left(p\right)\left({\mathrm{deg}}_1\left(R\right)\left(p\right)\right)\ne 0_R$$
21	2 17 9	0ring01eq	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to 0_R=1_R$$
22	3 4 21	syl2anc	$$⊢\phi \to 0_R=1_R$$
23	22	adantr	$$⊢\left(\phi \wedge p\in M\right)\to 0_R=1_R$$
24	20 23	neeqtrd	$$⊢\left(\phi \wedge p\in M\right)\to {\mathrm{coe}}_1\left(p\right)\left({\mathrm{deg}}_1\left(R\right)\left(p\right)\right)\ne 1_R$$
25	24	neneqd	$$⊢\left(\phi \wedge p\in M\right)\to \neg {\mathrm{coe}}_1\left(p\right)\left({\mathrm{deg}}_1\left(R\right)\left(p\right)\right)=1_R$$
26	13 25	pm2.65da	$$⊢\phi \to \neg p\in M$$
27	26	eq0rdv	$$⊢\phi \to M=\varnothing$$