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

Metamath Proof Explorer

Theorem rgspnmin

Description: The ring-span is contained in all subrings 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 ⊢ ( 𝜑 → 𝑈 ⊆ 𝑆 )