subrngin

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

		Ref	Expression
	Assertion	subrngin	$⊢ (A \in SubRng (R) \land B \in SubRng (R)) \to A \cap B \in SubRng (R)$

Step	Hyp	Ref	Expression
1		intprg	$⊢ (A \in SubRng (R) \land B \in SubRng (R)) \to ⋂ \{A, B\} = A \cap B$
2		prssi	$⊢ (A \in SubRng (R) \land B \in SubRng (R)) \to \{A, B\} \subseteq SubRng (R)$
3		prnzg	$⊢ A \in SubRng (R) \to \{A, B\} \neq \emptyset$
4	3	adantr	$⊢ (A \in SubRng (R) \land B \in SubRng (R)) \to \{A, B\} \neq \emptyset$
5		subrngint	$⊢ (\{A, B\} \subseteq SubRng (R) \land \{A, B\} \neq \emptyset) \to ⋂ \{A, B\} \in SubRng (R)$
6	2 4 5	syl2anc	$⊢ (A \in SubRng (R) \land B \in SubRng (R)) \to ⋂ \{A, B\} \in SubRng (R)$
7	1 6	eqeltrrd	$⊢ (A \in SubRng (R) \land B \in SubRng (R)) \to A \cap B \in SubRng (R)$

Metamath Proof Explorer