Theorem abveq0

Description: The value of an absolute value is zero iff the argument is zero. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypotheses	abvf.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
	abvf.b	$$⊢B={\mathrm{Base}}_R$$
	abveq0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	abveq0	$$⊢\left(F\in A\wedge X\in B\right)\to \left(F\left(X\right)=0\leftrightarrow X=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		abvf.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abvf.b	$$⊢B={\mathrm{Base}}_R$$
3		abveq0.z	$$⊢\underset{\dot{}}{0}=0_R$$
4	1	abvrcl	$$⊢F\in A\to R\in \mathrm{Ring}$$
5		eqid	$$⊢{+}_R={+}_R$$
6		eqid	$$⊢{\cdot }_R={\cdot }_R$$
7	1 2 5 6 3	isabv	$$⊢R\in \mathrm{Ring}\to \left(F\in A\leftrightarrow \left(F:B⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in B\left(\left(F\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\wedge \forall y\in B\left(F\left(x{\cdot }_{R}y\right)=F\left(x\right)F\left(y\right)\wedge F\left(x{+}_{R}y\right)\le F\left(x\right)+F\left(y\right)\right)\right)\right)\right)$$
8	4 7	syl	$$⊢F\in A\to \left(F\in A\leftrightarrow \left(F:B⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in B\left(\left(F\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\wedge \forall y\in B\left(F\left(x{\cdot }_{R}y\right)=F\left(x\right)F\left(y\right)\wedge F\left(x{+}_{R}y\right)\le F\left(x\right)+F\left(y\right)\right)\right)\right)\right)$$
9	8	ibi	$$⊢F\in A\to \left(F:B⟶\left[0,\mathrm{+\infty }\right)\wedge \forall x\in B\left(\left(F\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\wedge \forall y\in B\left(F\left(x{\cdot }_{R}y\right)=F\left(x\right)F\left(y\right)\wedge F\left(x{+}_{R}y\right)\le F\left(x\right)+F\left(y\right)\right)\right)\right)$$
10		simpl	$$⊢\left(\left(F\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\wedge \forall y\in B\left(F\left(x{\cdot }_{R}y\right)=F\left(x\right)F\left(y\right)\wedge F\left(x{+}_{R}y\right)\le F\left(x\right)+F\left(y\right)\right)\right)\to \left(F\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)$$
11	10	ralimi	$$⊢\forall x\in B\left(\left(F\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\wedge \forall y\in B\left(F\left(x{\cdot }_{R}y\right)=F\left(x\right)F\left(y\right)\wedge F\left(x{+}_{R}y\right)\le F\left(x\right)+F\left(y\right)\right)\right)\to \forall x\in B\left(F\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)$$
12	9 11	simpl2im	$$⊢F\in A\to \forall x\in B\left(F\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)$$
13		fveqeq2	$$⊢x=X\to \left(F\left(x\right)=0\leftrightarrow F\left(X\right)=0\right)$$
14		eqeq1	$$⊢x=X\to \left(x=\underset{\dot{}}{0}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
15	13 14	bibi12d	$$⊢x=X\to \left(\left(F\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\leftrightarrow \left(F\left(X\right)=0\leftrightarrow X=\underset{\dot{}}{0}\right)\right)$$
16	15	rspccva	$$⊢\left(\forall x\in B\left(F\left(x\right)=0\leftrightarrow x=\underset{\dot{}}{0}\right)\wedge X\in B\right)\to \left(F\left(X\right)=0\leftrightarrow X=\underset{\dot{}}{0}\right)$$
17	12 16	sylan	$$⊢\left(F\in A\wedge X\in B\right)\to \left(F\left(X\right)=0\leftrightarrow X=\underset{\dot{}}{0}\right)$$