Theorem fldlring

Description: A field is a local ring. (Contributed by Thierry Arnoux, 3-Jun-2026) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	fldlring.1	$$⊢\phi \to F\in \mathrm{Field}$$
Assertion	fldlring	$$⊢\phi \to F\in \mathrm{LRing}$$

Proof

Step	Hyp	Ref	Expression
1		fldlring.1	$$⊢\phi \to F\in \mathrm{Field}$$
2	1	fldcrngd	$$⊢\phi \to F\in \mathrm{CRing}$$
3	1	flddrngd	$$⊢\phi \to F\in \mathrm{DivRing}$$
4		eqid	$$⊢0_F=0_F$$
5	4	drngmxidl	$$⊢F\in \mathrm{DivRing}\to \mathrm{MaxIdeal}\left(F\right)=\left\{\left\{0_F\right\}\right\}$$
6	3 5	syl	$$⊢\phi \to \mathrm{MaxIdeal}\left(F\right)=\left\{\left\{0_F\right\}\right\}$$
7		snex	$$⊢\left\{0_F\right\}\in \mathrm{V}$$
8	7	ensn1	$$⊢\left\{\left\{0_F\right\}\right\}\approx 1_{𝑜}$$
9	6 8	eqbrtrdi	$$⊢\phi \to \mathrm{MaxIdeal}\left(F\right)\approx 1_{𝑜}$$
10		dflring3	$$⊢F\in \mathrm{CRing}\to \left(F\in \mathrm{LRing}\leftrightarrow \mathrm{MaxIdeal}\left(F\right)\approx 1_{𝑜}\right)$$
11	10	biimpar	$$⊢\left(F\in \mathrm{CRing}\wedge \mathrm{MaxIdeal}\left(F\right)\approx 1_{𝑜}\right)\to F\in \mathrm{LRing}$$
12	2 9 11	syl2anc	$$⊢\phi \to F\in \mathrm{LRing}$$