Metamath Proof Explorer

Theorem dflring2

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

Ref Expression
Hypotheses dflring2.1 
|- B = ( Base ` R )
dflring2.2 
|- U = ( Unit ` R )
dflring2.3 
|- .1. = ( 1r ` R )
dflring2.4 
|- .- = ( -g ` R )
Assertion dflring2 
|- ( R e. LRing <-> ( R e. NzRing /\ A. x e. B ( x e. U \/ ( .1. .- x ) e. U ) ) )

Proof

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