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=BaseR
Assertion fiidomfld ⊢B∈Fin→R∈IDomn↔R∈Field

Proof

Step Hyp Ref Expression
1 fidomndrng.b ⊢B=BaseR
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