# 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 ) )