Metamath Proof Explorer


Theorem abvdom

Description: Any ring with an absolute value is a domain, which is to say that it contains no zero divisors. (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses abv0.a A=AbsValR
abvneg.b B=BaseR
abvrec.z 0˙=0R
abvdom.t ·˙=R
Assertion abvdom FAXBX0˙YBY0˙X·˙Y0˙

Proof

Step Hyp Ref Expression
1 abv0.a A=AbsValR
2 abvneg.b B=BaseR
3 abvrec.z 0˙=0R
4 abvdom.t ·˙=R
5 simp1 FAXBX0˙YBY0˙FA
6 simp2l FAXBX0˙YBY0˙XB
7 simp3l FAXBX0˙YBY0˙YB
8 1 2 4 abvmul FAXBYBFX·˙Y=FXFY
9 5 6 7 8 syl3anc FAXBX0˙YBY0˙FX·˙Y=FXFY
10 1 2 abvcl FAXBFX
11 5 6 10 syl2anc FAXBX0˙YBY0˙FX
12 11 recnd FAXBX0˙YBY0˙FX
13 1 2 abvcl FAYBFY
14 5 7 13 syl2anc FAXBX0˙YBY0˙FY
15 14 recnd FAXBX0˙YBY0˙FY
16 simp2r FAXBX0˙YBY0˙X0˙
17 1 2 3 abvne0 FAXBX0˙FX0
18 5 6 16 17 syl3anc FAXBX0˙YBY0˙FX0
19 simp3r FAXBX0˙YBY0˙Y0˙
20 1 2 3 abvne0 FAYBY0˙FY0
21 5 7 19 20 syl3anc FAXBX0˙YBY0˙FY0
22 12 15 18 21 mulne0d FAXBX0˙YBY0˙FXFY0
23 9 22 eqnetrd FAXBX0˙YBY0˙FX·˙Y0
24 1 3 abv0 FAF0˙=0
25 5 24 syl FAXBX0˙YBY0˙F0˙=0
26 fveqeq2 X·˙Y=0˙FX·˙Y=0F0˙=0
27 25 26 syl5ibrcom FAXBX0˙YBY0˙X·˙Y=0˙FX·˙Y=0
28 27 necon3d FAXBX0˙YBY0˙FX·˙Y0X·˙Y0˙
29 23 28 mpd FAXBX0˙YBY0˙X·˙Y0˙