Theorem rgspnid

Description: The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014)

	Ref	Expression
Hypotheses	rgspnid.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	rgspnid.sr	$$⊢\phi \to A\in \mathrm{SubRing}\left(R\right)$$
	rgspnid.sp	$$⊢\phi \to S=\mathrm{RingSpan}\left(R\right)\left(A\right)$$
Assertion	rgspnid	$$⊢\phi \to S=A$$

Proof

Step	Hyp	Ref	Expression
1		rgspnid.r	$$⊢\phi \to R\in \mathrm{Ring}$$
2		rgspnid.sr	$$⊢\phi \to A\in \mathrm{SubRing}\left(R\right)$$
3		rgspnid.sp	$$⊢\phi \to S=\mathrm{RingSpan}\left(R\right)\left(A\right)$$
4		eqidd	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_R$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6	5	subrgss	$$⊢A\in \mathrm{SubRing}\left(R\right)\to A\subseteq {\mathrm{Base}}_R$$
7	2 6	syl	$$⊢\phi \to A\subseteq {\mathrm{Base}}_R$$
8		eqidd	$$⊢\phi \to \mathrm{RingSpan}\left(R\right)=\mathrm{RingSpan}\left(R\right)$$
9		ssidd	$$⊢\phi \to A\subseteq A$$
10	1 4 7 8 3 2 9	rgspnmin	$$⊢\phi \to S\subseteq A$$
11	1 4 7 8 3	rgspnssid	$$⊢\phi \to A\subseteq S$$
12	10 11	eqssd	$$⊢\phi \to S=A$$