Theorem rgspnmin

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

	Ref	Expression
Hypotheses	rgspnval.r	|- ( ph -> R e. Ring )
	rgspnval.b	|- ( ph -> B = ( Base ` R ) )
	rgspnval.ss	|- ( ph -> A C_ B )
	rgspnval.n	|- ( ph -> N = ( RingSpan ` R ) )
	rgspnval.sp	|- ( ph -> U = ( N ` A ) )
	rgspnmin.sr	|- ( ph -> S e. ( SubRing ` R ) )
	rgspnmin.ss	|- ( ph -> A C_ S )
Assertion	rgspnmin	|- ( ph -> U C_ S )

Proof

Step	Hyp	Ref	Expression
1		rgspnval.r	|- ( ph -> R e. Ring )
2		rgspnval.b	|- ( ph -> B = ( Base ` R ) )
3		rgspnval.ss	|- ( ph -> A C_ B )
4		rgspnval.n	|- ( ph -> N = ( RingSpan ` R ) )
5		rgspnval.sp	|- ( ph -> U = ( N ` A ) )
6		rgspnmin.sr	|- ( ph -> S e. ( SubRing ` R ) )
7		rgspnmin.ss	|- ( ph -> A C_ S )
8	1 2 3 4 5	rgspnval	|- ( ph -> U = |^| { t e. ( SubRing ` R ) | A C_ t } )
9		sseq2	|- ( t = S -> ( A C_ t <-> A C_ S ) )
10	9	elrab	|- ( S e. { t e. ( SubRing ` R ) | A C_ t } <-> ( S e. ( SubRing ` R ) /\ A C_ S ) )
11	6 7 10	sylanbrc	|- ( ph -> S e. { t e. ( SubRing ` R ) | A C_ t } )
12		intss1	|- ( S e. { t e. ( SubRing ` R ) | A C_ t } -> |^| { t e. ( SubRing ` R ) | A C_ t } C_ S )
13	11 12	syl	|- ( ph -> |^| { t e. ( SubRing ` R ) | A C_ t } C_ S )
14	8 13	eqsstrd	|- ( ph -> U C_ S )