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 Domn R NzRing A

Proof

Step Hyp Ref Expression
1 abvn0b.b A = AbsVal R
2 domnnzr R Domn R NzRing
3 eqid Base R = Base R
4 eqid 0 R = 0 R
5 eqid x Base R if x = 0 R 0 1 = x Base R if x = 0 R 0 1
6 eqid R = R
7 domnring R Domn R Ring
8 3 6 4 domnmuln0 R Domn y Base R y 0 R z Base R z 0 R y R z 0 R
9 1 3 4 5 6 7 8 abvtrivd R Domn x Base R if x = 0 R 0 1 A
10 9 ne0d R Domn A
11 2 10 jca R Domn R NzRing A
12 n0 A x x A
13 neanior y 0 R z 0 R ¬ y = 0 R z = 0 R
14 an4 y Base R z Base R y 0 R z 0 R y Base R y 0 R z Base R z 0 R
15 1 3 4 6 abvdom x A y Base R y 0 R z Base R z 0 R y R z 0 R
16 15 3expib x A y Base R y 0 R z Base R z 0 R y R z 0 R
17 14 16 syl5bi x A y Base R z Base R y 0 R z 0 R y R z 0 R
18 17 expdimp x A y Base R z Base R y 0 R z 0 R y R z 0 R
19 13 18 syl5bir x A y Base R z Base R ¬ y = 0 R z = 0 R y R z 0 R
20 19 necon4bd x A y Base R z Base R y R z = 0 R y = 0 R z = 0 R
21 20 ralrimivva x A y Base R z Base R y R z = 0 R y = 0 R z = 0 R
22 21 exlimiv x x A y Base R z Base R y R z = 0 R y = 0 R z = 0 R
23 12 22 sylbi A y Base R z Base R y R z = 0 R y = 0 R z = 0 R
24 23 anim2i R NzRing A R NzRing y Base R z Base R y R z = 0 R y = 0 R z = 0 R
25 3 6 4 isdomn R Domn R NzRing y Base R z Base R y R z = 0 R y = 0 R z = 0 R
26 24 25 sylibr R NzRing A R Domn
27 11 26 impbii R Domn R NzRing A