abvn0b

Description: Another characterization of domains, hinted at in abvtriv : a nonzero ring is a domain iff it has an absolute value. (Contributed by Mario Carneiro, 6-May-2015)

		Ref	Expression
	Hypothesis	abvn0b.b	$⊢ A = AbsVal (R)$
	Assertion	abvn0b	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land A \neq \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		abvn0b.b	$⊢ A = AbsVal (R)$
2		domnnzr	$⊢ R \in Domn \to R \in NzRing$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4		eqid	$⊢ 0_{R} = 0_{R}$
5		eqid	$⊢ (x \in {Base}_{R} ⟼ if (x = 0_{R}, 0, 1)) = (x \in {Base}_{R} ⟼ if (x = 0_{R}, 0, 1))$
6		eqid	$⊢ \cdot_{R} = \cdot_{R}$
7		domnring	$⊢ R \in Domn \to R \in Ring$
8	3 6 4	domnmuln0	$⊢ (R \in Domn \land (y \in {Base}_{R} \land y \neq 0_{R}) \land (z \in {Base}_{R} \land z \neq 0_{R})) \to y \cdot_{R} z \neq 0_{R}$
9	1 3 4 5 6 7 8	abvtrivd	$⊢ R \in Domn \to (x \in {Base}_{R} ⟼ if (x = 0_{R}, 0, 1)) \in A$
10	9	ne0d	$⊢ R \in Domn \to A \neq \emptyset$
11	2 10	jca	$⊢ R \in Domn \to (R \in NzRing \land A \neq \emptyset)$
12		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
13		neanior	$⊢ (y \neq 0_{R} \land z \neq 0_{R}) \leftrightarrow \neg (y = 0_{R} \lor z = 0_{R})$
14		an4	$⊢ ((y \in {Base}_{R} \land z \in {Base}_{R}) \land (y \neq 0_{R} \land z \neq 0_{R})) \leftrightarrow ((y \in {Base}_{R} \land y \neq 0_{R}) \land (z \in {Base}_{R} \land z \neq 0_{R}))$
15	1 3 4 6	abvdom	$⊢ (x \in A \land (y \in {Base}_{R} \land y \neq 0_{R}) \land (z \in {Base}_{R} \land z \neq 0_{R})) \to y \cdot_{R} z \neq 0_{R}$
16	15	3expib	$⊢ x \in A \to (((y \in {Base}_{R} \land y \neq 0_{R}) \land (z \in {Base}_{R} \land z \neq 0_{R})) \to y \cdot_{R} z \neq 0_{R})$
17	14 16	biimtrid	$⊢ x \in A \to (((y \in {Base}_{R} \land z \in {Base}_{R}) \land (y \neq 0_{R} \land z \neq 0_{R})) \to y \cdot_{R} z \neq 0_{R})$
18	17	expdimp	$⊢ (x \in A \land (y \in {Base}_{R} \land z \in {Base}_{R})) \to ((y \neq 0_{R} \land z \neq 0_{R}) \to y \cdot_{R} z \neq 0_{R})$
19	13 18	biimtrrid	$⊢ (x \in A \land (y \in {Base}_{R} \land z \in {Base}_{R})) \to (\neg (y = 0_{R} \lor z = 0_{R}) \to y \cdot_{R} z \neq 0_{R})$
20	19	necon4bd	$⊢ (x \in A \land (y \in {Base}_{R} \land z \in {Base}_{R})) \to (y \cdot_{R} z = 0_{R} \to (y = 0_{R} \lor z = 0_{R}))$
21	20	ralrimivva	$⊢ x \in A \to \forall y \in {Base}_{R} \forall z \in {Base}_{R} (y \cdot_{R} z = 0_{R} \to (y = 0_{R} \lor z = 0_{R}))$
22	21	exlimiv	$⊢ \exists x x \in A \to \forall y \in {Base}_{R} \forall z \in {Base}_{R} (y \cdot_{R} z = 0_{R} \to (y = 0_{R} \lor z = 0_{R}))$
23	12 22	sylbi	$⊢ A \neq \emptyset \to \forall y \in {Base}_{R} \forall z \in {Base}_{R} (y \cdot_{R} z = 0_{R} \to (y = 0_{R} \lor z = 0_{R}))$
24	23	anim2i	$⊢ (R \in NzRing \land A \neq \emptyset) \to (R \in NzRing \land \forall y \in {Base}_{R} \forall z \in {Base}_{R} (y \cdot_{R} z = 0_{R} \to (y = 0_{R} \lor z = 0_{R})))$
25	3 6 4	isdomn	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land \forall y \in {Base}_{R} \forall z \in {Base}_{R} (y \cdot_{R} z = 0_{R} \to (y = 0_{R} \lor z = 0_{R})))$
26	24 25	sylibr	$⊢ (R \in NzRing \land A \neq \emptyset) \to R \in Domn$
27	11 26	impbii	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land A \neq \emptyset)$

Metamath Proof Explorer

Theorem abvn0b

Proof