subrgin

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

		Ref	Expression
	Assertion	subrgin	$⊢ (A \in SubRing (R) \land B \in SubRing (R)) \to A \cap B \in SubRing (R)$

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

Metamath Proof Explorer