Theorem irredn1

Description: The multiplicative identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014)

	Ref	Expression
Hypotheses	irredn0.i	$$⊢I=\mathrm{Irred}\left(R\right)$$
	irredn1.o	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	irredn1	$$⊢\left(R\in \mathrm{Ring}\wedge X\in I\right)\to X\ne \underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		irredn0.i	$$⊢I=\mathrm{Irred}\left(R\right)$$
2		irredn1.o	$$⊢\underset{\dot{}}{1}=1_R$$
3		eqid	$$⊢\mathrm{Unit}\left(R\right)=\mathrm{Unit}\left(R\right)$$
4	3 2	1unit	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in \mathrm{Unit}\left(R\right)$$
5		eleq1	$$⊢X=\underset{\dot{}}{1}\to \left(X\in \mathrm{Unit}\left(R\right)\leftrightarrow \underset{\dot{}}{1}\in \mathrm{Unit}\left(R\right)\right)$$
6	4 5	syl5ibrcom	$$⊢R\in \mathrm{Ring}\to \left(X=\underset{\dot{}}{1}\to X\in \mathrm{Unit}\left(R\right)\right)$$
7	6	necon3bd	$$⊢R\in \mathrm{Ring}\to \left(\neg X\in \mathrm{Unit}\left(R\right)\to X\ne \underset{\dot{}}{1}\right)$$
8	1 3	irrednu	$$⊢X\in I\to \neg X\in \mathrm{Unit}\left(R\right)$$
9	7 8	impel	$$⊢\left(R\in \mathrm{Ring}\wedge X\in I\right)\to X\ne \underset{\dot{}}{1}$$