istrg

Description: Express the predicate " R is a topological ring". (Contributed by Mario Carneiro, 5-Oct-2015)

		Ref	Expression
	Hypothesis	istrg.1	$⊢ M = {mulGrp}_{R}$
	Assertion	istrg	$⊢ R \in TopRing \leftrightarrow (R \in TopGrp \land R \in Ring \land M \in TopMnd)$

Step	Hyp	Ref	Expression
1		istrg.1	$⊢ M = {mulGrp}_{R}$
2		elin	$⊢ R \in (TopGrp \cap Ring) \leftrightarrow (R \in TopGrp \land R \in Ring)$
3	2	anbi1i	$⊢ (R \in (TopGrp \cap Ring) \land M \in TopMnd) \leftrightarrow ((R \in TopGrp \land R \in Ring) \land M \in TopMnd)$
4		fveq2	$⊢ r = R \to {mulGrp}_{r} = {mulGrp}_{R}$
5	4 1	eqtr4di	$⊢ r = R \to {mulGrp}_{r} = M$
6	5	eleq1d	$⊢ r = R \to ({mulGrp}_{r} \in TopMnd \leftrightarrow M \in TopMnd)$
7		df-trg	$⊢ TopRing = \{r \in (TopGrp \cap Ring) \| {mulGrp}_{r} \in TopMnd\}$
8	6 7	elrab2	$⊢ R \in TopRing \leftrightarrow (R \in (TopGrp \cap Ring) \land M \in TopMnd)$
9		df-3an	$⊢ (R \in TopGrp \land R \in Ring \land M \in TopMnd) \leftrightarrow ((R \in TopGrp \land R \in Ring) \land M \in TopMnd)$
10	3 8 9	3bitr4i	$⊢ R \in TopRing \leftrightarrow (R \in TopGrp \land R \in Ring \land M \in TopMnd)$

Metamath Proof Explorer