abvcxp

Description: Raising an absolute value to a power less than one yields another absolute value. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypotheses	abvcxp.a	$⊢ A = AbsVal (R)$
	abvcxp.b	$⊢ B = {Base}_{R}$
	abvcxp.f	$⊢ G = (x \in B ⟼ {F (x)}^{S})$
Assertion	abvcxp	$⊢ (F \in A \land S \in (0, 1]) \to G \in A$

Proof

Step	Hyp	Ref	Expression
1		abvcxp.a	$⊢ A = AbsVal (R)$
2		abvcxp.b	$⊢ B = {Base}_{R}$
3		abvcxp.f	$⊢ G = (x \in B ⟼ {F (x)}^{S})$
4	1	a1i	$⊢ (F \in A \land S \in (0, 1]) \to A = AbsVal (R)$
5	2	a1i	$⊢ (F \in A \land S \in (0, 1]) \to B = {Base}_{R}$
6		eqidd	$⊢ (F \in A \land S \in (0, 1]) \to +_{R} = +_{R}$
7		eqidd	$⊢ (F \in A \land S \in (0, 1]) \to \cdot_{R} = \cdot_{R}$
8		eqidd	$⊢ (F \in A \land S \in (0, 1]) \to 0_{R} = 0_{R}$
9	1	abvrcl	$⊢ F \in A \to R \in Ring$
10	9	adantr	$⊢ (F \in A \land S \in (0, 1]) \to R \in Ring$
11	1 2	abvcl	$⊢ (F \in A \land x \in B) \to F (x) \in ℝ$
12	11	adantlr	$⊢ ((F \in A \land S \in (0, 1]) \land x \in B) \to F (x) \in ℝ$
13	1 2	abvge0	$⊢ (F \in A \land x \in B) \to 0 \leq F (x)$
14	13	adantlr	$⊢ ((F \in A \land S \in (0, 1]) \land x \in B) \to 0 \leq F (x)$
15		simpr	$⊢ (F \in A \land S \in (0, 1]) \to S \in (0, 1]$
16		0xr	$⊢ 0 \in ℝ^{*}$
17		1re	$⊢ 1 \in ℝ$
18		elioc2	$⊢ (0 \in ℝ^{*} \land 1 \in ℝ) \to (S \in (0, 1] \leftrightarrow (S \in ℝ \land 0 < S \land S \leq 1))$
19	16 17 18	mp2an	$⊢ S \in (0, 1] \leftrightarrow (S \in ℝ \land 0 < S \land S \leq 1)$
20	15 19	sylib	$⊢ (F \in A \land S \in (0, 1]) \to (S \in ℝ \land 0 < S \land S \leq 1)$
21	20	simp1d	$⊢ (F \in A \land S \in (0, 1]) \to S \in ℝ$
22	21	adantr	$⊢ ((F \in A \land S \in (0, 1]) \land x \in B) \to S \in ℝ$
23	12 14 22	recxpcld	$⊢ ((F \in A \land S \in (0, 1]) \land x \in B) \to {F (x)}^{S} \in ℝ$
24	23 3	fmptd	$⊢ (F \in A \land S \in (0, 1]) \to G : B ⟶ ℝ$
25		eqid	$⊢ 0_{R} = 0_{R}$
26	2 25	ring0cl	$⊢ R \in Ring \to 0_{R} \in B$
27	10 26	syl	$⊢ (F \in A \land S \in (0, 1]) \to 0_{R} \in B$
28		fveq2	$⊢ x = 0_{R} \to F (x) = F (0_{R})$
29	28	oveq1d	$⊢ x = 0_{R} \to {F (x)}^{S} = {F (0_{R})}^{S}$
30		ovex	$⊢ {F (0_{R})}^{S} \in V$
31	29 3 30	fvmpt	$⊢ 0_{R} \in B \to G (0_{R}) = {F (0_{R})}^{S}$
32	27 31	syl	$⊢ (F \in A \land S \in (0, 1]) \to G (0_{R}) = {F (0_{R})}^{S}$
33	1 25	abv0	$⊢ F \in A \to F (0_{R}) = 0$
34	33	adantr	$⊢ (F \in A \land S \in (0, 1]) \to F (0_{R}) = 0$
35	34	oveq1d	$⊢ (F \in A \land S \in (0, 1]) \to {F (0_{R})}^{S} = 0^{S}$
36	21	recnd	$⊢ (F \in A \land S \in (0, 1]) \to S \in ℂ$
37	20	simp2d	$⊢ (F \in A \land S \in (0, 1]) \to 0 < S$
38	37	gt0ne0d	$⊢ (F \in A \land S \in (0, 1]) \to S \neq 0$
39	36 38	0cxpd	$⊢ (F \in A \land S \in (0, 1]) \to 0^{S} = 0$
40	35 39	eqtrd	$⊢ (F \in A \land S \in (0, 1]) \to {F (0_{R})}^{S} = 0$
41	32 40	eqtrd	$⊢ (F \in A \land S \in (0, 1]) \to G (0_{R}) = 0$
42		simp1l	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to F \in A$
43		simp2	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to y \in B$
44	1 2	abvcl	$⊢ (F \in A \land y \in B) \to F (y) \in ℝ$
45	42 43 44	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to F (y) \in ℝ$
46	1 2 25	abvgt0	$⊢ (F \in A \land y \in B \land y \neq 0_{R}) \to 0 < F (y)$
47	46	3adant1r	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to 0 < F (y)$
48	45 47	elrpd	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to F (y) \in ℝ^{+}$
49	21	3ad2ant1	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to S \in ℝ$
50	48 49	rpcxpcld	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to {F (y)}^{S} \in ℝ^{+}$
51	50	rpgt0d	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to 0 < {F (y)}^{S}$
52		fveq2	$⊢ x = y \to F (x) = F (y)$
53	52	oveq1d	$⊢ x = y \to {F (x)}^{S} = {F (y)}^{S}$
54		ovex	$⊢ {F (y)}^{S} \in V$
55	53 3 54	fvmpt	$⊢ y \in B \to G (y) = {F (y)}^{S}$
56	43 55	syl	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to G (y) = {F (y)}^{S}$
57	51 56	breqtrrd	$⊢ ((F \in A \land S \in (0, 1]) \land y \in B \land y \neq 0_{R}) \to 0 < G (y)$
58		simp1l	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F \in A$
59		simp2l	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to y \in B$
60		simp3l	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to z \in B$
61		eqid	$⊢ \cdot_{R} = \cdot_{R}$
62	1 2 61	abvmul	$⊢ (F \in A \land y \in B \land z \in B) \to F (y \cdot_{R} z) = F (y) F (z)$
63	58 59 60 62	syl3anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F (y \cdot_{R} z) = F (y) F (z)$
64	63	oveq1d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y \cdot_{R} z)}^{S} = {F (y) F (z)}^{S}$
65	58 59 44	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F (y) \in ℝ$
66	1 2	abvge0	$⊢ (F \in A \land y \in B) \to 0 \leq F (y)$
67	58 59 66	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to 0 \leq F (y)$
68	1 2	abvcl	$⊢ (F \in A \land z \in B) \to F (z) \in ℝ$
69	58 60 68	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F (z) \in ℝ$
70	1 2	abvge0	$⊢ (F \in A \land z \in B) \to 0 \leq F (z)$
71	58 60 70	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to 0 \leq F (z)$
72	36	3ad2ant1	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to S \in ℂ$
73	65 67 69 71 72	mulcxpd	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y) F (z)}^{S} = {F (y)}^{S} {F (z)}^{S}$
74	64 73	eqtrd	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y \cdot_{R} z)}^{S} = {F (y)}^{S} {F (z)}^{S}$
75	10	3ad2ant1	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to R \in Ring$
76	2 61	ringcl	$⊢ (R \in Ring \land y \in B \land z \in B) \to y \cdot_{R} z \in B$
77	75 59 60 76	syl3anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to y \cdot_{R} z \in B$
78		fveq2	$⊢ x = y \cdot_{R} z \to F (x) = F (y \cdot_{R} z)$
79	78	oveq1d	$⊢ x = y \cdot_{R} z \to {F (x)}^{S} = {F (y \cdot_{R} z)}^{S}$
80		ovex	$⊢ {F (y \cdot_{R} z)}^{S} \in V$
81	79 3 80	fvmpt	$⊢ y \cdot_{R} z \in B \to G (y \cdot_{R} z) = {F (y \cdot_{R} z)}^{S}$
82	77 81	syl	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y \cdot_{R} z) = {F (y \cdot_{R} z)}^{S}$
83	59 55	syl	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y) = {F (y)}^{S}$
84		fveq2	$⊢ x = z \to F (x) = F (z)$
85	84	oveq1d	$⊢ x = z \to {F (x)}^{S} = {F (z)}^{S}$
86		ovex	$⊢ {F (z)}^{S} \in V$
87	85 3 86	fvmpt	$⊢ z \in B \to G (z) = {F (z)}^{S}$
88	60 87	syl	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (z) = {F (z)}^{S}$
89	83 88	oveq12d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y) G (z) = {F (y)}^{S} {F (z)}^{S}$
90	74 82 89	3eqtr4d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y \cdot_{R} z) = G (y) G (z)$
91		ringgrp	$⊢ R \in Ring \to R \in Grp$
92	75 91	syl	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to R \in Grp$
93		eqid	$⊢ +_{R} = +_{R}$
94	2 93	grpcl	$⊢ (R \in Grp \land y \in B \land z \in B) \to y +_{R} z \in B$
95	92 59 60 94	syl3anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to y +_{R} z \in B$
96	1 2	abvcl	$⊢ (F \in A \land y +_{R} z \in B) \to F (y +_{R} z) \in ℝ$
97	58 95 96	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F (y +_{R} z) \in ℝ$
98	1 2	abvge0	$⊢ (F \in A \land y +_{R} z \in B) \to 0 \leq F (y +_{R} z)$
99	58 95 98	syl2anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to 0 \leq F (y +_{R} z)$
100	20	3ad2ant1	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to (S \in ℝ \land 0 < S \land S \leq 1)$
101	100	simp1d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to S \in ℝ$
102	97 99 101	recxpcld	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y +_{R} z)}^{S} \in ℝ$
103	65 69	readdcld	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F (y) + F (z) \in ℝ$
104	65 69 67 71	addge0d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to 0 \leq F (y) + F (z)$
105	103 104 101	recxpcld	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {(F (y) + F (z))}^{S} \in ℝ$
106	65 67 101	recxpcld	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y)}^{S} \in ℝ$
107	69 71 101	recxpcld	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (z)}^{S} \in ℝ$
108	106 107	readdcld	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y)}^{S} + {F (z)}^{S} \in ℝ$
109	1 2 93	abvtri	$⊢ (F \in A \land y \in B \land z \in B) \to F (y +_{R} z) \leq F (y) + F (z)$
110	58 59 60 109	syl3anc	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to F (y +_{R} z) \leq F (y) + F (z)$
111	100	simp2d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to 0 < S$
112	101 111	elrpd	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to S \in ℝ^{+}$
113	97 99 103 104 112	cxple2d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to (F (y +_{R} z) \leq F (y) + F (z) \leftrightarrow {F (y +_{R} z)}^{S} \leq {(F (y) + F (z))}^{S})$
114	110 113	mpbid	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y +_{R} z)}^{S} \leq {(F (y) + F (z))}^{S}$
115	100	simp3d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to S \leq 1$
116	65 67 69 71 112 115	cxpaddle	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {(F (y) + F (z))}^{S} \leq {F (y)}^{S} + {F (z)}^{S}$
117	102 105 108 114 116	letrd	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to {F (y +_{R} z)}^{S} \leq {F (y)}^{S} + {F (z)}^{S}$
118		fveq2	$⊢ x = y +_{R} z \to F (x) = F (y +_{R} z)$
119	118	oveq1d	$⊢ x = y +_{R} z \to {F (x)}^{S} = {F (y +_{R} z)}^{S}$
120		ovex	$⊢ {F (y +_{R} z)}^{S} \in V$
121	119 3 120	fvmpt	$⊢ y +_{R} z \in B \to G (y +_{R} z) = {F (y +_{R} z)}^{S}$
122	95 121	syl	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y +_{R} z) = {F (y +_{R} z)}^{S}$
123	83 88	oveq12d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y) + G (z) = {F (y)}^{S} + {F (z)}^{S}$
124	117 122 123	3brtr4d	$⊢ ((F \in A \land S \in (0, 1]) \land (y \in B \land y \neq 0_{R}) \land (z \in B \land z \neq 0_{R})) \to G (y +_{R} z) \leq G (y) + G (z)$
125	4 5 6 7 8 10 24 41 57 90 124	isabvd	$⊢ (F \in A \land S \in (0, 1]) \to G \in A$

Metamath Proof Explorer

Theorem abvcxp

Proof