# 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 ‘ 𝑅 ) ) → ( 𝐹𝐶 ) ∈ 𝐵 )