# Metamath Proof Explorer

## Theorem abvres

Description: The restriction of an absolute value to a subring is an absolute value. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses abvres.a
`|- A = ( AbsVal ` R )`
abvres.s
`|- S = ( R |`s C )`
abvres.b
`|- B = ( AbsVal ` S )`
Assertion abvres
`|- ( ( F e. A /\ C e. ( SubRing ` R ) ) -> ( F |` C ) e. B )`

### Proof

Step Hyp Ref Expression
1 abvres.a
` |-  A = ( AbsVal ` R )`
2 abvres.s
` |-  S = ( R |`s C )`
3 abvres.b
` |-  B = ( AbsVal ` S )`
4 3 a1i
` |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> B = ( AbsVal ` S ) )`
5 2 subrgbas
` |-  ( C e. ( SubRing ` R ) -> C = ( Base ` S ) )`
` |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> C = ( Base ` S ) )`
7 eqid
` |-  ( +g ` R ) = ( +g ` R )`
8 2 7 ressplusg
` |-  ( C e. ( SubRing ` R ) -> ( +g ` R ) = ( +g ` S ) )`
` |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> ( +g ` R ) = ( +g ` S ) )`
10 eqid
` |-  ( .r ` R ) = ( .r ` R )`
11 2 10 ressmulr
` |-  ( C e. ( SubRing ` R ) -> ( .r ` R ) = ( .r ` S ) )`
` |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> ( .r ` R ) = ( .r ` S ) )`
13 subrgsubg
` |-  ( C e. ( SubRing ` R ) -> C e. ( SubGrp ` R ) )`
` |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> C e. ( SubGrp ` R ) )`
15 eqid
` |-  ( 0g ` R ) = ( 0g ` R )`
16 2 15 subg0
` |-  ( C e. ( SubGrp ` R ) -> ( 0g ` R ) = ( 0g ` S ) )`
17 14 16 syl
` |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> ( 0g ` R ) = ( 0g ` S ) )`
18 2 subrgring
` |-  ( C e. ( SubRing ` R ) -> S e. Ring )`
` |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> S e. Ring )`
20 eqid
` |-  ( Base ` R ) = ( Base ` R )`
21 1 20 abvf
` |-  ( F e. A -> F : ( Base ` R ) --> RR )`
22 20 subrgss
` |-  ( C e. ( SubRing ` R ) -> C C_ ( Base ` R ) )`
23 fssres
` |-  ( ( F : ( Base ` R ) --> RR /\ C C_ ( Base ` R ) ) -> ( F |` C ) : C --> RR )`
24 21 22 23 syl2an
` |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> ( F |` C ) : C --> RR )`
25 15 subg0cl
` |-  ( C e. ( SubGrp ` R ) -> ( 0g ` R ) e. C )`
26 fvres
` |-  ( ( 0g ` R ) e. C -> ( ( F |` C ) ` ( 0g ` R ) ) = ( F ` ( 0g ` R ) ) )`
27 14 25 26 3syl
` |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> ( ( F |` C ) ` ( 0g ` R ) ) = ( F ` ( 0g ` R ) ) )`
28 1 15 abv0
` |-  ( F e. A -> ( F ` ( 0g ` R ) ) = 0 )`
` |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> ( F ` ( 0g ` R ) ) = 0 )`
30 27 29 eqtrd
` |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> ( ( F |` C ) ` ( 0g ` R ) ) = 0 )`
31 simp1l
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ x e. C /\ x =/= ( 0g ` R ) ) -> F e. A )`
` |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> C C_ ( Base ` R ) )`
33 32 sselda
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ x e. C ) -> x e. ( Base ` R ) )`
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ x e. C /\ x =/= ( 0g ` R ) ) -> x e. ( Base ` R ) )`
35 simp3
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ x e. C /\ x =/= ( 0g ` R ) ) -> x =/= ( 0g ` R ) )`
36 1 20 15 abvgt0
` |-  ( ( F e. A /\ x e. ( Base ` R ) /\ x =/= ( 0g ` R ) ) -> 0 < ( F ` x ) )`
37 31 34 35 36 syl3anc
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ x e. C /\ x =/= ( 0g ` R ) ) -> 0 < ( F ` x ) )`
38 fvres
` |-  ( x e. C -> ( ( F |` C ) ` x ) = ( F ` x ) )`
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ x e. C /\ x =/= ( 0g ` R ) ) -> ( ( F |` C ) ` x ) = ( F ` x ) )`
40 37 39 breqtrrd
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ x e. C /\ x =/= ( 0g ` R ) ) -> 0 < ( ( F |` C ) ` x ) )`
41 simp1l
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> F e. A )`
42 simp1r
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> C e. ( SubRing ` R ) )`
43 42 22 syl
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> C C_ ( Base ` R ) )`
44 simp2l
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> x e. C )`
45 43 44 sseldd
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> x e. ( Base ` R ) )`
46 simp3l
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> y e. C )`
47 43 46 sseldd
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> y e. ( Base ` R ) )`
48 1 20 10 abvmul
` |-  ( ( F e. A /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) x. ( F ` y ) ) )`
49 41 45 47 48 syl3anc
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) x. ( F ` y ) ) )`
50 10 subrgmcl
` |-  ( ( C e. ( SubRing ` R ) /\ x e. C /\ y e. C ) -> ( x ( .r ` R ) y ) e. C )`
51 42 44 46 50 syl3anc
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> ( x ( .r ` R ) y ) e. C )`
52 51 fvresd
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> ( ( F |` C ) ` ( x ( .r ` R ) y ) ) = ( F ` ( x ( .r ` R ) y ) ) )`
53 44 fvresd
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> ( ( F |` C ) ` x ) = ( F ` x ) )`
54 46 fvresd
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> ( ( F |` C ) ` y ) = ( F ` y ) )`
55 53 54 oveq12d
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> ( ( ( F |` C ) ` x ) x. ( ( F |` C ) ` y ) ) = ( ( F ` x ) x. ( F ` y ) ) )`
56 49 52 55 3eqtr4d
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> ( ( F |` C ) ` ( x ( .r ` R ) y ) ) = ( ( ( F |` C ) ` x ) x. ( ( F |` C ) ` y ) ) )`
57 1 20 7 abvtri
` |-  ( ( F e. A /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( F ` ( x ( +g ` R ) y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )`
58 41 45 47 57 syl3anc
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> ( F ` ( x ( +g ` R ) y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )`
59 7 subrgacl
` |-  ( ( C e. ( SubRing ` R ) /\ x e. C /\ y e. C ) -> ( x ( +g ` R ) y ) e. C )`
60 42 44 46 59 syl3anc
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> ( x ( +g ` R ) y ) e. C )`
61 60 fvresd
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> ( ( F |` C ) ` ( x ( +g ` R ) y ) ) = ( F ` ( x ( +g ` R ) y ) ) )`
62 53 54 oveq12d
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> ( ( ( F |` C ) ` x ) + ( ( F |` C ) ` y ) ) = ( ( F ` x ) + ( F ` y ) ) )`
63 58 61 62 3brtr4d
` |-  ( ( ( F e. A /\ C e. ( SubRing ` R ) ) /\ ( x e. C /\ x =/= ( 0g ` R ) ) /\ ( y e. C /\ y =/= ( 0g ` R ) ) ) -> ( ( F |` C ) ` ( x ( +g ` R ) y ) ) <_ ( ( ( F |` C ) ` x ) + ( ( F |` C ) ` y ) ) )`
64 4 6 9 12 17 19 24 30 40 56 63 isabvd
` |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> ( F |` C ) e. B )`