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 ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
abvres.s ⊢ 𝑆 = ( 𝑅 ↾s 𝐶 )
abvres.b ⊢ 𝐵 = ( AbsVal ‘ 𝑆 )
Assertion abvres ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝐹 ↾ 𝐶 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 abvres.a ⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2 abvres.s ⊢ 𝑆 = ( 𝑅 ↾s 𝐶 )
3 abvres.b ⊢ 𝐵 = ( AbsVal ‘ 𝑆 )
4 3 a1i ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐵 = ( AbsVal ‘ 𝑆 ) )
5 2 subrgbas ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝑅 ) → 𝐶 = ( Base ‘ 𝑆 ) )
6 5 adantl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐶 = ( Base ‘ 𝑆 ) )
7 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
8 2 7 ressplusg ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝑅 ) → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑆 ) )
9 8 adantl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑆 ) )
10 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11 2 10 ressmulr ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝑅 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
12 11 adantl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝑆 ) )
13 subrgsubg ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝑅 ) → 𝐶 ∈ ( SubGrp ‘ 𝑅 ) )
14 13 adantl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐶 ∈ ( SubGrp ‘ 𝑅 ) )
15 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
16 2 15 subg0 ⊢ ( 𝐶 ∈ ( SubGrp ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑆 ) )
17 14 16 syl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑆 ) )
18 2 subrgring ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝑅 ) → 𝑆 ∈ Ring )
19 18 adantl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑆 ∈ Ring )
20 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
21 1 20 abvf ⊢ ( 𝐹 ∈ 𝐴 → 𝐹 : ( Base ‘ 𝑅 ) ⟶ ℝ )
22 20 subrgss ⊢ ( 𝐶 ∈ ( SubRing ‘ 𝑅 ) → 𝐶 ⊆ ( Base ‘ 𝑅 ) )
23 fssres ⊢ ( ( 𝐹 : ( Base ‘ 𝑅 ) ⟶ ℝ ∧ 𝐶 ⊆ ( Base ‘ 𝑅 ) ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ ℝ )
24 21 22 23 syl2an ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ ℝ )
25 15 subg0cl ⊢ ( 𝐶 ∈ ( SubGrp ‘ 𝑅 ) → ( 0g ‘ 𝑅 ) ∈ 𝐶 )
26 fvres ⊢ ( ( 0g ‘ 𝑅 ) ∈ 𝐶 → ( ( 𝐹 ↾ 𝐶 ) ‘ ( 0g ‘ 𝑅 ) ) = ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) )
27 14 25 26 3syl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → ( ( 𝐹 ↾ 𝐶 ) ‘ ( 0g ‘ 𝑅 ) ) = ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) )
28 1 15 abv0 ⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = 0 )
29 28 adantr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 0g ‘ 𝑅 ) ) = 0 )
30 27 29 eqtrd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → ( ( 𝐹 ↾ 𝐶 ) ‘ ( 0g ‘ 𝑅 ) ) = 0 )
31 simp1l ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) → 𝐹 ∈ 𝐴 )
32 22 adantl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → 𝐶 ⊆ ( Base ‘ 𝑅 ) )
33 32 sselda ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐶 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
34 33 3adant3 ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
35 simp3 ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) → 𝑥 ≠ ( 0g ‘ 𝑅 ) )
36 1 20 15 abvgt0 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) → 0 < ( 𝐹 ‘ 𝑥 ) )
37 31 34 35 36 syl3anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) → 0 < ( 𝐹 ‘ 𝑥 ) )
38 fvres ⊢ ( 𝑥 ∈ 𝐶 → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
39 38 3ad2ant2 ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
40 37 39 breqtrrd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) → 0 < ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) )
41 simp1l ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝐹 ∈ 𝐴 )
42 simp1r ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝐶 ∈ ( SubRing ‘ 𝑅 ) )
43 42 22 syl ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝐶 ⊆ ( Base ‘ 𝑅 ) )
44 simp2l ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑥 ∈ 𝐶 )
45 43 44 sseldd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
46 simp3l ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑦 ∈ 𝐶 )
47 43 46 sseldd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
48 1 20 10 abvmul ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) )
49 41 45 47 48 syl3anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) )
50 10 subrgmcl ⊢ ( ( 𝐶 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐶 )
51 42 44 46 50 syl3anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐶 )
52 51 fvresd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ↾ 𝐶 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) )
53 44 fvresd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
54 46 fvresd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
55 53 54 oveq12d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) · ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) · ( 𝐹 ‘ 𝑦 ) ) )
56 49 52 55 3eqtr4d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ↾ 𝐶 ) ‘ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) · ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ) )
57 1 20 7 abvtri ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
58 41 45 47 57 syl3anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
59 7 subrgacl ⊢ ( ( 𝐶 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶 ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐶 )
60 42 44 46 59 syl3anc ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐶 )
61 60 fvresd ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ↾ 𝐶 ) ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) )
62 53 54 oveq12d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) + ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) + ( 𝐹 ‘ 𝑦 ) ) )
63 58 61 62 3brtr4d ⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 ≠ ( 0g ‘ 𝑅 ) ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑦 ≠ ( 0g ‘ 𝑅 ) ) ) → ( ( 𝐹 ↾ 𝐶 ) ‘ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) ≤ ( ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑥 ) + ( ( 𝐹 ↾ 𝐶 ) ‘ 𝑦 ) ) )
64 4 6 9 12 17 19 24 30 40 56 63 isabvd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝐶 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝐹 ↾ 𝐶 ) ∈ 𝐵 )