# 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 𝐴 = ( AbsVal ‘ 𝑅 )
abvneg.b 𝐵 = ( Base ‘ 𝑅 )
abvrec.z 0 = ( 0g𝑅 )
abvdom.t · = ( .r𝑅 )
Assertion abvdom ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( 𝑋 · 𝑌 ) ≠ 0 )

### Proof

Step Hyp Ref Expression
1 abv0.a 𝐴 = ( AbsVal ‘ 𝑅 )
2 abvneg.b 𝐵 = ( Base ‘ 𝑅 )
3 abvrec.z 0 = ( 0g𝑅 )
4 abvdom.t · = ( .r𝑅 )
5 simp1 ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → 𝐹𝐴 )
6 simp2l ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → 𝑋𝐵 )
7 simp3l ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → 𝑌𝐵 )
8 1 2 4 abvmul ( ( 𝐹𝐴𝑋𝐵𝑌𝐵 ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹𝑋 ) · ( 𝐹𝑌 ) ) )
9 5 6 7 8 syl3anc ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐹𝑋 ) · ( 𝐹𝑌 ) ) )
10 1 2 abvcl ( ( 𝐹𝐴𝑋𝐵 ) → ( 𝐹𝑋 ) ∈ ℝ )
11 5 6 10 syl2anc ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( 𝐹𝑋 ) ∈ ℝ )
12 11 recnd ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( 𝐹𝑋 ) ∈ ℂ )
13 1 2 abvcl ( ( 𝐹𝐴𝑌𝐵 ) → ( 𝐹𝑌 ) ∈ ℝ )
14 5 7 13 syl2anc ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( 𝐹𝑌 ) ∈ ℝ )
15 14 recnd ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( 𝐹𝑌 ) ∈ ℂ )
16 simp2r ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → 𝑋0 )
17 1 2 3 abvne0 ( ( 𝐹𝐴𝑋𝐵𝑋0 ) → ( 𝐹𝑋 ) ≠ 0 )
18 5 6 16 17 syl3anc ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( 𝐹𝑋 ) ≠ 0 )
19 simp3r ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → 𝑌0 )
20 1 2 3 abvne0 ( ( 𝐹𝐴𝑌𝐵𝑌0 ) → ( 𝐹𝑌 ) ≠ 0 )
21 5 7 19 20 syl3anc ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( 𝐹𝑌 ) ≠ 0 )
22 12 15 18 21 mulne0d ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( ( 𝐹𝑋 ) · ( 𝐹𝑌 ) ) ≠ 0 )
23 9 22 eqnetrd ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ≠ 0 )
24 1 3 abv0 ( 𝐹𝐴 → ( 𝐹0 ) = 0 )
25 5 24 syl ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( 𝐹0 ) = 0 )
26 fveqeq2 ( ( 𝑋 · 𝑌 ) = 0 → ( ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = 0 ↔ ( 𝐹0 ) = 0 ) )
27 25 26 syl5ibrcom ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( ( 𝑋 · 𝑌 ) = 0 → ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) = 0 ) )
28 27 necon3d ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( ( 𝐹 ‘ ( 𝑋 · 𝑌 ) ) ≠ 0 → ( 𝑋 · 𝑌 ) ≠ 0 ) )
29 23 28 mpd ( ( 𝐹𝐴 ∧ ( 𝑋𝐵𝑋0 ) ∧ ( 𝑌𝐵𝑌0 ) ) → ( 𝑋 · 𝑌 ) ≠ 0 )