Theorem abv1

Description: The absolute value of one is one in a division ring. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypotheses	abv0.a	|- A = ( AbsVal ` R )
	abv1.p	|- .1. = ( 1r ` R )
Assertion	abv1	|- ( ( R e. DivRing /\ F e. A ) -> ( F ` .1. ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		abv0.a	|- A = ( AbsVal ` R )
2		abv1.p	|- .1. = ( 1r ` R )
3		id	|- ( F e. A -> F e. A )
4		eqid	|- ( 0g ` R ) = ( 0g ` R )
5	4 2	drngunz	|- ( R e. DivRing -> .1. =/= ( 0g ` R ) )
6	1 2 4	abv1z	|- ( ( F e. A /\ .1. =/= ( 0g ` R ) ) -> ( F ` .1. ) = 1 )
7	3 5 6	syl2anr	|- ( ( R e. DivRing /\ F e. A ) -> ( F ` .1. ) = 1 )