Metamath Proof Explorer


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 ( 𝜑𝑅 ∈ Ring )
rgspnval.b ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
rgspnval.ss ( 𝜑𝐴𝐵 )
rgspnval.n ( 𝜑𝑁 = ( RingSpan ‘ 𝑅 ) )
rgspnval.sp ( 𝜑𝑈 = ( 𝑁𝐴 ) )
rgspnmin.sr ( 𝜑𝑆 ∈ ( SubRing ‘ 𝑅 ) )
rgspnmin.ss ( 𝜑𝐴𝑆 )
Assertion rgspnmin ( 𝜑𝑈𝑆 )

Proof

Step Hyp Ref Expression
1 rgspnval.r ( 𝜑𝑅 ∈ Ring )
2 rgspnval.b ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
3 rgspnval.ss ( 𝜑𝐴𝐵 )
4 rgspnval.n ( 𝜑𝑁 = ( RingSpan ‘ 𝑅 ) )
5 rgspnval.sp ( 𝜑𝑈 = ( 𝑁𝐴 ) )
6 rgspnmin.sr ( 𝜑𝑆 ∈ ( SubRing ‘ 𝑅 ) )
7 rgspnmin.ss ( 𝜑𝐴𝑆 )
8 1 2 3 4 5 rgspnval ( 𝜑𝑈 = { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } )
9 sseq2 ( 𝑡 = 𝑆 → ( 𝐴𝑡𝐴𝑆 ) )
10 9 elrab ( 𝑆 ∈ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } ↔ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐴𝑆 ) )
11 6 7 10 sylanbrc ( 𝜑𝑆 ∈ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } )
12 intss1 ( 𝑆 ∈ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } → { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } ⊆ 𝑆 )
13 11 12 syl ( 𝜑 { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴𝑡 } ⊆ 𝑆 )
14 8 13 eqsstrd ( 𝜑𝑈𝑆 )