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