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