Theorem abvtriv

Description: The trivial absolute value. (Contributed by Mario Carneiro, 8-Sep-2014) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	abvtriv.a	|- A = ( AbsVal ` R )
	abvtriv.b	|- B = ( Base ` R )
	abvtriv.z	|- .0. = ( 0g ` R )
	abvtriv.f	|- F = ( x e. B |-> if ( x = .0. , 0 , 1 ) )
Assertion	abvtriv	|- ( R e. DivRing -> F e. A )

Proof

Step	Hyp	Ref	Expression
1		abvtriv.a	|- A = ( AbsVal ` R )
2		abvtriv.b	|- B = ( Base ` R )
3		abvtriv.z	|- .0. = ( 0g ` R )
4		abvtriv.f	|- F = ( x e. B |-> if ( x = .0. , 0 , 1 ) )
5		drngdomn	|- ( R e. DivRing -> R e. Domn )
6	1 2 3 4	abvtrivg	|- ( R e. Domn -> F e. A )
7	5 6	syl	|- ( R e. DivRing -> F e. A )