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

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 ⊢ A = AbsVal ⁡ R
abvf.b ⊢ B = Base R
Assertion abvfge0 ⊢ F ∈ A → F : B ⟶ 0 +∞

Proof

Step Hyp Ref Expression
1 abvf.a ⊢ A = AbsVal ⁡ R
2 abvf.b ⊢ B = Base R
3 1 abvrcl ⊢ F ∈ A → R ∈ Ring
4 eqid ⊢ + R = + R
5 eqid ⊢ ⋅ R = ⋅ R
6 eqid ⊢ 0 R = 0 R
7 1 2 4 5 6 isabv ⊢ R ∈ Ring → F ∈ A ↔ F : B ⟶ 0 +∞ ∧ ∀ x ∈ B F ⁡ x = 0 ↔ x = 0 R ∧ ∀ y ∈ B F ⁡ x ⋅ R y = F ⁡ x ⁢ F ⁡ y ∧ F ⁡ x + R y ≤ F ⁡ x + F ⁡ y
8 3 7 syl ⊢ F ∈ A → F ∈ A ↔ F : B ⟶ 0 +∞ ∧ ∀ x ∈ B F ⁡ x = 0 ↔ x = 0 R ∧ ∀ y ∈ B F ⁡ x ⋅ R y = F ⁡ x ⁢ F ⁡ y ∧ F ⁡ x + R y ≤ F ⁡ x + F ⁡ y
9 8 ibi ⊢ F ∈ A → F : B ⟶ 0 +∞ ∧ ∀ x ∈ B F ⁡ x = 0 ↔ x = 0 R ∧ ∀ y ∈ B F ⁡ x ⋅ R y = F ⁡ x ⁢ F ⁡ y ∧ F ⁡ x + R y ≤ F ⁡ x + F ⁡ y
10 9 simpld ⊢ F ∈ A → F : B ⟶ 0 +∞