# Metamath Proof Explorer

## Theorem isabv

Description: Elementhood in 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 isabv
`|- ( R e. Ring -> ( F e. A <-> ( F : B --> ( 0 [,) +oo ) /\ 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 1 2 3 4 5 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 ) ) ) ) } )`
7 6 eleq2d
` |-  ( R e. Ring -> ( F e. A <-> F e. { 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 ) ) ) ) } ) )`
8 fveq1
` |-  ( f = F -> ( f ` x ) = ( F ` x ) )`
9 8 eqeq1d
` |-  ( f = F -> ( ( f ` x ) = 0 <-> ( F ` x ) = 0 ) )`
10 9 bibi1d
` |-  ( f = F -> ( ( ( f ` x ) = 0 <-> x = .0. ) <-> ( ( F ` x ) = 0 <-> x = .0. ) ) )`
11 fveq1
` |-  ( f = F -> ( f ` ( x .x. y ) ) = ( F ` ( x .x. y ) ) )`
12 fveq1
` |-  ( f = F -> ( f ` y ) = ( F ` y ) )`
13 8 12 oveq12d
` |-  ( f = F -> ( ( f ` x ) x. ( f ` y ) ) = ( ( F ` x ) x. ( F ` y ) ) )`
14 11 13 eqeq12d
` |-  ( f = F -> ( ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) <-> ( F ` ( x .x. y ) ) = ( ( F ` x ) x. ( F ` y ) ) ) )`
15 fveq1
` |-  ( f = F -> ( f ` ( x .+ y ) ) = ( F ` ( x .+ y ) ) )`
16 8 12 oveq12d
` |-  ( f = F -> ( ( f ` x ) + ( f ` y ) ) = ( ( F ` x ) + ( F ` y ) ) )`
17 15 16 breq12d
` |-  ( f = F -> ( ( f ` ( x .+ y ) ) <_ ( ( f ` x ) + ( f ` y ) ) <-> ( F ` ( x .+ y ) ) <_ ( ( F ` x ) + ( F ` y ) ) ) )`
18 14 17 anbi12d
` |-  ( f = F -> ( ( ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x .+ y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) <-> ( ( F ` ( x .x. y ) ) = ( ( F ` x ) x. ( F ` y ) ) /\ ( F ` ( x .+ y ) ) <_ ( ( F ` x ) + ( F ` y ) ) ) ) )`
19 18 ralbidv
` |-  ( f = F -> ( A. y e. B ( ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x .+ 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 ) ) ) ) )`
20 10 19 anbi12d
` |-  ( f = F -> ( ( ( ( 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 ) ) ) ) <-> ( ( ( 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 ) ) ) ) ) )`
21 20 ralbidv
` |-  ( f = F -> ( 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 ) ) ) ) <-> 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 ) ) ) ) ) )`
22 21 elrab
` |-  ( F e. { 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 ) ) ) ) } <-> ( 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 ) ) ) ) ) )`
23 ovex
` |-  ( 0 [,) +oo ) e. _V`
24 2 fvexi
` |-  B e. _V`
25 23 24 elmap
` |-  ( F e. ( ( 0 [,) +oo ) ^m B ) <-> F : B --> ( 0 [,) +oo ) )`
26 25 anbi1i
` |-  ( ( 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 ) ) ) ) ) <-> ( F : B --> ( 0 [,) +oo ) /\ 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 22 26 bitri
` |-  ( F e. { 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 ) ) ) ) } <-> ( F : B --> ( 0 [,) +oo ) /\ 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 ) ) ) ) ) )`
28 7 27 syl6bb
` |-  ( R e. Ring -> ( F e. A <-> ( F : B --> ( 0 [,) +oo ) /\ 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 ) ) ) ) ) ) )`