Theorem abv0

Description: The absolute value of zero is zero. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypotheses	abv0.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
	abv0.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	abv0	⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 0 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		abv0.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2		abv0.z	⊢ 0 = ( 0g ‘ 𝑅 )
3	1	abvrcl	⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Ring )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5	4 2	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
6	3 5	syl	⊢ ( 𝐹 ∈ 𝐴 → 0 ∈ ( Base ‘ 𝑅 ) )
7		eqid	⊢ 0 = 0
8	1 4 2	abveq0	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 0 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐹 ‘ 0 ) = 0 ↔ 0 = 0 ) )
9	7 8	mpbiri	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 0 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ 0 ) = 0 )
10	6 9	mpdan	⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ 0 ) = 0 )