Theorem pridln1

Description: A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024)

	Ref	Expression
Hypotheses	pridln1.1	$$⊢B={\mathrm{Base}}_R$$
	pridln1.2	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	pridln1	$$⊢\left(R\in \mathrm{Ring}\wedge I\in \mathrm{LIdeal}\left(R\right)\wedge I\ne B\right)\to \neg \underset{\dot{}}{1}\in I$$

Proof

Step	Hyp	Ref	Expression
1		pridln1.1	$$⊢B={\mathrm{Base}}_R$$
2		pridln1.2	$$⊢\underset{\dot{}}{1}=1_R$$
3		eqid	$$⊢\mathrm{LIdeal}\left(R\right)=\mathrm{LIdeal}\left(R\right)$$
4	3 1 2	lidl1el	$$⊢\left(R\in \mathrm{Ring}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\to \left(\underset{\dot{}}{1}\in I\leftrightarrow I=B\right)$$
5	4	necon3bbid	$$⊢\left(R\in \mathrm{Ring}\wedge I\in \mathrm{LIdeal}\left(R\right)\right)\to \left(\neg \underset{\dot{}}{1}\in I\leftrightarrow I\ne B\right)$$
6	5	biimp3ar	$$⊢\left(R\in \mathrm{Ring}\wedge I\in \mathrm{LIdeal}\left(R\right)\wedge I\ne B\right)\to \neg \underset{\dot{}}{1}\in I$$