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 ) )
6 5 adantl 
 |-  ( ( 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 ) )
9 8 adantl 
 |-  ( ( 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 ) )
12 11 adantl 
 |-  ( ( F e. A /\ C e. ( SubRing ` R ) ) -> ( .r ` R ) = ( .r ` S ) )
13 subrgsubg 
 |-  ( C e. ( SubRing ` R ) -> C e. ( SubGrp ` R ) )
14 13 adantl 
 |-  ( ( 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 )
19 18 adantl 
 |-  ( ( 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 )
29 28 adantr 
 |-  ( ( 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 )
32 22 adantl 
 |-  ( ( 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 ) )
34 33 3adant3 
 |-  ( ( ( 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 ) )
39 38 3ad2ant2 
 |-  ( ( ( 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 )