# 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 = ( AbsVal ` R )`
abvneg.b
`|- B = ( Base ` R )`
abvrec.z
`|- .0. = ( 0g ` R )`
abvdom.t
`|- .x. = ( .r ` R )`
Assertion abvdom
`|- ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( X .x. Y ) =/= .0. )`

### Proof

Step Hyp Ref Expression
1 abv0.a
` |-  A = ( AbsVal ` R )`
2 abvneg.b
` |-  B = ( Base ` R )`
3 abvrec.z
` |-  .0. = ( 0g ` R )`
4 abvdom.t
` |-  .x. = ( .r ` R )`
5 simp1
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> F e. A )`
6 simp2l
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> X e. B )`
7 simp3l
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> Y e. B )`
8 1 2 4 abvmul
` |-  ( ( F e. A /\ X e. B /\ Y e. B ) -> ( F ` ( X .x. Y ) ) = ( ( F ` X ) x. ( F ` Y ) ) )`
9 5 6 7 8 syl3anc
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( F ` ( X .x. Y ) ) = ( ( F ` X ) x. ( F ` Y ) ) )`
10 1 2 abvcl
` |-  ( ( F e. A /\ X e. B ) -> ( F ` X ) e. RR )`
11 5 6 10 syl2anc
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( F ` X ) e. RR )`
12 11 recnd
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( F ` X ) e. CC )`
13 1 2 abvcl
` |-  ( ( F e. A /\ Y e. B ) -> ( F ` Y ) e. RR )`
14 5 7 13 syl2anc
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( F ` Y ) e. RR )`
15 14 recnd
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( F ` Y ) e. CC )`
16 simp2r
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> X =/= .0. )`
17 1 2 3 abvne0
` |-  ( ( F e. A /\ X e. B /\ X =/= .0. ) -> ( F ` X ) =/= 0 )`
18 5 6 16 17 syl3anc
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( F ` X ) =/= 0 )`
19 simp3r
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> Y =/= .0. )`
20 1 2 3 abvne0
` |-  ( ( F e. A /\ Y e. B /\ Y =/= .0. ) -> ( F ` Y ) =/= 0 )`
21 5 7 19 20 syl3anc
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( F ` Y ) =/= 0 )`
22 12 15 18 21 mulne0d
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( ( F ` X ) x. ( F ` Y ) ) =/= 0 )`
23 9 22 eqnetrd
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( F ` ( X .x. Y ) ) =/= 0 )`
24 1 3 abv0
` |-  ( F e. A -> ( F ` .0. ) = 0 )`
25 5 24 syl
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( F ` .0. ) = 0 )`
26 fveqeq2
` |-  ( ( X .x. Y ) = .0. -> ( ( F ` ( X .x. Y ) ) = 0 <-> ( F ` .0. ) = 0 ) )`
27 25 26 syl5ibrcom
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( ( X .x. Y ) = .0. -> ( F ` ( X .x. Y ) ) = 0 ) )`
28 27 necon3d
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( ( F ` ( X .x. Y ) ) =/= 0 -> ( X .x. Y ) =/= .0. ) )`
29 23 28 mpd
` |-  ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( X .x. Y ) =/= .0. )`