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 bitrdi 
 |-  ( 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 ) ) ) ) ) ) )