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	|- ( ph -> F e. Field )
Assertion	fldlring	|- ( ph -> F e. LRing )

Proof

Step	Hyp	Ref	Expression
1		fldlring.1	|- ( ph -> F e. Field )
2	1	fldcrngd	|- ( ph -> F e. CRing )
3	1	flddrngd	|- ( ph -> F e. DivRing )
4		eqid	|- ( 0g ` F ) = ( 0g ` F )
5	4	drngmxidl	|- ( F e. DivRing -> ( MaxIdeal ` F ) = { { ( 0g ` F ) } } )
6	3 5	syl	|- ( ph -> ( MaxIdeal ` F ) = { { ( 0g ` F ) } } )
7		snex	|- { ( 0g ` F ) } e. _V
8	7	ensn1	|- { { ( 0g ` F ) } } ~~ 1o
9	6 8	eqbrtrdi	|- ( ph -> ( MaxIdeal ` F ) ~~ 1o )
10		dflring3	|- ( F e. CRing -> ( F e. LRing <-> ( MaxIdeal ` F ) ~~ 1o ) )
11	10	biimpar	|- ( ( F e. CRing /\ ( MaxIdeal ` F ) ~~ 1o ) -> F e. LRing )
12	2 9 11	syl2anc	|- ( ph -> F e. LRing )