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 )