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 ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
abvf.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
abveq0.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion abveq0 ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) = 0 ↔ 𝑋 = 0 ) )

Proof

Step Hyp Ref Expression
1 abvf.a ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2 abvf.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 abveq0.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 1 abvrcl ⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Ring )
5 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
6 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7 1 2 5 6 3 isabv ⊢ ( 𝑅 ∈ Ring → ( 𝐹 ∈ 𝐴 ↔ ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) ) )
8 4 7 syl ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ∈ 𝐴 ↔ ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) ) )
9 8 ibi ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 : 𝐵 ⟶ ( 0 [,) +∞ ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
10 simpl ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
11 10 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) ) ) → ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
12 9 11 simpl2im ⊢ ( 𝐹 ∈ 𝐴 → ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
13 fveqeq2 ⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ ( 𝐹 ‘ 𝑋 ) = 0 ) )
14 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 0 ↔ 𝑋 = 0 ) )
15 13 14 bibi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ↔ ( ( 𝐹 ‘ 𝑋 ) = 0 ↔ 𝑋 = 0 ) ) )
16 15 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) = 0 ↔ 𝑋 = 0 ) )
17 12 16 sylan ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) = 0 ↔ 𝑋 = 0 ) )