Theorem abv0

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

	Ref	Expression
Hypotheses	abv0.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
	abv0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	abv0	$$⊢F\in A\to F\left(\underset{\dot{}}{0}\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		abv0.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abv0.z	$$⊢\underset{\dot{}}{0}=0_R$$
3	1	abvrcl	$$⊢F\in A\to R\in \mathrm{Ring}$$
4		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
5	4 2	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
6	3 5	syl	$$⊢F\in A\to \underset{\dot{}}{0}\in {\mathrm{Base}}_R$$
7		eqid	$$⊢\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
8	1 4 2	abveq0	$$⊢\left(F\in A\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_R\right)\to \left(F\left(\underset{\dot{}}{0}\right)=0\leftrightarrow \underset{\dot{}}{0}=\underset{\dot{}}{0}\right)$$
9	7 8	mpbiri	$$⊢\left(F\in A\wedge \underset{\dot{}}{0}\in {\mathrm{Base}}_R\right)\to F\left(\underset{\dot{}}{0}\right)=0$$
10	6 9	mpdan	$$⊢F\in A\to F\left(\underset{\dot{}}{0}\right)=0$$