Theorem 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 e. TopRing <-> ( R e. TopGrp /\ R e. Ring /\ M e. TopMnd ) )

Proof

Step	Hyp	Ref	Expression
1		istrg.1	|- M = ( mulGrp ` R )
2		elin	|- ( R e. ( TopGrp i^i Ring ) <-> ( R e. TopGrp /\ R e. Ring ) )
3	2	anbi1i	|- ( ( R e. ( TopGrp i^i Ring ) /\ M e. TopMnd ) <-> ( ( R e. TopGrp /\ R e. Ring ) /\ M e. TopMnd ) )
4		fveq2	|- ( r = R -> ( mulGrp ` r ) = ( mulGrp ` R ) )
5	4 1	eqtr4di	|- ( r = R -> ( mulGrp ` r ) = M )
6	5	eleq1d	|- ( r = R -> ( ( mulGrp ` r ) e. TopMnd <-> M e. TopMnd ) )
7		df-trg	|- TopRing = { r e. ( TopGrp i^i Ring ) | ( mulGrp ` r ) e. TopMnd }
8	6 7	elrab2	|- ( R e. TopRing <-> ( R e. ( TopGrp i^i Ring ) /\ M e. TopMnd ) )
9		df-3an	|- ( ( R e. TopGrp /\ R e. Ring /\ M e. TopMnd ) <-> ( ( R e. TopGrp /\ R e. Ring ) /\ M e. TopMnd ) )
10	3 8 9	3bitr4i	|- ( R e. TopRing <-> ( R e. TopGrp /\ R e. Ring /\ M e. TopMnd ) )