This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )