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

Metamath Proof Explorer

Theorem abveq0

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

Ref Expression
Hypotheses abvf.a ⊢ A = AbsVal ⁡ R
abvf.b ⊢ B = Base R
abveq0.z ⊢ 0 ˙ = 0 R
Assertion abveq0 ⊢ F ∈ A ∧ X ∈ B → F ⁡ X = 0 ↔ X = 0 ˙

Proof

Step Hyp Ref Expression
1 abvf.a ⊢ A = AbsVal ⁡ R
2 abvf.b ⊢ B = Base R
3 abveq0.z ⊢ 0 ˙ = 0 R
4 1 abvrcl ⊢ F ∈ A → R ∈ Ring
5 eqid ⊢ + R = + R
6 eqid ⊢ ⋅ R = ⋅ R
7 1 2 5 6 3 isabv ⊢ R ∈ Ring → F ∈ A ↔ F : B ⟶ 0 +∞ ∧ ∀ x ∈ B F ⁡ x = 0 ↔ x = 0 ˙ ∧ ∀ y ∈ B F ⁡ x ⋅ R y = F ⁡ x ⁢ F ⁡ y ∧ F ⁡ x + R y ≤ F ⁡ x + F ⁡ y
8 4 7 syl ⊢ F ∈ A → F ∈ A ↔ F : B ⟶ 0 +∞ ∧ ∀ x ∈ B F ⁡ x = 0 ↔ x = 0 ˙ ∧ ∀ 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 ˙ ∧ ∀ y ∈ B F ⁡ x ⋅ R y = F ⁡ x ⁢ F ⁡ y ∧ F ⁡ x + R y ≤ F ⁡ x + F ⁡ y
10 simpl ⊢ F ⁡ x = 0 ↔ x = 0 ˙ ∧ ∀ y ∈ B F ⁡ x ⋅ R y = F ⁡ x ⁢ F ⁡ y ∧ F ⁡ x + R y ≤ F ⁡ x + F ⁡ y → F ⁡ x = 0 ↔ x = 0 ˙
11 10 ralimi ⊢ ∀ x ∈ B F ⁡ x = 0 ↔ x = 0 ˙ ∧ ∀ y ∈ B F ⁡ x ⋅ R y = F ⁡ x ⁢ F ⁡ y ∧ F ⁡ x + R y ≤ F ⁡ x + F ⁡ y → ∀ x ∈ B F ⁡ x = 0 ↔ x = 0 ˙
12 9 11 simpl2im ⊢ F ∈ A → ∀ x ∈ B F ⁡ x = 0 ↔ x = 0 ˙
13 fveqeq2 ⊢ x = X → F ⁡ x = 0 ↔ F ⁡ X = 0
14 eqeq1 ⊢ x = X → x = 0 ˙ ↔ X = 0 ˙
15 13 14 bibi12d ⊢ x = X → F ⁡ x = 0 ↔ x = 0 ˙ ↔ F ⁡ X = 0 ↔ X = 0 ˙
16 15 rspccva ⊢ ∀ x ∈ B F ⁡ x = 0 ↔ x = 0 ˙ ∧ X ∈ B → F ⁡ X = 0 ↔ X = 0 ˙
17 12 16 sylan ⊢ F ∈ A ∧ X ∈ B → F ⁡ X = 0 ↔ X = 0 ˙