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	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
	abvtriv.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	abvtriv.z	⊢ 0 = ( 0g ‘ 𝑅 )
	abvtriv.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , 1 ) )
Assertion	abvtriv	⊢ ( 𝑅 ∈ DivRing → 𝐹 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		abvtriv.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2		abvtriv.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		abvtriv.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		abvtriv.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 0 , 0 , 1 ) )
5		drngdomn	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Domn )
6	1 2 3 4	abvtrivg	⊢ ( 𝑅 ∈ Domn → 𝐹 ∈ 𝐴 )
7	5 6	syl	⊢ ( 𝑅 ∈ DivRing → 𝐹 ∈ 𝐴 )