subrngint

Description: The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		subrngsubg	$⊢ r \in SubRng (R) \to r \in SubGrp (R)$
2	1	ssriv	$⊢ SubRng (R) \subseteq SubGrp (R)$
3		sstr	$⊢ (S \subseteq SubRng (R) \land SubRng (R) \subseteq SubGrp (R)) \to S \subseteq SubGrp (R)$
4	2 3	mpan2	$⊢ S \subseteq SubRng (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 SubRng (R) \land S \neq \emptyset) \to ⋂ S \in SubGrp (R)$
7		ssel2	$⊢ (S \subseteq SubRng (R) \land r \in S) \to r \in SubRng (R)$
8	7	ad4ant14	$⊢ (((S \subseteq SubRng (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \land r \in S) \to r \in SubRng (R)$
9		simprl	$⊢ ((S \subseteq SubRng (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \to x \in ⋂ S$
10		elinti	$⊢ x \in ⋂ S \to (r \in S \to x \in r)$
11	10	imp	$⊢ (x \in ⋂ S \land r \in S) \to x \in r$
12	9 11	sylan	$⊢ (((S \subseteq SubRng (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \land r \in S) \to x \in r$
13		simprr	$⊢ ((S \subseteq SubRng (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \to y \in ⋂ S$
14		elinti	$⊢ y \in ⋂ S \to (r \in S \to y \in r)$
15	14	imp	$⊢ (y \in ⋂ S \land r \in S) \to y \in r$
16	13 15	sylan	$⊢ (((S \subseteq SubRng (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \land r \in S) \to y \in r$
17		eqid	$⊢ \cdot_{R} = \cdot_{R}$
18	17	subrngmcl	$⊢ (r \in SubRng (R) \land x \in r \land y \in r) \to x \cdot_{R} y \in r$
19	8 12 16 18	syl3anc	$⊢ (((S \subseteq SubRng (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \land r \in S) \to x \cdot_{R} y \in r$
20	19	ralrimiva	$⊢ ((S \subseteq SubRng (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \to \forall r \in S x \cdot_{R} y \in r$
21		ovex	$⊢ x \cdot_{R} y \in V$
22	21	elint2	$⊢ x \cdot_{R} y \in ⋂ S \leftrightarrow \forall r \in S x \cdot_{R} y \in r$
23	20 22	sylibr	$⊢ ((S \subseteq SubRng (R) \land S \neq \emptyset) \land (x \in ⋂ S \land y \in ⋂ S)) \to x \cdot_{R} y \in ⋂ S$
24	23	ralrimivva	$⊢ (S \subseteq SubRng (R) \land S \neq \emptyset) \to \forall x \in ⋂ S \forall y \in ⋂ S x \cdot_{R} y \in ⋂ S$
25		ssn0	$⊢ (S \subseteq SubRng (R) \land S \neq \emptyset) \to SubRng (R) \neq \emptyset$
26		n0	$⊢ SubRng (R) \neq \emptyset \leftrightarrow \exists r r \in SubRng (R)$
27		subrngrcl	$⊢ r \in SubRng (R) \to R \in Rng$
28	27	exlimiv	$⊢ \exists r r \in SubRng (R) \to R \in Rng$
29	26 28	sylbi	$⊢ SubRng (R) \neq \emptyset \to R \in Rng$
30		eqid	$⊢ {Base}_{R} = {Base}_{R}$
31	30 17	issubrng2	$⊢ R \in Rng \to (⋂ S \in SubRng (R) \leftrightarrow (⋂ S \in SubGrp (R) \land \forall x \in ⋂ S \forall y \in ⋂ S x \cdot_{R} y \in ⋂ S))$
32	25 29 31	3syl	$⊢ (S \subseteq SubRng (R) \land S \neq \emptyset) \to (⋂ S \in SubRng (R) \leftrightarrow (⋂ S \in SubGrp (R) \land \forall x \in ⋂ S \forall y \in ⋂ S x \cdot_{R} y \in ⋂ S))$
33	6 24 32	mpbir2and	$⊢ (S \subseteq SubRng (R) \land S \neq \emptyset) \to ⋂ S \in SubRng (R)$

Metamath Proof Explorer

Theorem subrngint

Proof