Metamath Proof Explorer


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 ) )