Theorem islpidl

Description: Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lpival.p	$$⊢P=\mathrm{LPIdeal}\left(R\right)$$
	lpival.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
	lpival.b	$$⊢B={\mathrm{Base}}_R$$
Assertion	islpidl	$$⊢R\in \mathrm{Ring}\to \left(I\in P\leftrightarrow \exists g\in BI=K\left(\left\{g\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		lpival.p	$$⊢P=\mathrm{LPIdeal}\left(R\right)$$
2		lpival.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
3		lpival.b	$$⊢B={\mathrm{Base}}_R$$
4	1 2 3	lpival	$$⊢R\in \mathrm{Ring}\to P=\bigcup _{g\in B}\left\{K\left(\left\{g\right\}\right)\right\}$$
5	4	eleq2d	$$⊢R\in \mathrm{Ring}\to \left(I\in P\leftrightarrow I\in \bigcup _{g\in B}\left\{K\left(\left\{g\right\}\right)\right\}\right)$$
6		eliun	$$⊢I\in \bigcup _{g\in B}\left\{K\left(\left\{g\right\}\right)\right\}\leftrightarrow \exists g\in BI\in \left\{K\left(\left\{g\right\}\right)\right\}$$
7		fvex	$$⊢K\left(\left\{g\right\}\right)\in \mathrm{V}$$
8	7	elsn2	$$⊢I\in \left\{K\left(\left\{g\right\}\right)\right\}\leftrightarrow I=K\left(\left\{g\right\}\right)$$
9	8	rexbii	$$⊢\exists g\in BI\in \left\{K\left(\left\{g\right\}\right)\right\}\leftrightarrow \exists g\in BI=K\left(\left\{g\right\}\right)$$
10	6 9	bitri	$$⊢I\in \bigcup _{g\in B}\left\{K\left(\left\{g\right\}\right)\right\}\leftrightarrow \exists g\in BI=K\left(\left\{g\right\}\right)$$
11	5 10	bitrdi	$$⊢R\in \mathrm{Ring}\to \left(I\in P\leftrightarrow \exists g\in BI=K\left(\left\{g\right\}\right)\right)$$