Theorem drnglring

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

	Ref	Expression
Hypothesis	drnglring.1	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
Assertion	drnglring	⊢ ( 𝜑 → 𝐹 ∈ LRing )

Proof

Step	Hyp	Ref	Expression
1		drnglring.1	⊢ ( 𝜑 → 𝐹 ∈ DivRing )
2		drngnzr	⊢ ( 𝐹 ∈ DivRing → 𝐹 ∈ NzRing )
3	1 2	syl	⊢ ( 𝜑 → 𝐹 ∈ NzRing )
4	1	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) ∧ ¬ 𝑥 = ( 0g ‘ 𝐹 ) ) → 𝐹 ∈ DivRing )
5		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) ∧ ¬ 𝑥 = ( 0g ‘ 𝐹 ) ) → 𝑥 ∈ ( Base ‘ 𝐹 ) )
6		neqne	⊢ ( ¬ 𝑥 = ( 0g ‘ 𝐹 ) → 𝑥 ≠ ( 0g ‘ 𝐹 ) )
7	6	adantl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) ∧ ¬ 𝑥 = ( 0g ‘ 𝐹 ) ) → 𝑥 ≠ ( 0g ‘ 𝐹 ) )
8		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
9		eqid	⊢ ( Unit ‘ 𝐹 ) = ( Unit ‘ 𝐹 )
10		eqid	⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
11	8 9 10	drngunit	⊢ ( 𝐹 ∈ DivRing → ( 𝑥 ∈ ( Unit ‘ 𝐹 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑥 ≠ ( 0g ‘ 𝐹 ) ) ) )
12	11	biimpar	⊢ ( ( 𝐹 ∈ DivRing ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑥 ≠ ( 0g ‘ 𝐹 ) ) ) → 𝑥 ∈ ( Unit ‘ 𝐹 ) )
13	4 5 7 12	syl12anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) ∧ ¬ 𝑥 = ( 0g ‘ 𝐹 ) ) → 𝑥 ∈ ( Unit ‘ 𝐹 ) )
14	1	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) ∧ ¬ 𝑦 = ( 0g ‘ 𝐹 ) ) → 𝐹 ∈ DivRing )
15		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) ∧ ¬ 𝑦 = ( 0g ‘ 𝐹 ) ) → 𝑦 ∈ ( Base ‘ 𝐹 ) )
16		neqne	⊢ ( ¬ 𝑦 = ( 0g ‘ 𝐹 ) → 𝑦 ≠ ( 0g ‘ 𝐹 ) )
17	16	adantl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) ∧ ¬ 𝑦 = ( 0g ‘ 𝐹 ) ) → 𝑦 ≠ ( 0g ‘ 𝐹 ) )
18	8 9 10	drngunit	⊢ ( 𝐹 ∈ DivRing → ( 𝑦 ∈ ( Unit ‘ 𝐹 ) ↔ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ≠ ( 0g ‘ 𝐹 ) ) ) )
19	18	biimpar	⊢ ( ( 𝐹 ∈ DivRing ∧ ( 𝑦 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ≠ ( 0g ‘ 𝐹 ) ) ) → 𝑦 ∈ ( Unit ‘ 𝐹 ) )
20	14 15 17 19	syl12anc	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) ∧ ¬ 𝑦 = ( 0g ‘ 𝐹 ) ) → 𝑦 ∈ ( Unit ‘ 𝐹 ) )
21		simplll	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) → 𝜑 )
22		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) )
23		eqid	⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
24	23 10	nzrnz	⊢ ( 𝐹 ∈ NzRing → ( 1r ‘ 𝐹 ) ≠ ( 0g ‘ 𝐹 ) )
25	3 24	syl	⊢ ( 𝜑 → ( 1r ‘ 𝐹 ) ≠ ( 0g ‘ 𝐹 ) )
26	25	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) → ( 1r ‘ 𝐹 ) ≠ ( 0g ‘ 𝐹 ) )
27	22 26	eqnetrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) ≠ ( 0g ‘ 𝐹 ) )
28	27	neneqd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) → ¬ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 0g ‘ 𝐹 ) )
29		oveq12	⊢ ( ( 𝑥 = ( 0g ‘ 𝐹 ) ∧ 𝑦 = ( 0g ‘ 𝐹 ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( ( 0g ‘ 𝐹 ) ( +g ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) )
30	29	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 0g ‘ 𝐹 ) ∧ 𝑦 = ( 0g ‘ 𝐹 ) ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( ( 0g ‘ 𝐹 ) ( +g ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) )
31		eqid	⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
32	1	drnggrpd	⊢ ( 𝜑 → 𝐹 ∈ Grp )
33	32	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 0g ‘ 𝐹 ) ∧ 𝑦 = ( 0g ‘ 𝐹 ) ) ) → 𝐹 ∈ Grp )
34	8 10 33	grpidcld	⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 0g ‘ 𝐹 ) ∧ 𝑦 = ( 0g ‘ 𝐹 ) ) ) → ( 0g ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) )
35	8 31 10 33 34	grplidd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 0g ‘ 𝐹 ) ∧ 𝑦 = ( 0g ‘ 𝐹 ) ) ) → ( ( 0g ‘ 𝐹 ) ( +g ‘ 𝐹 ) ( 0g ‘ 𝐹 ) ) = ( 0g ‘ 𝐹 ) )
36	30 35	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 = ( 0g ‘ 𝐹 ) ∧ 𝑦 = ( 0g ‘ 𝐹 ) ) ) → ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 0g ‘ 𝐹 ) )
37	36	stoic1a	⊢ ( ( 𝜑 ∧ ¬ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 0g ‘ 𝐹 ) ) → ¬ ( 𝑥 = ( 0g ‘ 𝐹 ) ∧ 𝑦 = ( 0g ‘ 𝐹 ) ) )
38	21 28 37	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) → ¬ ( 𝑥 = ( 0g ‘ 𝐹 ) ∧ 𝑦 = ( 0g ‘ 𝐹 ) ) )
39		ianor	⊢ ( ¬ ( 𝑥 = ( 0g ‘ 𝐹 ) ∧ 𝑦 = ( 0g ‘ 𝐹 ) ) ↔ ( ¬ 𝑥 = ( 0g ‘ 𝐹 ) ∨ ¬ 𝑦 = ( 0g ‘ 𝐹 ) ) )
40	38 39	sylib	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) → ( ¬ 𝑥 = ( 0g ‘ 𝐹 ) ∨ ¬ 𝑦 = ( 0g ‘ 𝐹 ) ) )
41	13 20 40	orim12da	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ∧ ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) ) → ( 𝑥 ∈ ( Unit ‘ 𝐹 ) ∨ 𝑦 ∈ ( Unit ‘ 𝐹 ) ) )
42	41	ex	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐹 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) → ( ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) → ( 𝑥 ∈ ( Unit ‘ 𝐹 ) ∨ 𝑦 ∈ ( Unit ‘ 𝐹 ) ) ) )
43	42	anasss	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐹 ) ∧ 𝑦 ∈ ( Base ‘ 𝐹 ) ) ) → ( ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) → ( 𝑥 ∈ ( Unit ‘ 𝐹 ) ∨ 𝑦 ∈ ( Unit ‘ 𝐹 ) ) ) )
44	43	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ( ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) → ( 𝑥 ∈ ( Unit ‘ 𝐹 ) ∨ 𝑦 ∈ ( Unit ‘ 𝐹 ) ) ) )
45	8 31 23 9	islring	⊢ ( 𝐹 ∈ LRing ↔ ( 𝐹 ∈ NzRing ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ( ( 𝑥 ( +g ‘ 𝐹 ) 𝑦 ) = ( 1r ‘ 𝐹 ) → ( 𝑥 ∈ ( Unit ‘ 𝐹 ) ∨ 𝑦 ∈ ( Unit ‘ 𝐹 ) ) ) ) )
46	3 44 45	sylanbrc	⊢ ( 𝜑 → 𝐹 ∈ LRing )