drnglring

Description: A division ring is a local ring. (Contributed by Thierry Arnoux, 2-Jun-2026)

		Ref	Expression
	Hypothesis	drnglring.1	$⊢ φ \to F \in DivRing$
	Assertion	drnglring	$⊢ φ \to F \in LRing$

Proof

Step	Hyp	Ref	Expression
1		drnglring.1	$⊢ φ \to F \in DivRing$
2		drngnzr	$⊢ F \in DivRing \to F \in NzRing$
3	1 2	syl	$⊢ φ \to F \in NzRing$
4	1	ad4antr	$⊢ ((((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \land \neg x = 0_{F}) \to F \in DivRing$
5		simp-4r	$⊢ ((((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \land \neg x = 0_{F}) \to x \in {Base}_{F}$
6		neqne	$⊢ \neg x = 0_{F} \to x \neq 0_{F}$
7	6	adantl	$⊢ ((((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \land \neg x = 0_{F}) \to x \neq 0_{F}$
8		eqid	$⊢ {Base}_{F} = {Base}_{F}$
9		eqid	$⊢ Unit (F) = Unit (F)$
10		eqid	$⊢ 0_{F} = 0_{F}$
11	8 9 10	drngunit	$⊢ F \in DivRing \to (x \in Unit (F) \leftrightarrow (x \in {Base}_{F} \land x \neq 0_{F}))$
12	11	biimpar	$⊢ (F \in DivRing \land (x \in {Base}_{F} \land x \neq 0_{F})) \to x \in Unit (F)$
13	4 5 7 12	syl12anc	$⊢ ((((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \land \neg x = 0_{F}) \to x \in Unit (F)$
14	1	ad4antr	$⊢ ((((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \land \neg y = 0_{F}) \to F \in DivRing$
15		simpllr	$⊢ ((((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \land \neg y = 0_{F}) \to y \in {Base}_{F}$
16		neqne	$⊢ \neg y = 0_{F} \to y \neq 0_{F}$
17	16	adantl	$⊢ ((((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \land \neg y = 0_{F}) \to y \neq 0_{F}$
18	8 9 10	drngunit	$⊢ F \in DivRing \to (y \in Unit (F) \leftrightarrow (y \in {Base}_{F} \land y \neq 0_{F}))$
19	18	biimpar	$⊢ (F \in DivRing \land (y \in {Base}_{F} \land y \neq 0_{F})) \to y \in Unit (F)$
20	14 15 17 19	syl12anc	$⊢ ((((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \land \neg y = 0_{F}) \to y \in Unit (F)$
21		simplll	$⊢ (((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \to φ$
22		simpr	$⊢ (((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \to x +_{F} y = 1_{F}$
23		eqid	$⊢ 1_{F} = 1_{F}$
24	23 10	nzrnz	$⊢ F \in NzRing \to 1_{F} \neq 0_{F}$
25	3 24	syl	$⊢ φ \to 1_{F} \neq 0_{F}$
26	25	ad3antrrr	$⊢ (((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \to 1_{F} \neq 0_{F}$
27	22 26	eqnetrd	$⊢ (((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \to x +_{F} y \neq 0_{F}$
28	27	neneqd	$⊢ (((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \to \neg x +_{F} y = 0_{F}$
29		oveq12	$⊢ (x = 0_{F} \land y = 0_{F}) \to x +_{F} y = 0_{F} +_{F} 0_{F}$
30	29	adantl	$⊢ (φ \land (x = 0_{F} \land y = 0_{F})) \to x +_{F} y = 0_{F} +_{F} 0_{F}$
31		eqid	$⊢ +_{F} = +_{F}$
32	1	drnggrpd	$⊢ φ \to F \in Grp$
33	32	adantr	$⊢ (φ \land (x = 0_{F} \land y = 0_{F})) \to F \in Grp$
34	8 10 33	grpidcld	$⊢ (φ \land (x = 0_{F} \land y = 0_{F})) \to 0_{F} \in {Base}_{F}$
35	8 31 10 33 34	grplidd	$⊢ (φ \land (x = 0_{F} \land y = 0_{F})) \to 0_{F} +_{F} 0_{F} = 0_{F}$
36	30 35	eqtrd	$⊢ (φ \land (x = 0_{F} \land y = 0_{F})) \to x +_{F} y = 0_{F}$
37	36	stoic1a	$⊢ (φ \land \neg x +_{F} y = 0_{F}) \to \neg (x = 0_{F} \land y = 0_{F})$
38	21 28 37	syl2anc	$⊢ (((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \to \neg (x = 0_{F} \land y = 0_{F})$
39		ianor	$⊢ \neg (x = 0_{F} \land y = 0_{F}) \leftrightarrow (\neg x = 0_{F} \lor \neg y = 0_{F})$
40	38 39	sylib	$⊢ (((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \to (\neg x = 0_{F} \lor \neg y = 0_{F})$
41	13 20 40	orim12da	$⊢ (((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \land x +_{F} y = 1_{F}) \to (x \in Unit (F) \lor y \in Unit (F))$
42	41	ex	$⊢ ((φ \land x \in {Base}_{F}) \land y \in {Base}_{F}) \to (x +_{F} y = 1_{F} \to (x \in Unit (F) \lor y \in Unit (F)))$
43	42	anasss	$⊢ (φ \land (x \in {Base}_{F} \land y \in {Base}_{F})) \to (x +_{F} y = 1_{F} \to (x \in Unit (F) \lor y \in Unit (F)))$
44	43	ralrimivva	$⊢ φ \to \forall x \in {Base}_{F} \forall y \in {Base}_{F} (x +_{F} y = 1_{F} \to (x \in Unit (F) \lor y \in Unit (F)))$
45	8 31 23 9	islring	$⊢ F \in LRing \leftrightarrow (F \in NzRing \land \forall x \in {Base}_{F} \forall y \in {Base}_{F} (x +_{F} y = 1_{F} \to (x \in Unit (F) \lor y \in Unit (F))))$
46	3 44 45	sylanbrc	$⊢ φ \to F \in LRing$

Metamath Proof Explorer

Theorem drnglring

Proof