Metamath Proof Explorer

Theorem abvfval

Description: Value of the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses abvfval.a 
|- A = ( AbsVal ` R )
abvfval.b 
|- B = ( Base ` R )
abvfval.p 
|- .+ = ( +g ` R )
abvfval.t 
|- .x. = ( .r ` R )
abvfval.z 
|- .0. = ( 0g ` R )
Assertion abvfval 
|- ( R e. Ring -> A = { f e. ( ( 0 [,) +oo ) ^m B ) | A. x e. B ( ( ( f ` x ) = 0 <-> x = .0. ) /\ A. y e. B ( ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x .+ y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 abvfval.a 
 |-  A = ( AbsVal ` R )
2 abvfval.b 
 |-  B = ( Base ` R )
3 abvfval.p 
 |-  .+ = ( +g ` R )
4 abvfval.t 
 |-  .x. = ( .r ` R )
5 abvfval.z 
 |-  .0. = ( 0g ` R )
6 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
7 6 2 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
8 7 oveq2d 
 |-  ( r = R -> ( ( 0 [,) +oo ) ^m ( Base ` r ) ) = ( ( 0 [,) +oo ) ^m B ) )
9 fveq2 
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
10 9 5 eqtr4di 
 |-  ( r = R -> ( 0g ` r ) = .0. )
11 10 eqeq2d 
 |-  ( r = R -> ( x = ( 0g ` r ) <-> x = .0. ) )
12 11 bibi2d 
 |-  ( r = R -> ( ( ( f ` x ) = 0 <-> x = ( 0g ` r ) ) <-> ( ( f ` x ) = 0 <-> x = .0. ) ) )
13 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
14 13 4 eqtr4di 
 |-  ( r = R -> ( .r ` r ) = .x. )
15 14 oveqd 
 |-  ( r = R -> ( x ( .r ` r ) y ) = ( x .x. y ) )
16 15 fveqeq2d 
 |-  ( r = R -> ( ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) <-> ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) ) )
17 fveq2 
 |-  ( r = R -> ( +g ` r ) = ( +g ` R ) )
18 17 3 eqtr4di 
 |-  ( r = R -> ( +g ` r ) = .+ )
19 18 oveqd 
 |-  ( r = R -> ( x ( +g ` r ) y ) = ( x .+ y ) )
20 19 fveq2d 
 |-  ( r = R -> ( f ` ( x ( +g ` r ) y ) ) = ( f ` ( x .+ y ) ) )
21 20 breq1d 
 |-  ( r = R -> ( ( f ` ( x ( +g ` r ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) <-> ( f ` ( x .+ y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) )
22 16 21 anbi12d 
 |-  ( r = R -> ( ( ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` r ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) <-> ( ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x .+ y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) )
23 7 22 raleqbidv 
 |-  ( r = 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 ) ) ) <-> A. y e. B ( ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x .+ y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) )
24 12 23 anbi12d 
 |-  ( r = 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 ) ) ) ) <-> ( ( ( f ` x ) = 0 <-> x = .0. ) /\ A. y e. B ( ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x .+ y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) )
25 7 24 raleqbidv 
 |-  ( r = 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 ) ) ) ) <-> A. x e. B ( ( ( f ` x ) = 0 <-> x = .0. ) /\ A. y e. B ( ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x .+ y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) )
26 8 25 rabeqbidv 
 |-  ( r = R -> { 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 ) ) ) ) } = { f e. ( ( 0 [,) +oo ) ^m B ) | A. x e. B ( ( ( f ` x ) = 0 <-> x = .0. ) /\ A. y e. B ( ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x .+ y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) } )
27 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 ) ) ) ) } )
28 ovex 
 |-  ( ( 0 [,) +oo ) ^m B ) e. _V
29 28 rabex 
 |-  { f e. ( ( 0 [,) +oo ) ^m B ) | A. x e. B ( ( ( f ` x ) = 0 <-> x = .0. ) /\ A. y e. B ( ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x .+ y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) } e. _V
30 26 27 29 fvmpt 
 |-  ( R e. Ring -> ( AbsVal ` R ) = { f e. ( ( 0 [,) +oo ) ^m B ) | A. x e. B ( ( ( f ` x ) = 0 <-> x = .0. ) /\ A. y e. B ( ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x .+ y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) } )
31 1 30 syl5eq 
 |-  ( R e. Ring -> A = { f e. ( ( 0 [,) +oo ) ^m B ) | A. x e. B ( ( ( f ` x ) = 0 <-> x = .0. ) /\ A. y e. B ( ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x .+ y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) } )