Metamath Proof Explorer

Theorem istdrg

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

Ref Expression
Hypotheses istrg.1 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
istdrg.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion istdrg ( 𝑅 ∈ TopDRing ↔ ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ( 𝑀 ↾s 𝑈 ) ∈ TopGrp ) )

Proof

Step Hyp Ref Expression
1 istrg.1 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2 istdrg.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 elin ⊢ ( 𝑅 ∈ ( TopRing ∩ DivRing ) ↔ ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ) )
4 3 anbi1i ⊢ ( ( 𝑅 ∈ ( TopRing ∩ DivRing ) ∧ ( 𝑀 ↾s 𝑈 ) ∈ TopGrp ) ↔ ( ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑀 ↾s 𝑈 ) ∈ TopGrp ) )
5 fveq2 ⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) )
6 5 1 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = 𝑀 )
7 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = ( Unit ‘ 𝑅 ) )
8 7 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = 𝑈 )
9 6 8 oveq12d ⊢ ( 𝑟 = 𝑅 → ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) = ( 𝑀 ↾s 𝑈 ) )
10 9 eleq1d ⊢ ( 𝑟 = 𝑅 → ( ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) ∈ TopGrp ↔ ( 𝑀 ↾s 𝑈 ) ∈ TopGrp ) )
11 df-tdrg ⊢ TopDRing = { 𝑟 ∈ ( TopRing ∩ DivRing ) ∣ ( ( mulGrp ‘ 𝑟 ) ↾s ( Unit ‘ 𝑟 ) ) ∈ TopGrp }
12 10 11 elrab2 ⊢ ( 𝑅 ∈ TopDRing ↔ ( 𝑅 ∈ ( TopRing ∩ DivRing ) ∧ ( 𝑀 ↾s 𝑈 ) ∈ TopGrp ) )
13 df-3an ⊢ ( ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ( 𝑀 ↾s 𝑈 ) ∈ TopGrp ) ↔ ( ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ) ∧ ( 𝑀 ↾s 𝑈 ) ∈ TopGrp ) )
14 4 12 13 3bitr4i ⊢ ( 𝑅 ∈ TopDRing ↔ ( 𝑅 ∈ TopRing ∧ 𝑅 ∈ DivRing ∧ ( 𝑀 ↾s 𝑈 ) ∈ TopGrp ) )