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	⊢ ( 𝜑 → 𝐹 ∈ Field )
Assertion	fldlring	⊢ ( 𝜑 → 𝐹 ∈ LRing )

Proof

Step	Hyp	Ref	Expression
1		fldlring.1	⊢ ( 𝜑 → 𝐹 ∈ Field )
2	1	fldcrngd	⊢ ( 𝜑 → 𝐹 ∈ CRing )
3	1	flddrngd	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
4		eqid	⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
5	4	drngmxidl	⊢ ( 𝐹 ∈ DivRing → ( MaxIdeal ‘ 𝐹 ) = { { ( 0g ‘ 𝐹 ) } } )
6	3 5	syl	⊢ ( 𝜑 → ( MaxIdeal ‘ 𝐹 ) = { { ( 0g ‘ 𝐹 ) } } )
7		snex	⊢ { ( 0g ‘ 𝐹 ) } ∈ V
8	7	ensn1	⊢ { { ( 0g ‘ 𝐹 ) } } ≈ 1o
9	6 8	eqbrtrdi	⊢ ( 𝜑 → ( MaxIdeal ‘ 𝐹 ) ≈ 1o )
10		dflring3	⊢ ( 𝐹 ∈ CRing → ( 𝐹 ∈ LRing ↔ ( MaxIdeal ‘ 𝐹 ) ≈ 1o ) )
11	10	biimpar	⊢ ( ( 𝐹 ∈ CRing ∧ ( MaxIdeal ‘ 𝐹 ) ≈ 1o ) → 𝐹 ∈ LRing )
12	2 9 11	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ LRing )