Theorem abvrcl

Description: Reverse closure for the absolute value set. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypothesis	abvf.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
Assertion	abvrcl	⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		abvf.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2		df-abv	⊢ AbsVal = ( 𝑟 ∈ Ring ↦ { 𝑓 ∈ ( ( 0 [,) +∞ ) ↑m ( Base ‘ 𝑟 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ( ( ( 𝑓 ‘ 𝑥 ) = 0 ↔ 𝑥 = ( 0g ‘ 𝑟 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) · ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) ≤ ( ( 𝑓 ‘ 𝑥 ) + ( 𝑓 ‘ 𝑦 ) ) ) ) } )
3	2	mptrcl	⊢ ( 𝐹 ∈ ( AbsVal ‘ 𝑅 ) → 𝑅 ∈ Ring )
4	3 1	eleq2s	⊢ ( 𝐹 ∈ 𝐴 → 𝑅 ∈ Ring )