# 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 ) )`
` |-  ( ( 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 ) ) ) ) ) ) )`
` |-  ( 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 ) ) ) ) ) ) )`
` |-  ( 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 ) ) ) ) ) ) )`
` |-  ( ph -> ( f e. ( AbsVal ` K ) <-> f e. ( AbsVal ` L ) ) )`
` |-  ( ph -> ( AbsVal ` K ) = ( AbsVal ` L ) )`