Metamath Proof Explorer

Theorem sdrgint

Description: The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023)

		Ref	Expression
	Assertion	sdrgint	$⊢ (R \in DivRing \land S \subseteq SubDRing (R) \land S \neq \emptyset) \to ⋂ S \in SubDRing (R)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (R \in DivRing \land S \subseteq SubDRing (R) \land S \neq \emptyset) \to R \in DivRing$
2		simp2	$⊢ (R \in DivRing \land S \subseteq SubDRing (R) \land S \neq \emptyset) \to S \subseteq SubDRing (R)$
3		issdrg	$⊢ s \in SubDRing (R) \leftrightarrow (R \in DivRing \land s \in SubRing (R) \land R ↾_{𝑠} s \in DivRing)$
4	3	simp2bi	$⊢ s \in SubDRing (R) \to s \in SubRing (R)$
5	4	ssriv	$⊢ SubDRing (R) \subseteq SubRing (R)$
6	2 5	sstrdi	$⊢ (R \in DivRing \land S \subseteq SubDRing (R) \land S \neq \emptyset) \to S \subseteq SubRing (R)$
7		simp3	$⊢ (R \in DivRing \land S \subseteq SubDRing (R) \land S \neq \emptyset) \to S \neq \emptyset$
8		subrgint	$⊢ (S \subseteq SubRing (R) \land S \neq \emptyset) \to ⋂ S \in SubRing (R)$
9	6 7 8	syl2anc	$⊢ (R \in DivRing \land S \subseteq SubDRing (R) \land S \neq \emptyset) \to ⋂ S \in SubRing (R)$
10		eqid	$⊢ R ↾_{𝑠} ⋂ S = R ↾_{𝑠} ⋂ S$
11	2	sselda	$⊢ ((R \in DivRing \land S \subseteq SubDRing (R) \land S \neq \emptyset) \land s \in S) \to s \in SubDRing (R)$
12	3	simp3bi	$⊢ s \in SubDRing (R) \to R ↾_{𝑠} s \in DivRing$
13	11 12	syl	$⊢ ((R \in DivRing \land S \subseteq SubDRing (R) \land S \neq \emptyset) \land s \in S) \to R ↾_{𝑠} s \in DivRing$
14	10 1 6 7 13	subdrgint	$⊢ (R \in DivRing \land S \subseteq SubDRing (R) \land S \neq \emptyset) \to R ↾_{𝑠} ⋂ S \in DivRing$
15		issdrg	$⊢ ⋂ S \in SubDRing (R) \leftrightarrow (R \in DivRing \land ⋂ S \in SubRing (R) \land R ↾_{𝑠} ⋂ S \in DivRing)$
16	1 9 14 15	syl3anbrc	$⊢ (R \in DivRing \land S \subseteq SubDRing (R) \land S \neq \emptyset) \to ⋂ S \in SubDRing (R)$