evthiccabs

Description: Extreme Value Theorem on y closed interval, for the absolute value of y continuous function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	evthiccabs.a	$⊢ φ \to A \in ℝ$
	evthiccabs.b	$⊢ φ \to B \in ℝ$
	evthiccabs.aleb	$⊢ φ \to A \leq B$
	evthiccabs.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
Assertion	evthiccabs	$⊢ φ \to (\exists x \in [A, B] \forall y \in [A, B] \|F (y)\| \leq \|F (x)\| \land \exists z \in [A, B] \forall w \in [A, B] \|F (z)\| \leq \|F (w)\|)$

Proof

Step	Hyp	Ref	Expression
1		evthiccabs.a	$⊢ φ \to A \in ℝ$
2		evthiccabs.b	$⊢ φ \to B \in ℝ$
3		evthiccabs.aleb	$⊢ φ \to A \leq B$
4		evthiccabs.f	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℝ$
5		ax-resscn	$⊢ ℝ \subseteq ℂ$
6		ssid	$⊢ ℂ \subseteq ℂ$
7		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to [A, B] \underset{cn}{⟶} ℝ \subseteq [A, B] \underset{cn}{⟶} ℂ$
8	5 6 7	mp2an	$⊢ [A, B] \underset{cn}{⟶} ℝ \subseteq [A, B] \underset{cn}{⟶} ℂ$
9	8 4	sselid	$⊢ φ \to F : [A, B] \underset{cn}{⟶} ℂ$
10		abscncf	$⊢ abs : ℂ \underset{cn}{⟶} ℝ$
11	10	a1i	$⊢ φ \to abs : ℂ \underset{cn}{⟶} ℝ$
12	9 11	cncfco	$⊢ φ \to (abs \circ F) : [A, B] \underset{cn}{⟶} ℝ$
13	1 2 3 12	evthicc	$⊢ φ \to (\exists x \in [A, B] \forall y \in [A, B] (abs \circ F) (y) \leq (abs \circ F) (x) \land \exists z \in [A, B] \forall w \in [A, B] (abs \circ F) (z) \leq (abs \circ F) (w))$
14	13	simpld	$⊢ φ \to \exists x \in [A, B] \forall y \in [A, B] (abs \circ F) (y) \leq (abs \circ F) (x)$
15		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℝ \to F : [A, B] ⟶ ℝ$
16		ffun	$⊢ F : [A, B] ⟶ ℝ \to Fun F$
17	4 15 16	3syl	$⊢ φ \to Fun F$
18	17	adantr	$⊢ (φ \land y \in [A, B]) \to Fun F$
19		simpr	$⊢ (φ \land y \in [A, B]) \to y \in [A, B]$
20		fdm	$⊢ F : [A, B] ⟶ ℝ \to dom F = [A, B]$
21	4 15 20	3syl	$⊢ φ \to dom F = [A, B]$
22	21	eqcomd	$⊢ φ \to [A, B] = dom F$
23	22	adantr	$⊢ (φ \land y \in [A, B]) \to [A, B] = dom F$
24	19 23	eleqtrd	$⊢ (φ \land y \in [A, B]) \to y \in dom F$
25		fvco	$⊢ (Fun F \land y \in dom F) \to (abs \circ F) (y) = \|F (y)\|$
26	18 24 25	syl2anc	$⊢ (φ \land y \in [A, B]) \to (abs \circ F) (y) = \|F (y)\|$
27	26	adantlr	$⊢ ((φ \land x \in [A, B]) \land y \in [A, B]) \to (abs \circ F) (y) = \|F (y)\|$
28	17	adantr	$⊢ (φ \land x \in [A, B]) \to Fun F$
29		simpr	$⊢ (φ \land x \in [A, B]) \to x \in [A, B]$
30	22	adantr	$⊢ (φ \land x \in [A, B]) \to [A, B] = dom F$
31	29 30	eleqtrd	$⊢ (φ \land x \in [A, B]) \to x \in dom F$
32		fvco	$⊢ (Fun F \land x \in dom F) \to (abs \circ F) (x) = \|F (x)\|$
33	28 31 32	syl2anc	$⊢ (φ \land x \in [A, B]) \to (abs \circ F) (x) = \|F (x)\|$
34	33	adantr	$⊢ ((φ \land x \in [A, B]) \land y \in [A, B]) \to (abs \circ F) (x) = \|F (x)\|$
35	27 34	breq12d	$⊢ ((φ \land x \in [A, B]) \land y \in [A, B]) \to ((abs \circ F) (y) \leq (abs \circ F) (x) \leftrightarrow \|F (y)\| \leq \|F (x)\|)$
36	35	ralbidva	$⊢ (φ \land x \in [A, B]) \to (\forall y \in [A, B] (abs \circ F) (y) \leq (abs \circ F) (x) \leftrightarrow \forall y \in [A, B] \|F (y)\| \leq \|F (x)\|)$
37	36	rexbidva	$⊢ φ \to (\exists x \in [A, B] \forall y \in [A, B] (abs \circ F) (y) \leq (abs \circ F) (x) \leftrightarrow \exists x \in [A, B] \forall y \in [A, B] \|F (y)\| \leq \|F (x)\|)$
38	14 37	mpbid	$⊢ φ \to \exists x \in [A, B] \forall y \in [A, B] \|F (y)\| \leq \|F (x)\|$
39	13	simprd	$⊢ φ \to \exists z \in [A, B] \forall w \in [A, B] (abs \circ F) (z) \leq (abs \circ F) (w)$
40	17	adantr	$⊢ (φ \land z \in [A, B]) \to Fun F$
41		simpr	$⊢ (φ \land z \in [A, B]) \to z \in [A, B]$
42	22	adantr	$⊢ (φ \land z \in [A, B]) \to [A, B] = dom F$
43	41 42	eleqtrd	$⊢ (φ \land z \in [A, B]) \to z \in dom F$
44		fvco	$⊢ (Fun F \land z \in dom F) \to (abs \circ F) (z) = \|F (z)\|$
45	40 43 44	syl2anc	$⊢ (φ \land z \in [A, B]) \to (abs \circ F) (z) = \|F (z)\|$
46	45	adantr	$⊢ ((φ \land z \in [A, B]) \land w \in [A, B]) \to (abs \circ F) (z) = \|F (z)\|$
47	17	adantr	$⊢ (φ \land w \in [A, B]) \to Fun F$
48		simpr	$⊢ (φ \land w \in [A, B]) \to w \in [A, B]$
49	22	adantr	$⊢ (φ \land w \in [A, B]) \to [A, B] = dom F$
50	48 49	eleqtrd	$⊢ (φ \land w \in [A, B]) \to w \in dom F$
51		fvco	$⊢ (Fun F \land w \in dom F) \to (abs \circ F) (w) = \|F (w)\|$
52	47 50 51	syl2anc	$⊢ (φ \land w \in [A, B]) \to (abs \circ F) (w) = \|F (w)\|$
53	52	adantlr	$⊢ ((φ \land z \in [A, B]) \land w \in [A, B]) \to (abs \circ F) (w) = \|F (w)\|$
54	46 53	breq12d	$⊢ ((φ \land z \in [A, B]) \land w \in [A, B]) \to ((abs \circ F) (z) \leq (abs \circ F) (w) \leftrightarrow \|F (z)\| \leq \|F (w)\|)$
55	54	ralbidva	$⊢ (φ \land z \in [A, B]) \to (\forall w \in [A, B] (abs \circ F) (z) \leq (abs \circ F) (w) \leftrightarrow \forall w \in [A, B] \|F (z)\| \leq \|F (w)\|)$
56	55	rexbidva	$⊢ φ \to (\exists z \in [A, B] \forall w \in [A, B] (abs \circ F) (z) \leq (abs \circ F) (w) \leftrightarrow \exists z \in [A, B] \forall w \in [A, B] \|F (z)\| \leq \|F (w)\|)$
57	39 56	mpbid	$⊢ φ \to \exists z \in [A, B] \forall w \in [A, B] \|F (z)\| \leq \|F (w)\|$
58	38 57	jca	$⊢ φ \to (\exists x \in [A, B] \forall y \in [A, B] \|F (y)\| \leq \|F (x)\| \land \exists z \in [A, B] \forall w \in [A, B] \|F (z)\| \leq \|F (w)\|)$

Metamath Proof Explorer

Theorem evthiccabs

Proof