Metamath Proof Explorer

Theorem islring

Description: The predicate "is a local ring". (Contributed by SN, 23-Feb-2025)

Ref Expression
Hypotheses islring.b 
|- B = ( Base ` R )
islring.a 
|- .+ = ( +g ` R )
islring.1 
|- .1. = ( 1r ` R )
islring.u 
|- U = ( Unit ` R )
Assertion islring 
|- ( R e. LRing <-> ( R e. NzRing /\ A. x e. B A. y e. B ( ( x .+ y ) = .1. -> ( x e. U \/ y e. U ) ) ) )

Proof

Step Hyp Ref Expression
1 islring.b 
 |-  B = ( Base ` R )
2 islring.a 
 |-  .+ = ( +g ` R )
3 islring.1 
 |-  .1. = ( 1r ` R )
4 islring.u 
 |-  U = ( Unit ` R )
5 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
6 5 1 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
7 fveq2 
 |-  ( r = R -> ( +g ` r ) = ( +g ` R ) )
8 7 2 eqtr4di 
 |-  ( r = R -> ( +g ` r ) = .+ )
9 8 oveqd 
 |-  ( r = R -> ( x ( +g ` r ) y ) = ( x .+ y ) )
10 fveq2 
 |-  ( r = R -> ( 1r ` r ) = ( 1r ` R ) )
11 10 3 eqtr4di 
 |-  ( r = R -> ( 1r ` r ) = .1. )
12 9 11 eqeq12d 
 |-  ( r = R -> ( ( x ( +g ` r ) y ) = ( 1r ` r ) <-> ( x .+ y ) = .1. ) )
13 fveq2 
 |-  ( r = R -> ( Unit ` r ) = ( Unit ` R ) )
14 13 4 eqtr4di 
 |-  ( r = R -> ( Unit ` r ) = U )
15 14 eleq2d 
 |-  ( r = R -> ( x e. ( Unit ` r ) <-> x e. U ) )
16 14 eleq2d 
 |-  ( r = R -> ( y e. ( Unit ` r ) <-> y e. U ) )
17 15 16 orbi12d 
 |-  ( r = R -> ( ( x e. ( Unit ` r ) \/ y e. ( Unit ` r ) ) <-> ( x e. U \/ y e. U ) ) )
18 12 17 imbi12d 
 |-  ( r = R -> ( ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. ( Unit ` r ) \/ y e. ( Unit ` r ) ) ) <-> ( ( x .+ y ) = .1. -> ( x e. U \/ y e. U ) ) ) )
19 6 18 raleqbidv 
 |-  ( r = R -> ( A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. ( Unit ` r ) \/ y e. ( Unit ` r ) ) ) <-> A. y e. B ( ( x .+ y ) = .1. -> ( x e. U \/ y e. U ) ) ) )
20 6 19 raleqbidv 
 |-  ( r = R -> ( A. x e. ( Base ` r ) A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. ( Unit ` r ) \/ y e. ( Unit ` r ) ) ) <-> A. x e. B A. y e. B ( ( x .+ y ) = .1. -> ( x e. U \/ y e. U ) ) ) )
21 df-lring 
 |-  LRing = { r e. NzRing | A. x e. ( Base ` r ) A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. ( Unit ` r ) \/ y e. ( Unit ` r ) ) ) }
22 20 21 elrab2 
 |-  ( R e. LRing <-> ( R e. NzRing /\ A. x e. B A. y e. B ( ( x .+ y ) = .1. -> ( x e. U \/ y e. U ) ) ) )