istdrg

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

	Ref	Expression
Hypotheses	istrg.1	$⊢ M = {mulGrp}_{R}$
	istdrg.1	$⊢ U = Unit (R)$
Assertion	istdrg	$⊢ R \in TopDRing \leftrightarrow (R \in TopRing \land R \in DivRing \land M ↾_{𝑠} U \in TopGrp)$

Step	Hyp	Ref	Expression
1		istrg.1	$⊢ M = {mulGrp}_{R}$
2		istdrg.1	$⊢ U = Unit (R)$
3		elin	$⊢ R \in (TopRing \cap DivRing) \leftrightarrow (R \in TopRing \land R \in DivRing)$
4	3	anbi1i	$⊢ (R \in (TopRing \cap DivRing) \land M ↾_{𝑠} U \in TopGrp) \leftrightarrow ((R \in TopRing \land R \in DivRing) \land M ↾_{𝑠} U \in TopGrp)$
5		fveq2	$⊢ r = R \to {mulGrp}_{r} = {mulGrp}_{R}$
6	5 1	eqtr4di	$⊢ r = R \to {mulGrp}_{r} = M$
7		fveq2	$⊢ r = R \to Unit (r) = Unit (R)$
8	7 2	eqtr4di	$⊢ r = R \to Unit (r) = U$
9	6 8	oveq12d	$⊢ r = R \to {mulGrp}_{r} ↾_{𝑠} Unit (r) = M ↾_{𝑠} U$
10	9	eleq1d	$⊢ r = R \to ({mulGrp}_{r} ↾_{𝑠} Unit (r) \in TopGrp \leftrightarrow M ↾_{𝑠} U \in TopGrp)$
11		df-tdrg	$⊢ TopDRing = \{r \in (TopRing \cap DivRing) \| {mulGrp}_{r} ↾_{𝑠} Unit (r) \in TopGrp\}$
12	10 11	elrab2	$⊢ R \in TopDRing \leftrightarrow (R \in (TopRing \cap DivRing) \land M ↾_{𝑠} U \in TopGrp)$
13		df-3an	$⊢ (R \in TopRing \land R \in DivRing \land M ↾_{𝑠} U \in TopGrp) \leftrightarrow ((R \in TopRing \land R \in DivRing) \land M ↾_{𝑠} U \in TopGrp)$
14	4 12 13	3bitr4i	$⊢ R \in TopDRing \leftrightarrow (R \in TopRing \land R \in DivRing \land M ↾_{𝑠} U \in TopGrp)$

Metamath Proof Explorer