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	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
	abv1.p	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	abv1	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴 ) → ( 𝐹 ‘ 1 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		abv0.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2		abv1.p	⊢ 1 = ( 1r ‘ 𝑅 )
3		id	⊢ ( 𝐹 ∈ 𝐴 → 𝐹 ∈ 𝐴 )
4		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
5	4 2	drngunz	⊢ ( 𝑅 ∈ DivRing → 1 ≠ ( 0g ‘ 𝑅 ) )
6	1 2 4	abv1z	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐹 ‘ 1 ) = 1 )
7	3 5 6	syl2anr	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐴 ) → ( 𝐹 ‘ 1 ) = 1 )