Theorem abvtriv

Description: The trivial absolute value. (Contributed by Mario Carneiro, 8-Sep-2014) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	abvtriv.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
	abvtriv.b	$$⊢B={\mathrm{Base}}_R$$
	abvtriv.z	$$⊢\underset{\dot{}}{0}=0_R$$
	abvtriv.f	$$⊢F=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,1\right)\right)$$
Assertion	abvtriv	$$⊢R\in \mathrm{DivRing}\to F\in A$$

Proof

Step	Hyp	Ref	Expression
1		abvtriv.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abvtriv.b	$$⊢B={\mathrm{Base}}_R$$
3		abvtriv.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		abvtriv.f	$$⊢F=\left(x\in B⟼if\left(x=\underset{\dot{}}{0},0,1\right)\right)$$
5		drngdomn	$$⊢R\in \mathrm{DivRing}\to R\in \mathrm{Domn}$$
6	1 2 3 4	abvtrivg	$$⊢R\in \mathrm{Domn}\to F\in A$$
7	5 6	syl	$$⊢R\in \mathrm{DivRing}\to F\in A$$