This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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