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 = ( 0_g ‘ 𝑅 )
	Assertion	abveq0	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) = 0 ↔ 𝑋 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		abvf.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2		abvf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		abveq0.z	⊢ 0 = ( 0_g ‘ 𝑅 )
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 ) )