Metamath Proof Explorer

Theorem fiidomfld

Description: A finite integral domain is a field. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Hypothesis fidomndrng.b ⊢ B = Base R
Assertion fiidomfld ⊢ B ∈ Fin → R ∈ IDomn ↔ R ∈ Field

Proof

Step Hyp Ref Expression
1 fidomndrng.b ⊢ B = Base R
2 1 fidomndrng ⊢ B ∈ Fin → R ∈ Domn ↔ R ∈ DivRing
3 2 anbi2d ⊢ B ∈ Fin → R ∈ CRing ∧ R ∈ Domn ↔ R ∈ CRing ∧ R ∈ DivRing
4 isidom ⊢ R ∈ IDomn ↔ R ∈ CRing ∧ R ∈ Domn
5 isfld ⊢ R ∈ Field ↔ R ∈ DivRing ∧ R ∈ CRing
6 5 biancomi ⊢ R ∈ Field ↔ R ∈ CRing ∧ R ∈ DivRing
7 3 4 6 3bitr4g ⊢ B ∈ Fin → R ∈ IDomn ↔ R ∈ Field