Theorem isnirred

Description: The property of being a non-irreducible (reducible) element in a ring. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	irred.1	$$⊢B={\mathrm{Base}}_R$$
	irred.2	$$⊢U=\mathrm{Unit}\left(R\right)$$
	irred.3	$$⊢I=\mathrm{Irred}\left(R\right)$$
	irred.4	$$⊢N=B\setminus U$$
	irred.5	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	isnirred	$$⊢X\in B\to \left(\neg X\in I\leftrightarrow \left(X\in U\vee \exists x\in N\exists y\in Nx\underset{\dot{}}{·}y=X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		irred.1	$$⊢B={\mathrm{Base}}_R$$
2		irred.2	$$⊢U=\mathrm{Unit}\left(R\right)$$
3		irred.3	$$⊢I=\mathrm{Irred}\left(R\right)$$
4		irred.4	$$⊢N=B\setminus U$$
5		irred.5	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
6	4	eleq2i	$$⊢X\in N\leftrightarrow X\in \left(B\setminus U\right)$$
7		eldif	$$⊢X\in \left(B\setminus U\right)\leftrightarrow \left(X\in B\wedge \neg X\in U\right)$$
8	6 7	bitri	$$⊢X\in N\leftrightarrow \left(X\in B\wedge \neg X\in U\right)$$
9	8	baibr	$$⊢X\in B\to \left(\neg X\in U\leftrightarrow X\in N\right)$$
10		df-ne	$$⊢x\underset{\dot{}}{·}y\ne X\leftrightarrow \neg x\underset{\dot{}}{·}y=X$$
11	10	ralbii	$$⊢\forall y\in Nx\underset{\dot{}}{·}y\ne X\leftrightarrow \forall y\in N\neg x\underset{\dot{}}{·}y=X$$
12		ralnex	$$⊢\forall y\in N\neg x\underset{\dot{}}{·}y=X\leftrightarrow \neg \exists y\in Nx\underset{\dot{}}{·}y=X$$
13	11 12	bitri	$$⊢\forall y\in Nx\underset{\dot{}}{·}y\ne X\leftrightarrow \neg \exists y\in Nx\underset{\dot{}}{·}y=X$$
14	13	ralbii	$$⊢\forall x\in N\forall y\in Nx\underset{\dot{}}{·}y\ne X\leftrightarrow \forall x\in N\neg \exists y\in Nx\underset{\dot{}}{·}y=X$$
15		ralnex	$$⊢\forall x\in N\neg \exists y\in Nx\underset{\dot{}}{·}y=X\leftrightarrow \neg \exists x\in N\exists y\in Nx\underset{\dot{}}{·}y=X$$
16	14 15	bitr2i	$$⊢\neg \exists x\in N\exists y\in Nx\underset{\dot{}}{·}y=X\leftrightarrow \forall x\in N\forall y\in Nx\underset{\dot{}}{·}y\ne X$$
17	16	a1i	$$⊢X\in B\to \left(\neg \exists x\in N\exists y\in Nx\underset{\dot{}}{·}y=X\leftrightarrow \forall x\in N\forall y\in Nx\underset{\dot{}}{·}y\ne X\right)$$
18	9 17	anbi12d	$$⊢X\in B\to \left(\left(\neg X\in U\wedge \neg \exists x\in N\exists y\in Nx\underset{\dot{}}{·}y=X\right)\leftrightarrow \left(X\in N\wedge \forall x\in N\forall y\in Nx\underset{\dot{}}{·}y\ne X\right)\right)$$
19		ioran	$$⊢\neg \left(X\in U\vee \exists x\in N\exists y\in Nx\underset{\dot{}}{·}y=X\right)\leftrightarrow \left(\neg X\in U\wedge \neg \exists x\in N\exists y\in Nx\underset{\dot{}}{·}y=X\right)$$
20	1 2 3 4 5	isirred	$$⊢X\in I\leftrightarrow \left(X\in N\wedge \forall x\in N\forall y\in Nx\underset{\dot{}}{·}y\ne X\right)$$
21	18 19 20	3bitr4g	$$⊢X\in B\to \left(\neg \left(X\in U\vee \exists x\in N\exists y\in Nx\underset{\dot{}}{·}y=X\right)\leftrightarrow X\in I\right)$$
22	21	con1bid	$$⊢X\in B\to \left(\neg X\in I\leftrightarrow \left(X\in U\vee \exists x\in N\exists y\in Nx\underset{\dot{}}{·}y=X\right)\right)$$