Theorem rgspnid

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

	Ref	Expression
Hypotheses	rgspnid.r	|- ( ph -> R e. Ring )
	rgspnid.sr	|- ( ph -> A e. ( SubRing ` R ) )
	rgspnid.sp	|- ( ph -> S = ( ( RingSpan ` R ) ` A ) )
Assertion	rgspnid	|- ( ph -> S = A )

Proof

Step	Hyp	Ref	Expression
1		rgspnid.r	|- ( ph -> R e. Ring )
2		rgspnid.sr	|- ( ph -> A e. ( SubRing ` R ) )
3		rgspnid.sp	|- ( ph -> S = ( ( RingSpan ` R ) ` A ) )
4		eqidd	|- ( ph -> ( Base ` R ) = ( Base ` R ) )
5		eqid	|- ( Base ` R ) = ( Base ` R )
6	5	subrgss	|- ( A e. ( SubRing ` R ) -> A C_ ( Base ` R ) )
7	2 6	syl	|- ( ph -> A C_ ( Base ` R ) )
8		eqidd	|- ( ph -> ( RingSpan ` R ) = ( RingSpan ` R ) )
9		ssidd	|- ( ph -> A C_ A )
10	1 4 7 8 3 2 9	rgspnmin	|- ( ph -> S C_ A )
11	1 4 7 8 3	rgspnssid	|- ( ph -> A C_ S )
12	10 11	eqssd	|- ( ph -> S = A )