Metamath Proof Explorer

Theorem abvpropd

Description: If two structures have the same ring components, they have the same collection of absolute values. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses abvpropd.1 
|- ( ph -> B = ( Base ` K ) )
abvpropd.2 
|- ( ph -> B = ( Base ` L ) )
abvpropd.3 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
abvpropd.4 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
Assertion abvpropd 
|- ( ph -> ( AbsVal ` K ) = ( AbsVal ` L ) )

Proof

Step Hyp Ref Expression
1 abvpropd.1 
 |-  ( ph -> B = ( Base ` K ) )
2 abvpropd.2 
 |-  ( ph -> B = ( Base ` L ) )
3 abvpropd.3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4 abvpropd.4 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
5 1 2 3 4 ringpropd 
 |-  ( ph -> ( K e. Ring <-> L e. Ring ) )
6 1 2 eqtr3d 
 |-  ( ph -> ( Base ` K ) = ( Base ` L ) )
7 6 feq2d 
 |-  ( ph -> ( f : ( Base ` K ) --> ( 0 [,) +oo ) <-> f : ( Base ` L ) --> ( 0 [,) +oo ) ) )
8 1 2 3 grpidpropd 
 |-  ( ph -> ( 0g ` K ) = ( 0g ` L ) )
9 8 adantr 
 |-  ( ( ph /\ x e. B ) -> ( 0g ` K ) = ( 0g ` L ) )
10 9 eqeq2d 
 |-  ( ( ph /\ x e. B ) -> ( x = ( 0g ` K ) <-> x = ( 0g ` L ) ) )
11 10 bibi2d 
 |-  ( ( ph /\ x e. B ) -> ( ( ( f ` x ) = 0 <-> x = ( 0g ` K ) ) <-> ( ( f ` x ) = 0 <-> x = ( 0g ` L ) ) ) )
12 4 fveqeq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) <-> ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) ) )
13 3 fveq2d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( f ` ( x ( +g ` K ) y ) ) = ( f ` ( x ( +g ` L ) y ) ) )
14 13 breq1d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) <-> ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) )
15 12 14 anbi12d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) <-> ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) )
16 15 anassrs 
 |-  ( ( ( ph /\ x e. B ) /\ y e. B ) -> ( ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) <-> ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) )
17 16 ralbidva 
 |-  ( ( ph /\ x e. B ) -> ( A. y e. B ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) <-> A. y e. B ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) )
18 11 17 anbi12d 
 |-  ( ( ph /\ x e. B ) -> ( ( ( ( f ` x ) = 0 <-> x = ( 0g ` K ) ) /\ A. y e. B ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) <-> ( ( ( f ` x ) = 0 <-> x = ( 0g ` L ) ) /\ A. y e. B ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) )
19 18 ralbidva 
 |-  ( ph -> ( A. x e. B ( ( ( f ` x ) = 0 <-> x = ( 0g ` K ) ) /\ A. y e. B ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) <-> A. x e. B ( ( ( f ` x ) = 0 <-> x = ( 0g ` L ) ) /\ A. y e. B ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) )
20 1 raleqdv 
 |-  ( ph -> ( A. y e. B ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) <-> A. y e. ( Base ` K ) ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) )
21 20 anbi2d 
 |-  ( ph -> ( ( ( ( f ` x ) = 0 <-> x = ( 0g ` K ) ) /\ A. y e. B ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) <-> ( ( ( f ` x ) = 0 <-> x = ( 0g ` K ) ) /\ A. y e. ( Base ` K ) ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) )
22 1 21 raleqbidv 
 |-  ( ph -> ( A. x e. B ( ( ( f ` x ) = 0 <-> x = ( 0g ` K ) ) /\ A. y e. B ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) <-> A. x e. ( Base ` K ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` K ) ) /\ A. y e. ( Base ` K ) ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) )
23 2 raleqdv 
 |-  ( ph -> ( A. y e. B ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) <-> A. y e. ( Base ` L ) ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) )
