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 = ( 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		eqid	|- ( .r ` R ) = ( .r ` R )
6		drngring	|- ( R e. DivRing -> R e. Ring )
7		biid	|- ( R e. DivRing <-> R e. DivRing )
8		eldifsn	|- ( y e. ( B \ { .0. } ) <-> ( y e. B /\ y =/= .0. ) )
9		eldifsn	|- ( z e. ( B \ { .0. } ) <-> ( z e. B /\ z =/= .0. ) )
10	2 5 3	drngmcl	|- ( ( R e. DivRing /\ y e. ( B \ { .0. } ) /\ z e. ( B \ { .0. } ) ) -> ( y ( .r ` R ) z ) e. ( B \ { .0. } ) )
11	7 8 9 10	syl3anbr	|- ( ( R e. DivRing /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y ( .r ` R ) z ) e. ( B \ { .0. } ) )
12		eldifsn	|- ( ( y ( .r ` R ) z ) e. ( B \ { .0. } ) <-> ( ( y ( .r ` R ) z ) e. B /\ ( y ( .r ` R ) z ) =/= .0. ) )
13	11 12	sylib	|- ( ( R e. DivRing /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( ( y ( .r ` R ) z ) e. B /\ ( y ( .r ` R ) z ) =/= .0. ) )
14	13	simprd	|- ( ( R e. DivRing /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y ( .r ` R ) z ) =/= .0. )
15	1 2 3 4 5 6 14	abvtrivd	|- ( R e. DivRing -> F e. A )