# Metamath Proof Explorer

## Theorem abvfge0

Description: An absolute value is a function from the ring to the nonnegative real numbers. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses abvf.a 𝐴 = ( AbsVal ‘ 𝑅 )
abvf.b 𝐵 = ( Base ‘ 𝑅 )
Assertion abvfge0 ( 𝐹𝐴𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) )

### Proof

Step Hyp Ref Expression
1 abvf.a 𝐴 = ( AbsVal ‘ 𝑅 )
2 abvf.b 𝐵 = ( Base ‘ 𝑅 )
3 1 abvrcl ( 𝐹𝐴𝑅 ∈ Ring )
4 eqid ( +g𝑅 ) = ( +g𝑅 )
5 eqid ( .r𝑅 ) = ( .r𝑅 )
6 eqid ( 0g𝑅 ) = ( 0g𝑅 )
7 1 2 4 5 6 isabv ( 𝑅 ∈ Ring → ( 𝐹𝐴 ↔ ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥𝐵 ( ( ( 𝐹𝑥 ) = 0 ↔ 𝑥 = ( 0g𝑅 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝐹 ‘ ( 𝑥 ( .r𝑅 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹𝑥 ) + ( 𝐹𝑦 ) ) ) ) ) ) )
8 3 7 syl ( 𝐹𝐴 → ( 𝐹𝐴 ↔ ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥𝐵 ( ( ( 𝐹𝑥 ) = 0 ↔ 𝑥 = ( 0g𝑅 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝐹 ‘ ( 𝑥 ( .r𝑅 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹𝑥 ) + ( 𝐹𝑦 ) ) ) ) ) ) )
9 8 ibi ( 𝐹𝐴 → ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥𝐵 ( ( ( 𝐹𝑥 ) = 0 ↔ 𝑥 = ( 0g𝑅 ) ) ∧ ∀ 𝑦𝐵 ( ( 𝐹 ‘ ( 𝑥 ( .r𝑅 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) · ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹𝑥 ) + ( 𝐹𝑦 ) ) ) ) ) )
10 9 simpld ( 𝐹𝐴𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) )