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 ⊢ M = mulGrp R
Assertion istrg ⊢ R ∈ TopRing ↔ R ∈ TopGrp ∧ R ∈ Ring ∧ M ∈ TopMnd

Proof

Step Hyp Ref Expression
1 istrg.1 ⊢ M = mulGrp R
2 elin ⊢ R ∈ TopGrp ∩ Ring ↔ R ∈ TopGrp ∧ R ∈ Ring
3 2 anbi1i ⊢ R ∈ TopGrp ∩ Ring ∧ M ∈ TopMnd ↔ R ∈ TopGrp ∧ R ∈ Ring ∧ M ∈ 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 ∈ TopMnd ↔ M ∈ TopMnd
7 df-trg ⊢ TopRing = r ∈ TopGrp ∩ Ring | mulGrp r ∈ TopMnd
8 6 7 elrab2 ⊢ R ∈ TopRing ↔ R ∈ TopGrp ∩ Ring ∧ M ∈ TopMnd
9 df-3an ⊢ R ∈ TopGrp ∧ R ∈ Ring ∧ M ∈ TopMnd ↔ R ∈ TopGrp ∧ R ∈ Ring ∧ M ∈ TopMnd
10 3 8 9 3bitr4i ⊢ R ∈ TopRing ↔ R ∈ TopGrp ∧ R ∈ Ring ∧ M ∈ TopMnd