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	$⊢ \underset{˙}{0} = 0_{R}$
	abvdom.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	abvdom	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to X \underset{˙}{\cdot} Y \neq \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		abv0.a	$⊢ A = AbsVal (R)$
2		abvneg.b	$⊢ B = {Base}_{R}$
3		abvrec.z	$⊢ \underset{˙}{0} = 0_{R}$
4		abvdom.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		simp1	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to F \in A$
6		simp2l	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to X \in B$
7		simp3l	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to Y \in B$
8	1 2 4	abvmul	$⊢ (F \in A \land X \in B \land Y \in B) \to F (X \underset{˙}{\cdot} Y) = F (X) F (Y)$
9	5 6 7 8	syl3anc	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to F (X \underset{˙}{\cdot} Y) = F (X) F (Y)$
10	1 2	abvcl	$⊢ (F \in A \land X \in B) \to F (X) \in ℝ$
11	5 6 10	syl2anc	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to F (X) \in ℝ$
12	11	recnd	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to F (X) \in ℂ$
13	1 2	abvcl	$⊢ (F \in A \land Y \in B) \to F (Y) \in ℝ$
14	5 7 13	syl2anc	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to F (Y) \in ℝ$
15	14	recnd	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to F (Y) \in ℂ$
16		simp2r	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to X \neq \underset{˙}{0}$
17	1 2 3	abvne0	$⊢ (F \in A \land X \in B \land X \neq \underset{˙}{0}) \to F (X) \neq 0$
18	5 6 16 17	syl3anc	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to F (X) \neq 0$
19		simp3r	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to Y \neq \underset{˙}{0}$
20	1 2 3	abvne0	$⊢ (F \in A \land Y \in B \land Y \neq \underset{˙}{0}) \to F (Y) \neq 0$
21	5 7 19 20	syl3anc	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to F (Y) \neq 0$
22	12 15 18 21	mulne0d	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to F (X) F (Y) \neq 0$
23	9 22	eqnetrd	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to F (X \underset{˙}{\cdot} Y) \neq 0$
24	1 3	abv0	$⊢ F \in A \to F (\underset{˙}{0}) = 0$
25	5 24	syl	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to F (\underset{˙}{0}) = 0$
26		fveqeq2	$⊢ X \underset{˙}{\cdot} Y = \underset{˙}{0} \to (F (X \underset{˙}{\cdot} Y) = 0 \leftrightarrow F (\underset{˙}{0}) = 0)$
27	25 26	syl5ibrcom	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \to F (X \underset{˙}{\cdot} Y) = 0)$
28	27	necon3d	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to (F (X \underset{˙}{\cdot} Y) \neq 0 \to X \underset{˙}{\cdot} Y \neq \underset{˙}{0})$
29	23 28	mpd	$⊢ (F \in A \land (X \in B \land X \neq \underset{˙}{0}) \land (Y \in B \land Y \neq \underset{˙}{0})) \to X \underset{˙}{\cdot} Y \neq \underset{˙}{0}$

Metamath Proof Explorer

Theorem abvdom

Proof