This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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. )