Theorem abv0

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

	Ref	Expression
Hypotheses	abv0.a	|- A = ( AbsVal ` R )
	abv0.z	|- .0. = ( 0g ` R )
Assertion	abv0	|- ( F e. A -> ( F ` .0. ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		abv0.a	|- A = ( AbsVal ` R )
2		abv0.z	|- .0. = ( 0g ` R )
3	1	abvrcl	|- ( F e. A -> R e. Ring )
4		eqid	|- ( Base ` R ) = ( Base ` R )
5	4 2	ring0cl	|- ( R e. Ring -> .0. e. ( Base ` R ) )
6	3 5	syl	|- ( F e. A -> .0. e. ( Base ` R ) )
7		eqid	|- .0. = .0.
8	1 4 2	abveq0	|- ( ( F e. A /\ .0. e. ( Base ` R ) ) -> ( ( F ` .0. ) = 0 <-> .0. = .0. ) )
9	7 8	mpbiri	|- ( ( F e. A /\ .0. e. ( Base ` R ) ) -> ( F ` .0. ) = 0 )
10	6 9	mpdan	|- ( F e. A -> ( F ` .0. ) = 0 )