24 23 anbi2d 
 |-  ( ph -> ( ( ( ( f ` x ) = 0 <-> x = ( 0g ` L ) ) /\ A. y e. B ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) <-> ( ( ( f ` x ) = 0 <-> x = ( 0g ` L ) ) /\ A. y e. ( Base ` L ) ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) )
25 2 24 raleqbidv 
 |-  ( ph -> ( A. x e. B ( ( ( f ` x ) = 0 <-> x = ( 0g ` L ) ) /\ A. y e. B ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) <-> A. x e. ( Base ` L ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` L ) ) /\ A. y e. ( Base ` L ) ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) )
26 19 22 25 3bitr3d 
 |-  ( ph -> ( A. x e. ( Base ` K ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` K ) ) /\ A. y e. ( Base ` K ) ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) <-> A. x e. ( Base ` L ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` L ) ) /\ A. y e. ( Base ` L ) ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) )
27 7 26 anbi12d 
 |-  ( ph -> ( ( f : ( Base ` K ) --> ( 0 [,) +oo ) /\ A. x e. ( Base ` K ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` K ) ) /\ A. y e. ( Base ` K ) ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) <-> ( f : ( Base ` L ) --> ( 0 [,) +oo ) /\ A. x e. ( Base ` L ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` L ) ) /\ A. y e. ( Base ` L ) ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) ) )
28 5 27 anbi12d 
 |-  ( ph -> ( ( K e. Ring /\ ( f : ( Base ` K ) --> ( 0 [,) +oo ) /\ A. x e. ( Base ` K ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` K ) ) /\ A. y e. ( Base ` K ) ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) ) <-> ( L e. Ring /\ ( f : ( Base ` L ) --> ( 0 [,) +oo ) /\ A. x e. ( Base ` L ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` L ) ) /\ A. y e. ( Base ` L ) ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) ) ) )
29 eqid 
 |-  ( AbsVal ` K ) = ( AbsVal ` K )
30 29 abvrcl 
 |-  ( f e. ( AbsVal ` K ) -> K e. Ring )
31 eqid 
 |-  ( Base ` K ) = ( Base ` K )
32 eqid 
 |-  ( +g ` K ) = ( +g ` K )
33 eqid 
 |-  ( .r ` K ) = ( .r ` K )
34 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
35 29 31 32 33 34 isabv 
 |-  ( K e. Ring -> ( f e. ( AbsVal ` K ) <-> ( f : ( Base ` K ) --> ( 0 [,) +oo ) /\ A. x e. ( Base ` K ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` K ) ) /\ A. y e. ( Base ` K ) ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) ) )
36 30 35 biadanii 
 |-  ( f e. ( AbsVal ` K ) <-> ( K e. Ring /\ ( f : ( Base ` K ) --> ( 0 [,) +oo ) /\ A. x e. ( Base ` K ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` K ) ) /\ A. y e. ( Base ` K ) ( ( f ` ( x ( .r ` K ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` K ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) ) )
37 eqid 
 |-  ( AbsVal ` L ) = ( AbsVal ` L )
38 37 abvrcl 
 |-  ( f e. ( AbsVal ` L ) -> L e. Ring )
39 eqid 
 |-  ( Base ` L ) = ( Base ` L )
40 eqid 
 |-  ( +g ` L ) = ( +g ` L )
41 eqid 
 |-  ( .r ` L ) = ( .r ` L )
42 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
43 37 39 40 41 42 isabv 
 |-  ( L e. Ring -> ( f e. ( AbsVal ` L ) <-> ( f : ( Base ` L ) --> ( 0 [,) +oo ) /\ A. x e. ( Base ` L ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` L ) ) /\ A. y e. ( Base ` L ) ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) ) )
44 38 43 biadanii 
 |-  ( f e. ( AbsVal ` L ) <-> ( L e. Ring /\ ( f : ( Base ` L ) --> ( 0 [,) +oo ) /\ A. x e. ( Base ` L ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` L ) ) /\ A. y e. ( Base ` L ) ( ( f ` ( x ( .r ` L ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` L ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) ) ) )
45 28 36 44 3bitr4g 
 |-  ( ph -> ( f e. ( AbsVal ` K ) <-> f e. ( AbsVal ` L ) ) )
46 45 eqrdv 
 |-  ( ph -> ( AbsVal ` K ) = ( AbsVal ` L ) )