Theorem rgspnmin

Description: The ring-span is contained in all subrings which contain all the generators. (Contributed by Stefan O'Rear, 30-Nov-2014)

	Ref	Expression
Hypotheses	rgspnval.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	rgspnval.b	$$⊢\phi \to B={\mathrm{Base}}_R$$
	rgspnval.ss	$$⊢\phi \to A\subseteq B$$
	rgspnval.n	$$⊢\phi \to N=\mathrm{RingSpan}\left(R\right)$$
	rgspnval.sp	$$⊢\phi \to U=N\left(A\right)$$
	rgspnmin.sr	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
	rgspnmin.ss	$$⊢\phi \to A\subseteq S$$
Assertion	rgspnmin	$$⊢\phi \to U\subseteq S$$

Proof

Step	Hyp	Ref	Expression
1		rgspnval.r	$$⊢\phi \to R\in \mathrm{Ring}$$
2		rgspnval.b	$$⊢\phi \to B={\mathrm{Base}}_R$$
3		rgspnval.ss	$$⊢\phi \to A\subseteq B$$
4		rgspnval.n	$$⊢\phi \to N=\mathrm{RingSpan}\left(R\right)$$
5		rgspnval.sp	$$⊢\phi \to U=N\left(A\right)$$
6		rgspnmin.sr	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
7		rgspnmin.ss	$$⊢\phi \to A\subseteq S$$
8	1 2 3 4 5	rgspnval	$$⊢\phi \to U=\bigcap \left\{t\in \mathrm{SubRing}\left(R\right)|A\subseteq t\right\}$$
9		sseq2	$$⊢t=S\to \left(A\subseteq t\leftrightarrow A\subseteq S\right)$$
10	9	elrab	$$⊢S\in \left\{t\in \mathrm{SubRing}\left(R\right)|A\subseteq t\right\}\leftrightarrow \left(S\in \mathrm{SubRing}\left(R\right)\wedge A\subseteq S\right)$$
11	6 7 10	sylanbrc	$$⊢\phi \to S\in \left\{t\in \mathrm{SubRing}\left(R\right)|A\subseteq t\right\}$$
12		intss1	$$⊢S\in \left\{t\in \mathrm{SubRing}\left(R\right)|A\subseteq t\right\}\to \bigcap \left\{t\in \mathrm{SubRing}\left(R\right)|A\subseteq t\right\}\subseteq S$$
13	11 12	syl	$$⊢\phi \to \bigcap \left\{t\in \mathrm{SubRing}\left(R\right)|A\subseteq t\right\}\subseteq S$$
14	8 13	eqsstrd	$$⊢\phi \to U\subseteq S$$