This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	abv1	$⊢ (R \in DivRing \land F \in A) \to F (\underset{˙}{1}) = 1$

Step	Hyp	Ref	Expression
1		abv0.a	$⊢ A = AbsVal (R)$
2		abv1.p	$⊢ \underset{˙}{1} = 1_{R}$
3		id	$⊢ F \in A \to F \in A$
4		eqid	$⊢ 0_{R} = 0_{R}$
5	4 2	drngunz	$⊢ R \in DivRing \to \underset{˙}{1} \neq 0_{R}$
6	1 2 4	abv1z	$⊢ (F \in A \land \underset{˙}{1} \neq 0_{R}) \to F (\underset{˙}{1}) = 1$
7	3 5 6	syl2anr	$⊢ (R \in DivRing \land F \in A) \to F (\underset{˙}{1}) = 1$