Theorem rspsnid

Description: A principal ideal contains the element that generates it. (Contributed by Thierry Arnoux, 15-Jan-2024)

	Ref	Expression
Hypotheses	rspsnid.b	$$⊢B={\mathrm{Base}}_R$$
	rspsnid.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
Assertion	rspsnid	$$⊢\left(R\in \mathrm{Ring}\wedge G\in B\right)\to G\in K\left(\left\{G\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rspsnid.b	$$⊢B={\mathrm{Base}}_R$$
2		rspsnid.k	$$⊢K=\mathrm{RSpan}\left(R\right)$$
3		snssi	$$⊢G\in B\to \left\{G\right\}\subseteq B$$
4	2 1	rspssid	$$⊢\left(R\in \mathrm{Ring}\wedge \left\{G\right\}\subseteq B\right)\to \left\{G\right\}\subseteq K\left(\left\{G\right\}\right)$$
5	3 4	sylan2	$$⊢\left(R\in \mathrm{Ring}\wedge G\in B\right)\to \left\{G\right\}\subseteq K\left(\left\{G\right\}\right)$$
6		snssg	$$⊢G\in B\to \left(G\in K\left(\left\{G\right\}\right)\leftrightarrow \left\{G\right\}\subseteq K\left(\left\{G\right\}\right)\right)$$
7	6	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge G\in B\right)\to \left(G\in K\left(\left\{G\right\}\right)\leftrightarrow \left\{G\right\}\subseteq K\left(\left\{G\right\}\right)\right)$$
8	5 7	mpbird	$$⊢\left(R\in \mathrm{Ring}\wedge G\in B\right)\to G\in K\left(\left\{G\right\}\right)$$