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	bilani	$$⊢\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)$$
12	11	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$$
13	3	adantr	$$⊢\left(\phi \wedge p\in M\right)\to R\in \mathrm{Ring}$$
14	11	simp1d	$$⊢\left(\phi \wedge p\in M\right)\to p\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
15	11	simp2d	$$⊢\left(\phi \wedge p\in M\right)\to p\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
16		eqid	$$⊢0_R=0_R$$
17		eqid	$$⊢{\mathrm{coe}}_1\left(p\right)={\mathrm{coe}}_1\left(p\right)$$
18	8 5 7 6 16 17	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$$
19	13 14 15 18	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$$
20	2 16 9	0ring01eq	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to 0_R=1_R$$
21	3 4 20	syl2anc	$$⊢\phi \to 0_R=1_R$$
22	21	adantr	$$⊢\left(\phi \wedge p\in M\right)\to 0_R=1_R$$
23	19 22	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$$
24	23	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$$
25	12 24	pm2.65da	$$⊢\phi \to \neg p\in M$$
26	25	eq0rdv	$$⊢\phi \to M=\varnothing$$