Metamath Proof Explorer

Theorem dflring2

Description: Alternate definition of a local ring. (Contributed by Thierry Arnoux, 2-Jun-2026)

Ref Expression
Hypotheses dflring2.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
dflring2.2 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
dflring2.3 ⊢ 1 = ( 1r ‘ 𝑅 )
dflring2.4 ⊢ − = ( -g ‘ 𝑅 )
Assertion dflring2 ( 𝑅 ∈ LRing ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 dflring2.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 dflring2.2 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 dflring2.3 ⊢ 1 = ( 1r ‘ 𝑅 )
4 dflring2.4 ⊢ − = ( -g ‘ 𝑅 )
5 lringnzr ⊢ ( 𝑅 ∈ LRing → 𝑅 ∈ NzRing )
6 1 a1i ⊢ ( ( 𝑅 ∈ LRing ∧ 𝑥 ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝑅 ) )
7 2 a1i ⊢ ( ( 𝑅 ∈ LRing ∧ 𝑥 ∈ 𝐵 ) → 𝑈 = ( Unit ‘ 𝑅 ) )
8 eqidd ⊢ ( ( 𝑅 ∈ LRing ∧ 𝑥 ∈ 𝐵 ) → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) )
9 simpl ⊢ ( ( 𝑅 ∈ LRing ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ LRing )
10 lringring ⊢ ( 𝑅 ∈ LRing → 𝑅 ∈ Ring )
11 10 ringabld ⊢ ( 𝑅 ∈ LRing → 𝑅 ∈ Abel )
12 11 adantr ⊢ ( ( 𝑅 ∈ LRing ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ Abel )
13 simpr ⊢ ( ( 𝑅 ∈ LRing ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
14 1 3 10 ringidcld ⊢ ( 𝑅 ∈ LRing → 1 ∈ 𝐵 )
15 14 adantr ⊢ ( ( 𝑅 ∈ LRing ∧ 𝑥 ∈ 𝐵 ) → 1 ∈ 𝐵 )
16 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
17 1 16 4 ablpncan3 ⊢ ( ( 𝑅 ∈ Abel ∧ ( 𝑥 ∈ 𝐵 ∧ 1 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) ( 1 − 𝑥 ) ) = 1 )
18 12 13 15 17 syl12anc ⊢ ( ( 𝑅 ∈ LRing ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝑅 ) ( 1 − 𝑥 ) ) = 1 )
19 2 3 1unit ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝑈 )
20 10 19 syl ⊢ ( 𝑅 ∈ LRing → 1 ∈ 𝑈 )
21 20 adantr ⊢ ( ( 𝑅 ∈ LRing ∧ 𝑥 ∈ 𝐵 ) → 1 ∈ 𝑈 )
22 18 21 eqeltrd ⊢ ( ( 𝑅 ∈ LRing ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝑅 ) ( 1 − 𝑥 ) ) ∈ 𝑈 )
23 10 ringgrpd ⊢ ( 𝑅 ∈ LRing → 𝑅 ∈ Grp )
24 23 adantr ⊢ ( ( 𝑅 ∈ LRing ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ Grp )
25 1 4 24 15 13 grpsubcld ⊢ ( ( 𝑅 ∈ LRing ∧ 𝑥 ∈ 𝐵 ) → ( 1 − 𝑥 ) ∈ 𝐵 )
26 6 7 8 9 22 13 25 lringuplu ⊢ ( ( 𝑅 ∈ LRing ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) )
27 26 ralrimiva ⊢ ( 𝑅 ∈ LRing → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) )
28 5 27 jca ⊢ ( 𝑅 ∈ LRing → ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) )
29 simpl ⊢ ( ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) → 𝑅 ∈ NzRing )
30 simpr ⊢ ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 )
31 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
32 31 ringgrpd ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Grp )
33 32 ad4antr ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) → 𝑅 ∈ Grp )
34 1 3 31 ringidcld ⊢ ( 𝑅 ∈ NzRing → 1 ∈ 𝐵 )
35 34 ad4antr ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) → 1 ∈ 𝐵 )
36 simp-4r ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) → 𝑥 ∈ 𝐵 )
37 simplr ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) → 𝑦 ∈ 𝐵 )
38 35 36 37 3jca ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) → ( 1 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
39 31 ringabld ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Abel )
40 39 ad4antr ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) → 𝑅 ∈ Abel )
41 1 16 40 37 36 ablcomd ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) )
42 simpr ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 )
43 41 42 eqtrd ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 1 )
44 1 16 4 grpsubadd ⊢ ( ( 𝑅 ∈ Grp ∧ ( 1 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 1 − 𝑥 ) = 𝑦 ↔ ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 1 ) )
45 44 biimpar ⊢ ( ( ( 𝑅 ∈ Grp ∧ ( 1 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑦 ( +g ‘ 𝑅 ) 𝑥 ) = 1 ) → ( 1 − 𝑥 ) = 𝑦 )
46 33 38 43 45 syl21anc ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) → ( 1 − 𝑥 ) = 𝑦 )
47 46 eqcomd ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) → 𝑦 = ( 1 − 𝑥 ) )
48 47 adantr ⊢ ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) ∧ ( 1 − 𝑥 ) ∈ 𝑈 ) → 𝑦 = ( 1 − 𝑥 ) )
49 simpr ⊢ ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) ∧ ( 1 − 𝑥 ) ∈ 𝑈 ) → ( 1 − 𝑥 ) ∈ 𝑈 )
50 48 49 eqeltrd ⊢ ( ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) ∧ ( 1 − 𝑥 ) ∈ 𝑈 ) → 𝑦 ∈ 𝑈 )
51 simpllr ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) → ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) )
52 30 50 51 orim12da ⊢ ( ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 ) → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) )
53 52 ex ⊢ ( ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) )
54 53 ralrimiva ⊢ ( ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) → ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) )
55 54 ex ⊢ ( ( 𝑅 ∈ NzRing ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )
56 55 ralimdva ⊢ ( 𝑅 ∈ NzRing → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )
57 56 imp ⊢ ( ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) )
58 1 16 3 2 islring ⊢ ( 𝑅 ∈ LRing ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = 1 → ( 𝑥 ∈ 𝑈 ∨ 𝑦 ∈ 𝑈 ) ) ) )
59 29 57 58 sylanbrc ⊢ ( ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) → 𝑅 ∈ LRing )
60 28 59 impbii ⊢ ( 𝑅 ∈ LRing ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ 𝑈 ∨ ( 1 − 𝑥 ) ∈ 𝑈 ) ) )