Theorem abvtriv

Description: The trivial absolute value. (This theorem is true as long as R is a domain, but it is not true for rings with zero divisors, which violate the multiplication axiom; abvdom is the converse of this remark.) (Contributed by Mario Carneiro, 8-Sep-2014) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	abvtriv.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
	abvtriv.b	$$⊢B={\mathrm{Base}}_R$$
	abvtriv.z	$$⊢\underset{\dot{}}{0}=0_R$$
	abvtriv.f	$$⊢F=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,1\right)\right)$$
Assertion	abvtriv	$$⊢R\in \mathrm{DivRing}\to F\in A$$

Proof

Step	Hyp	Ref	Expression
1		abvtriv.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abvtriv.b	$$⊢B={\mathrm{Base}}_R$$
3		abvtriv.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		abvtriv.f	$$⊢F=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,1\right)\right)$$
5		eqid	$$⊢{\cdot }_R={\cdot }_R$$
6		drngring	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{Ring}$$
7		biid	$$⊢R\in \mathrm{DivRing}\leftrightarrow R\in \mathrm{DivRing}$$
8		eldifsn	$$⊢y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)$$
9		eldifsn	$$⊢z\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)$$
10	2 5 3	drngmcl	$$⊢\left(R\in \mathrm{DivRing}\wedge y\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge z\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to y{\cdot }_{R}z\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11	7 8 9 10	syl3anbr	$$⊢\left(R\in \mathrm{DivRing}\wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to y{\cdot }_{R}z\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
12		eldifsn	$$⊢y{\cdot }_{R}z\in \left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)\leftrightarrow \left(y{\cdot }_{R}z\in B\wedge y{\cdot }_{R}z\ne \underset{\dot{}}{0}\right)$$
13	11 12	sylib	$$⊢\left(R\in \mathrm{DivRing}\wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to \left(y{\cdot }_{R}z\in B\wedge y{\cdot }_{R}z\ne \underset{\dot{}}{0}\right)$$
14	13	simprd	$$⊢\left(R\in \mathrm{DivRing}\wedge \left(y\in B\wedge y\ne \underset{\dot{}}{0}\right)\wedge \left(z\in B\wedge z\ne \underset{\dot{}}{0}\right)\right)\to y{\cdot }_{R}z\ne \underset{\dot{}}{0}$$
15	1 2 3 4 5 6 14	abvtrivd	$$⊢R\in \mathrm{DivRing}\to F\in A$$