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=\mathrm{AbsVal}\left(R\right)$$
	abv1.p	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	abv1	$$⊢\left(R\in \mathrm{DivRing}\wedge F\in A\right)\to F\left(\underset{\dot{}}{1}\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		abv0.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abv1.p	$$⊢\underset{\dot{}}{1}=1_R$$
3		id	$$⊢F\in A\to F\in A$$
4		eqid	$$⊢0_R=0_R$$
5	4 2	drngunz	$$⊢R\in \mathrm{DivRing}\to \underset{\dot{}}{1}\ne 0_R$$
6	1 2 4	abv1z	$$⊢\left(F\in A\wedge \underset{\dot{}}{1}\ne 0_R\right)\to F\left(\underset{\dot{}}{1}\right)=1$$
7	3 5 6	syl2anr	$$⊢\left(R\in \mathrm{DivRing}\wedge F\in A\right)\to F\left(\underset{\dot{}}{1}\right)=1$$