rgspncl

Description: The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014)

Step	Hyp	Ref	Expression
1		rgspnval.r	$⊢ φ \to R \in Ring$
2		rgspnval.b	$⊢ φ \to B = {Base}_{R}$
3		rgspnval.ss	$⊢ φ \to A \subseteq B$
4		rgspnval.n	$⊢ φ \to N = RingSpan (R)$
5		rgspnval.sp	$⊢ φ \to U = N (A)$
6	1 2 3 4 5	rgspnval	$⊢ φ \to U = ⋂ \{t \in SubRing (R) \| A \subseteq t\}$
7		ssrab2	$⊢ \{t \in SubRing (R) \| A \subseteq t\} \subseteq SubRing (R)$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9	8	subrgid	$⊢ R \in Ring \to {Base}_{R} \in SubRing (R)$
10	1 9	syl	$⊢ φ \to {Base}_{R} \in SubRing (R)$
11	2 10	eqeltrd	$⊢ φ \to B \in SubRing (R)$
12		sseq2	$⊢ t = B \to (A \subseteq t \leftrightarrow A \subseteq B)$
13	12	rspcev	$⊢ (B \in SubRing (R) \land A \subseteq B) \to \exists t \in SubRing (R) A \subseteq t$
14	11 3 13	syl2anc	$⊢ φ \to \exists t \in SubRing (R) A \subseteq t$
15		rabn0	$⊢ \{t \in SubRing (R) \| A \subseteq t\} \neq \emptyset \leftrightarrow \exists t \in SubRing (R) A \subseteq t$
16	14 15	sylibr	$⊢ φ \to \{t \in SubRing (R) \| A \subseteq t\} \neq \emptyset$
17		subrgint	$⊢ (\{t \in SubRing (R) \| A \subseteq t\} \subseteq SubRing (R) \land \{t \in SubRing (R) \| A \subseteq t\} \neq \emptyset) \to ⋂ \{t \in SubRing (R) \| A \subseteq t\} \in SubRing (R)$
18	7 16 17	sylancr	$⊢ φ \to ⋂ \{t \in SubRing (R) \| A \subseteq t\} \in SubRing (R)$
19	6 18	eqeltrd	$⊢ φ \to U \in SubRing (R)$

Metamath Proof Explorer