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

Proof

Step Hyp Ref Expression
1 rgspnval.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
2 rgspnval.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
3 rgspnval.ss ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
4 rgspnval.n ⊢ ( 𝜑 → 𝑁 = ( RingSpan ‘ 𝑅 ) )
5 rgspnval.sp ⊢ ( 𝜑 → 𝑈 = ( 𝑁 ‘ 𝐴 ) )
6 1 2 3 4 5 rgspnval ⊢ ( 𝜑 → 𝑈 = ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } )
7 ssrab2 ⊢ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } ⊆ ( SubRing ‘ 𝑅 )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 8 subrgid ⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
10 1 9 syl ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
11 2 10 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑅 ) )
12 sseq2 ⊢ ( 𝑡 = 𝐵 → ( 𝐴 ⊆ 𝑡 ↔ 𝐴 ⊆ 𝐵 ) )
13 12 rspcev ⊢ ( ( 𝐵 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐴 ⊆ 𝐵 ) → ∃ 𝑡 ∈ ( SubRing ‘ 𝑅 ) 𝐴 ⊆ 𝑡 )
14 11 3 13 syl2anc ⊢ ( 𝜑 → ∃ 𝑡 ∈ ( SubRing ‘ 𝑅 ) 𝐴 ⊆ 𝑡 )
15 rabn0 ⊢ ( { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } ≠ ∅ ↔ ∃ 𝑡 ∈ ( SubRing ‘ 𝑅 ) 𝐴 ⊆ 𝑡 )
16 14 15 sylibr ⊢ ( 𝜑 → { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } ≠ ∅ )
17 subrgint ⊢ ( ( { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } ⊆ ( SubRing ‘ 𝑅 ) ∧ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } ≠ ∅ ) → ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } ∈ ( SubRing ‘ 𝑅 ) )
18 7 16 17 sylancr ⊢ ( 𝜑 → ∩ { 𝑡 ∈ ( SubRing ‘ 𝑅 ) ∣ 𝐴 ⊆ 𝑡 } ∈ ( SubRing ‘ 𝑅 ) )
19 6 18 eqeltrd ⊢ ( 𝜑 → 𝑈 ∈ ( SubRing ‘ 𝑅 ) )