Theorem rgspncl

Description: The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-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 ) )
Assertion	rgspncl	|- ( ph -> U e. ( SubRing ` R ) )

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	1 2 3 4 5	rgspnval	|- ( ph -> U = |^| { t e. ( SubRing ` R ) | A C_ t } )
7		ssrab2	|- { t e. ( SubRing ` R ) | A C_ t } C_ ( SubRing ` R )
8		eqid	|- ( Base ` R ) = ( Base ` R )
9	8	subrgid	|- ( R e. Ring -> ( Base ` R ) e. ( SubRing ` R ) )
10	1 9	syl	|- ( ph -> ( Base ` R ) e. ( SubRing ` R ) )
11	2 10	eqeltrd	|- ( ph -> B e. ( SubRing ` R ) )
12		sseq2	|- ( t = B -> ( A C_ t <-> A C_ B ) )
13	12	rspcev	|- ( ( B e. ( SubRing ` R ) /\ A C_ B ) -> E. t e. ( SubRing ` R ) A C_ t )
14	11 3 13	syl2anc	|- ( ph -> E. t e. ( SubRing ` R ) A C_ t )
15		rabn0	|- ( { t e. ( SubRing ` R ) | A C_ t } =/= (/) <-> E. t e. ( SubRing ` R ) A C_ t )
16	14 15	sylibr	|- ( ph -> { t e. ( SubRing ` R ) | A C_ t } =/= (/) )
17		subrgint	|- ( ( { t e. ( SubRing ` R ) | A C_ t } C_ ( SubRing ` R ) /\ { t e. ( SubRing ` R ) | A C_ t } =/= (/) ) -> |^| { t e. ( SubRing ` R ) | A C_ t } e. ( SubRing ` R ) )
18	7 16 17	sylancr	|- ( ph -> |^| { t e. ( SubRing ` R ) | A C_ t } e. ( SubRing ` R ) )
19	6 18	eqeltrd	|- ( ph -> U e. ( SubRing ` R ) )