Metamath Proof Explorer

Theorem isdmn2

Description: The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Assertion isdmn2 ⊢ R ∈ Dmn ↔ R ∈ PrRing ∧ R ∈ CRingOps

Proof

Step Hyp Ref Expression
1 isdmn ⊢ R ∈ Dmn ↔ R ∈ PrRing ∧ R ∈ Com2
2 prrngorngo ⊢ R ∈ PrRing → R ∈ RingOps
3 iscrngo ⊢ R ∈ CRingOps ↔ R ∈ RingOps ∧ R ∈ Com2
4 3 baibr ⊢ R ∈ RingOps → R ∈ Com2 ↔ R ∈ CRingOps
5 2 4 syl ⊢ R ∈ PrRing → R ∈ Com2 ↔ R ∈ CRingOps
6 5 pm5.32i ⊢ R ∈ PrRing ∧ R ∈ Com2 ↔ R ∈ PrRing ∧ R ∈ CRingOps
7 1 6 bitri ⊢ R ∈ Dmn ↔ R ∈ PrRing ∧ R ∈ CRingOps