Theorem lpiss

Description: Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lpival.p	$$⊢P=\mathrm{LPIdeal}\left(R\right)$$
	lpiss.u	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
Assertion	lpiss	$$⊢R\in \mathrm{Ring}\to P\subseteq U$$

Proof

Step	Hyp	Ref	Expression
1		lpival.p	$$⊢P=\mathrm{LPIdeal}\left(R\right)$$
2		lpiss.u	$$⊢U=\mathrm{LIdeal}\left(R\right)$$
3		eqid	$$⊢\mathrm{RSpan}\left(R\right)=\mathrm{RSpan}\left(R\right)$$
4		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
5	1 3 4	islpidl	$$⊢R\in \mathrm{Ring}\to \left(a\in P\leftrightarrow \exists g\in {\mathrm{Base}}_{R}a=\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\right)$$
6		snssi	$$⊢g\in {\mathrm{Base}}_R\to \left\{g\right\}\subseteq {\mathrm{Base}}_R$$
7	3 4 2	rspcl	$$⊢\left(R\in \mathrm{Ring}\wedge \left\{g\right\}\subseteq {\mathrm{Base}}_R\right)\to \mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\in U$$
8	6 7	sylan2	$$⊢\left(R\in \mathrm{Ring}\wedge g\in {\mathrm{Base}}_R\right)\to \mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\in U$$
9		eleq1	$$⊢a=\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\to \left(a\in U\leftrightarrow \mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\in U\right)$$
10	8 9	syl5ibrcom	$$⊢\left(R\in \mathrm{Ring}\wedge g\in {\mathrm{Base}}_R\right)\to \left(a=\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\to a\in U\right)$$
11	10	rexlimdva	$$⊢R\in \mathrm{Ring}\to \left(\exists g\in {\mathrm{Base}}_{R}a=\mathrm{RSpan}\left(R\right)\left(\left\{g\right\}\right)\to a\in U\right)$$
12	5 11	sylbid	$$⊢R\in \mathrm{Ring}\to \left(a\in P\to a\in U\right)$$
13	12	ssrdv	$$⊢R\in \mathrm{Ring}\to P\subseteq U$$