Metamath Proof Explorer


Theorem 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 φ A
evthiccabs.b φ B
evthiccabs.aleb φ A B
evthiccabs.f φ F : A B cn
Assertion evthiccabs φ x A B y A B F y F x z A B w A B F z F w

Proof

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