abvn0b

Description: Another characterization of domains, hinted at in abvtrivg : 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	1 3 4 5	abvtrivg	$⊢ R \in Domn \to (x \in {Base}_{R} ⟼ if (x = 0_{R}, 0, 1)) \in A$
7	6	ne0d	$⊢ R \in Domn \to A \neq \emptyset$
8	2 7	jca	$⊢ R \in Domn \to (R \in NzRing \land A \neq \emptyset)$
9		n0	$⊢ A \neq \emptyset \leftrightarrow \exists x x \in A$
10		neanior	$⊢ (y \neq 0_{R} \land z \neq 0_{R}) \leftrightarrow \neg (y = 0_{R} \lor z = 0_{R})$
11		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}))$
12		eqid	$⊢ \cdot_{R} = \cdot_{R}$
13	1 3 4 12	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}$
14	13	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})$
15	11 14	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})$
16	15	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})$
17	10 16	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})$
18	17	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}))$
19	18	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}))$
20	19	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}))$
21	9 20	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}))$
22	21	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})))$
23	3 12 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})))$
24	22 23	sylibr	$⊢ (R \in NzRing \land A \neq \emptyset) \to R \in Domn$
25	8 24	impbii	$⊢ R \in Domn \leftrightarrow (R \in NzRing \land A \neq \emptyset)$

Metamath Proof Explorer

Theorem abvn0b

Proof