Metamath Proof Explorer

Theorem abvn0b

Description: Another characterization of domains, hinted at in abvtrivg : a nonzero ring is a domain iff it has an absolute value. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Hypothesis abvn0b.b 
|- A = ( AbsVal ` R )
Assertion abvn0b 
|- ( R e. Domn <-> ( R e. NzRing /\ A =/= (/) ) )

Proof

Step Hyp Ref Expression
1 abvn0b.b 
 |-  A = ( AbsVal ` R )
2 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
5 eqid 
 |-  ( x e. ( Base ` R ) |-> if ( x = ( 0g ` R ) , 0 , 1 ) ) = ( x e. ( Base ` R ) |-> if ( x = ( 0g ` R ) , 0 , 1 ) )
6 1 3 4 5 abvtrivg 
 |-  ( R e. Domn -> ( x e. ( Base ` R ) |-> if ( x = ( 0g ` R ) , 0 , 1 ) ) e. A )
7 6 ne0d 
 |-  ( R e. Domn -> A =/= (/) )
8 2 7 jca 
 |-  ( R e. Domn -> ( R e. NzRing /\ A =/= (/) ) )
9 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
10 neanior 
 |-  ( ( y =/= ( 0g ` R ) /\ z =/= ( 0g ` R ) ) <-> -. ( y = ( 0g ` R ) \/ z = ( 0g ` R ) ) )
11 an4 
 |-  ( ( ( y e. ( Base ` R ) /\ z e. ( Base ` R ) ) /\ ( y =/= ( 0g ` R ) /\ z =/= ( 0g ` R ) ) ) <-> ( ( y e. ( Base ` R ) /\ y =/= ( 0g ` R ) ) /\ ( z e. ( Base ` R ) /\ z =/= ( 0g ` R ) ) ) )
12 eqid 
 |-  ( .r ` R ) = ( .r ` R )
13 1 3 4 12 abvdom 
 |-  ( ( x e. A /\ ( y e. ( Base ` R ) /\ y =/= ( 0g ` R ) ) /\ ( z e. ( Base ` R ) /\ z =/= ( 0g ` R ) ) ) -> ( y ( .r ` R ) z ) =/= ( 0g ` R ) )
14 13 3expib 
 |-  ( x e. A -> ( ( ( y e. ( Base ` R ) /\ y =/= ( 0g ` R ) ) /\ ( z e. ( Base ` R ) /\ z =/= ( 0g ` R ) ) ) -> ( y ( .r ` R ) z ) =/= ( 0g ` R ) ) )
15 11 14 biimtrid 
 |-  ( x e. A -> ( ( ( y e. ( Base ` R ) /\ z e. ( Base ` R ) ) /\ ( y =/= ( 0g ` R ) /\ z =/= ( 0g ` R ) ) ) -> ( y ( .r ` R ) z ) =/= ( 0g ` R ) ) )
16 15 expdimp 
 |-  ( ( x e. A /\ ( y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( y =/= ( 0g ` R ) /\ z =/= ( 0g ` R ) ) -> ( y ( .r ` R ) z ) =/= ( 0g ` R ) ) )
17 10 16 biimtrrid 
 |-  ( ( x e. A /\ ( y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( -. ( y = ( 0g ` R ) \/ z = ( 0g ` R ) ) -> ( y ( .r ` R ) z ) =/= ( 0g ` R ) ) )
18 17 necon4bd 
 |-  ( ( x e. A /\ ( y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( y ( .r ` R ) z ) = ( 0g ` R ) -> ( y = ( 0g ` R ) \/ z = ( 0g ` R ) ) ) )
19 18 ralrimivva 
 |-  ( x e. A -> A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( y ( .r ` R ) z ) = ( 0g ` R ) -> ( y = ( 0g ` R ) \/ z = ( 0g ` R ) ) ) )
20 19 exlimiv 
 |-  ( E. x x e. A -> A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( y ( .r ` R ) z ) = ( 0g ` R ) -> ( y = ( 0g ` R ) \/ z = ( 0g ` R ) ) ) )
21 9 20 sylbi 
 |-  ( A =/= (/) -> A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( y ( .r ` R ) z ) = ( 0g ` R ) -> ( y = ( 0g ` R ) \/ z = ( 0g ` R ) ) ) )
22 21 anim2i 
 |-  ( ( R e. NzRing /\ A =/= (/) ) -> ( R e. NzRing /\ A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( y ( .r ` R ) z ) = ( 0g ` R ) -> ( y = ( 0g ` R ) \/ z = ( 0g ` R ) ) ) ) )
23 3 12 4 isdomn 
 |-  ( R e. Domn <-> ( R e. NzRing /\ A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( y ( .r ` R ) z ) = ( 0g ` R ) -> ( y = ( 0g ` R ) \/ z = ( 0g ` R ) ) ) ) )
24 22 23 sylibr 
 |-  ( ( R e. NzRing /\ A =/= (/) ) -> R e. Domn )
25 8 24 impbii 
 |-  ( R e. Domn <-> ( R e. NzRing /\ A =/= (/) ) )