Theorem istrg

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

	Ref	Expression
Hypothesis	istrg.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion	istrg	⊢ ( 𝑅 ∈ TopRing ↔ ( 𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ TopMnd ) )

Proof

Step	Hyp	Ref	Expression
1		istrg.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2		elin	⊢ ( 𝑅 ∈ ( TopGrp ∩ Ring ) ↔ ( 𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ) )
3	2	anbi1i	⊢ ( ( 𝑅 ∈ ( TopGrp ∩ Ring ) ∧ 𝑀 ∈ TopMnd ) ↔ ( ( 𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ TopMnd ) )
4		fveq2	⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) )
5	4 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = 𝑀 )
6	5	eleq1d	⊢ ( 𝑟 = 𝑅 → ( ( mulGrp ‘ 𝑟 ) ∈ TopMnd ↔ 𝑀 ∈ TopMnd ) )
7		df-trg	⊢ TopRing = { 𝑟 ∈ ( TopGrp ∩ Ring ) ∣ ( mulGrp ‘ 𝑟 ) ∈ TopMnd }
8	6 7	elrab2	⊢ ( 𝑅 ∈ TopRing ↔ ( 𝑅 ∈ ( TopGrp ∩ Ring ) ∧ 𝑀 ∈ TopMnd ) )
9		df-3an	⊢ ( ( 𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ TopMnd ) ↔ ( ( 𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ) ∧ 𝑀 ∈ TopMnd ) )
10	3 8 9	3bitr4i	⊢ ( 𝑅 ∈ TopRing ↔ ( 𝑅 ∈ TopGrp ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ TopMnd ) )