Theorem fiidomfld

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

	Ref	Expression
Hypothesis	fidomndrng.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	fiidomfld	⊢ ( 𝐵 ∈ Fin → ( 𝑅 ∈ IDomn ↔ 𝑅 ∈ Field ) )

Proof

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