Theorem abvrcl

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

	Ref	Expression
Hypothesis	abvf.a	|- A = ( AbsVal ` R )
Assertion	abvrcl	|- ( F e. A -> R e. Ring )

Proof

Step	Hyp	Ref	Expression
1		abvf.a	|- A = ( AbsVal ` R )
2		df-abv	|- AbsVal = ( r e. Ring |-> { f e. ( ( 0 [,) +oo ) ^m ( Base ` r ) ) | A. x e. ( Base ` r ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` r ) ) /\ A. y e. ( Base ` r ) ( ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` r ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) } )
3	2	mptrcl	|- ( F e. ( AbsVal ` R ) -> R e. Ring )
4	3 1	eleq2s	|- ( F e. A -> R e. Ring )