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 
|- ( ph -> A e. RR )
evthiccabs.b 
|- ( ph -> B e. RR )
evthiccabs.aleb 
|- ( ph -> A <_ B )
evthiccabs.f 
|- ( ph -> F e. ( ( A [,] B ) -cn-> RR ) )
Assertion evthiccabs 
|- ( ph -> ( E. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( F ` y ) ) <_ ( abs ` ( F ` x ) ) /\ E. z e. ( A [,] B ) A. w e. ( A [,] B ) ( abs ` ( F ` z ) ) <_ ( abs ` ( F ` w ) ) ) )

Proof

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