subrgint

Description: The intersection of a nonempty collection of subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014) (Revised by Mario Carneiro, 7-Dec-2014)

		Ref	Expression
	Assertion	subrgint	$⊢ (S \subseteq SubRing (R) \land S \neq \emptyset) \to ⋂ S \in SubRing (R)$

Proof

Step	Hyp	Ref	Expression
1		subrgsubg	$⊢ r \in SubRing (R) \to r \in SubGrp (R)$
2	1	ssriv	$⊢ SubRing (R) \subseteq SubGrp (R)$
3		sstr	$⊢ (S \subseteq SubRing (R) \land SubRing (R) \subseteq SubGrp (R)) \to S \subseteq SubGrp (R)$
4	2 3	mpan2	$⊢ S \subseteq SubRing (R) \to S \subseteq SubGrp (R)$
5		subgint	$⊢ (S \subseteq SubGrp (R) \land S \neq \emptyset) \to ⋂ S \in SubGrp (R)$
6	4 5	sylan	$⊢ (S \subseteq SubRing (R) \land S \neq \emptyset) \to ⋂ S \in SubGrp (R)$
7		ssel2	$⊢ (S \subseteq SubRing (R) \land r \in S) \to r \in SubRing (R)$
8	7	adantlr	$⊢ ((S \subseteq SubRing (R) \land S \neq \emptyset) \land r \in S) \to r \in SubRing (R)$
9		eqid	$⊢ 1_{R} = 1_{R}$
10	9	subrg1cl	$⊢ r \in SubRing (R) \to 1_{R} \in r$
11	8 10	syl	$⊢ ((S \subseteq SubRing (R) \land S \neq \emptyset) \land r \in S) \to 1_{R} \in r$
12	11	ralrimiva	$⊢ (S \subseteq SubRing (R) \land S \neq \emptyset) \to \forall r \in S 1_{R} \in r$
13		fvex	$⊢ 1_{R} \in V$
14	13	elint2	$⊢ 1_{R} \in ⋂ S \leftrightarrow \forall r \in S 1_{R} \in r$
15	12 14	sylibr	$⊢ (S \subseteq SubRing (R) \land S \neq \emptyset) \to 1_{R} \in ⋂ S$
16	8	adantlr	$⊢ (((S \subseteq SubRing (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \land r \in S) \to r \in SubRing (R)$
17		simprl	$⊢ ((S \subseteq SubRing (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \to x \in ⋂ S$
18		elinti	$⊢ x \in ⋂ S \to (r \in S \to x \in r)$
19	18	imp	$⊢ (x \in ⋂ S \land r \in S) \to x \in r$
20	17 19	sylan	$⊢ (((S \subseteq SubRing (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \land r \in S) \to x \in r$
21		simprr	$⊢ ((S \subseteq SubRing (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \to y \in ⋂ S$
22		elinti	$⊢ y \in ⋂ S \to (r \in S \to y \in r)$
23	22	imp	$⊢ (y \in ⋂ S \land r \in S) \to y \in r$
24	21 23	sylan	$⊢ (((S \subseteq SubRing (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \land r \in S) \to y \in r$
25		eqid	$⊢ \cdot_{R} = \cdot_{R}$
26	25	subrgmcl	$⊢ (r \in SubRing (R) \land x \in r \land y \in r) \to x \cdot_{R} y \in r$
27	16 20 24 26	syl3anc	$⊢ (((S \subseteq SubRing (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \land r \in S) \to x \cdot_{R} y \in r$
28	27	ralrimiva	$⊢ ((S \subseteq SubRing (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \to \forall r \in S x \cdot_{R} y \in r$
29		ovex	$⊢ x \cdot_{R} y \in V$
30	29	elint2	$⊢ x \cdot_{R} y \in ⋂ S \leftrightarrow \forall r \in S x \cdot_{R} y \in r$
31	28 30	sylibr	$⊢ ((S \subseteq SubRing (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \to x \cdot_{R} y \in ⋂ S$
32	31	ralrimivva	$⊢ (S \subseteq SubRing (R) \land S \neq \emptyset) \to \forall x \in ⋂ S \forall y \in ⋂ S x \cdot_{R} y \in ⋂ S$
33		ssn0	$⊢ (S \subseteq SubRing (R) \land S \neq \emptyset) \to SubRing (R) \neq \emptyset$
34		n0	$⊢ SubRing (R) \neq \emptyset \leftrightarrow \exists r r \in SubRing (R)$
35		subrgrcl	$⊢ r \in SubRing (R) \to R \in Ring$
36	35	exlimiv	$⊢ \exists r r \in SubRing (R) \to R \in Ring$
37	34 36	sylbi	$⊢ SubRing (R) \neq \emptyset \to R \in Ring$
38		eqid	$⊢ {Base}_{R} = {Base}_{R}$
39	38 9 25	issubrg2	$⊢ R \in Ring \to (⋂ S \in SubRing (R) \leftrightarrow (⋂ S \in SubGrp (R) \land 1_{R} \in ⋂ S \land \forall x \in ⋂ S \forall y \in ⋂ S x \cdot_{R} y \in ⋂ S))$
40	33 37 39	3syl	$⊢ (S \subseteq SubRing (R) \land S \neq \emptyset) \to (⋂ S \in SubRing (R) \leftrightarrow (⋂ S \in SubGrp (R) \land 1_{R} \in ⋂ S \land \forall x \in ⋂ S \forall y \in ⋂ S x \cdot_{R} y \in ⋂ S))$
41	6 15 32 40	mpbir3and	$⊢ (S \subseteq SubRing (R) \land S \neq \emptyset) \to ⋂ S \in SubRing (R)$

Metamath Proof Explorer

Theorem subrgint

Proof