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 ↾_{𝑠} C$
	abvres.b	$⊢ B = AbsVal (S)$
Assertion	abvres	$⊢ (F \in A \land C \in SubRing (R)) \to {F ↾}_{C} \in B$

Proof

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

Metamath Proof Explorer

Theorem abvres

Proof