Metamath Proof Explorer

Theorem abvn0b

Description: Another characterization of domains, hinted at in abvtriv : 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 eqid 
 |-  ( .r ` R ) = ( .r ` R )
7 domnring 
 |-  ( R e. Domn -> R e. Ring )
8 3 6 4 domnmuln0 
 |-  ( ( R e. Domn /\ ( y e. ( Base ` R ) /\ y =/= ( 0g ` R ) ) /\ ( z e. ( Base ` R ) /\ z =/= ( 0g ` R ) ) ) -> ( y ( .r ` R ) z ) =/= ( 0g ` R ) )
9 1 3 4 5 6 7 8 abvtrivd 
 |-  ( R e. Domn -> ( x e. ( Base ` R ) |-> if ( x = ( 0g ` R ) , 0 , 1 ) ) e. A )
10 9 ne0d 
 |-  ( R e. Domn -> A =/= (/) )
11 2 10 jca 
 |-  ( R e. Domn -> ( R e. NzRing /\ A =/= (/) ) )
12 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
13 neanior 
 |-  ( ( y =/= ( 0g ` R ) /\ z =/= ( 0g ` R ) ) <-> -. ( y = ( 0g ` R ) \/ z = ( 0g ` R ) ) )
14 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 ) ) ) )
15 1 3 4 6 abvdom 
 |-  ( ( x e. A /\ ( y e. ( Base ` R ) /\ y =/= ( 0g ` R ) ) /\ ( z e. ( Base ` R ) /\ z =/= ( 0g ` R ) ) ) -> ( y ( .r ` R ) z ) =/= ( 0g ` R ) )
16 15 3expib 
 |-  ( x e. A -> ( ( ( y e. ( Base ` R ) /\ y =/= ( 0g ` R ) ) /\ ( z e. ( Base ` R ) /\ z =/= ( 0g ` R ) ) ) -> ( y ( .r ` R ) z ) =/= ( 0g ` R ) ) )
17 14 16 syl5bi 
 |-  ( 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 expdimp 
 |-  ( ( x e. A /\ ( y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( y =/= ( 0g ` R ) /\ z =/= ( 0g ` R ) ) -> ( y ( .r ` R ) z ) =/= ( 0g ` R ) ) )
19 13 18 syl5bir 
 |-  ( ( x e. A /\ ( y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( -. ( y = ( 0g ` R ) \/ z = ( 0g ` R ) ) -> ( y ( .r ` R ) z ) =/= ( 0g ` R ) ) )
20 19 necon4bd 
 |-  ( ( x e. A /\ ( y e. ( Base ` R ) /\ z e. ( Base ` R ) ) ) -> ( ( y ( .r ` R ) z ) = ( 0g ` R ) -> ( y = ( 0g ` R ) \/ z = ( 0g ` R ) ) ) )
21 20 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 ) ) ) )
22 21 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 ) ) ) )
23 12 22 sylbi 
 |-  ( A =/= (/) -> A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( y ( .r ` R ) z ) = ( 0g ` R ) -> ( y = ( 0g ` R ) \/ z = ( 0g ` R ) ) ) )
24 23 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 ) ) ) ) )
25 3 6 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 ) ) ) ) )
26 24 25 sylibr 
 |-  ( ( R e. NzRing /\ A =/= (/) ) -> R e. Domn )
27 11 26 impbii 
 |-  ( R e. Domn <-> ( R e. NzRing /\ A =/= (/) ) )