Metamath Proof Explorer

Theorem infnsuprnmpt

Description: The indexed infimum of real numbers is the negative of the indexed supremum of the negative values. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses infnsuprnmpt.x 
|- F/ x ph
infnsuprnmpt.a 
|- ( ph -> A =/= (/) )
infnsuprnmpt.b 
|- ( ( ph /\ x e. A ) -> B e. RR )
infnsuprnmpt.l 
|- ( ph -> E. y e. RR A. x e. A y <_ B )
Assertion infnsuprnmpt 
|- ( ph -> inf ( ran ( x e. A |-> B ) , RR , < ) = -u sup ( ran ( x e. A |-> -u B ) , RR , < ) )

Proof

Step Hyp Ref Expression
1 infnsuprnmpt.x 
 |-  F/ x ph
2 infnsuprnmpt.a 
 |-  ( ph -> A =/= (/) )
3 infnsuprnmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
4 infnsuprnmpt.l 
 |-  ( ph -> E. y e. RR A. x e. A y <_ B )
5 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
6 1 5 3 rnmptssd 
 |-  ( ph -> ran ( x e. A |-> B ) C_ RR )
7 1 3 5 2 rnmptn0 
 |-  ( ph -> ran ( x e. A |-> B ) =/= (/) )
8 4 rnmptlb 
 |-  ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z )
9 infrenegsup 
 |-  ( ( ran ( x e. A |-> B ) C_ RR /\ ran ( x e. A |-> B ) =/= (/) /\ E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z ) -> inf ( ran ( x e. A |-> B ) , RR , < ) = -u sup ( { w e. RR | -u w e. ran ( x e. A |-> B ) } , RR , < ) )
10 6 7 8 9 syl3anc 
 |-  ( ph -> inf ( ran ( x e. A |-> B ) , RR , < ) = -u sup ( { w e. RR | -u w e. ran ( x e. A |-> B ) } , RR , < ) )
11 eqid 
 |-  ( x e. A |-> -u B ) = ( x e. A |-> -u B )
12 rabidim2 
 |-  ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } -> -u w e. ran ( x e. A |-> B ) )
13 12 adantl 
 |-  ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> -u w e. ran ( x e. A |-> B ) )
14 negex 
 |-  -u w e. _V
15 5 elrnmpt 
 |-  ( -u w e. _V -> ( -u w e. ran ( x e. A |-> B ) <-> E. x e. A -u w = B ) )
16 14 15 ax-mp 
 |-  ( -u w e. ran ( x e. A |-> B ) <-> E. x e. A -u w = B )
17 13 16 sylib 
 |-  ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> E. x e. A -u w = B )
18 nfcv 
 |-  F/_ x w
19 18 nfneg 
 |-  F/_ x -u w
20 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
21 20 nfrn 
 |-  F/_ x ran ( x e. A |-> B )
22 19 21 nfel 
 |-  F/ x -u w e. ran ( x e. A |-> B )
23 nfcv 
 |-  F/_ x RR
24 22 23 nfrabw 
 |-  F/_ x { w e. RR | -u w e. ran ( x e. A |-> B ) }
25 18 24 nfel 
 |-  F/ x w e. { w e. RR | -u w e. ran ( x e. A |-> B ) }
26 1 25 nfan 
 |-  F/ x ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } )
27 rabidim1 
 |-  ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } -> w e. RR )
28 27 adantl 
 |-  ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> w e. RR )
29 negeq 
 |-  ( -u w = B -> -u -u w = -u B )
30 29 eqcomd 
 |-  ( -u w = B -> -u B = -u -u w )
31 30 3ad2ant3 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ -u w = B ) -> -u B = -u -u w )
32 simp1r 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ -u w = B ) -> w e. RR )
33 recn 
 |-  ( w e. RR -> w e. CC )
34 33 negnegd 
 |-  ( w e. RR -> -u -u w = w )
35 32 34 syl 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ -u w = B ) -> -u -u w = w )
36 31 35 eqtr2d 
 |-  ( ( ( ph /\ w e. RR ) /\ x e. A /\ -u w = B ) -> w = -u B )
37 36 3exp 
 |-  ( ( ph /\ w e. RR ) -> ( x e. A -> ( -u w = B -> w = -u B ) ) )
38 28 37 syldan 
 |-  ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> ( x e. A -> ( -u w = B -> w = -u B ) ) )
39 26 38 reximdai 
 |-  ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> ( E. x e. A -u w = B -> E. x e. A w = -u B ) )
40 17 39 mpd 
 |-  ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> E. x e. A w = -u B )
41 simpr 
 |-  ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } )
42 11 40 41 elrnmptd 
 |-  ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> w e. ran ( x e. A |-> -u B ) )
43 42 ex 
 |-  ( ph -> ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } -> w e. ran ( x e. A |-> -u B ) ) )
44 vex 
 |-  w e. _V
45 11 elrnmpt 
 |-  ( w e. _V -> ( w e. ran ( x e. A |-> -u B ) <-> E. x e. A w = -u B ) )
46 44 45 ax-mp 
 |-  ( w e. ran ( x e. A |-> -u B ) <-> E. x e. A w = -u B )
47 46 biimpi 
 |-  ( w e. ran ( x e. A |-> -u B ) -> E. x e. A w = -u B )
48 47 adantl 
 |-  ( ( ph /\ w e. ran ( x e. A |-> -u B ) ) -> E. x e. A w = -u B )
49 18 23 nfel 
 |-  F/ x w e. RR
50 49 22 nfan 
 |-  F/ x ( w e. RR /\ -u w e. ran ( x e. A |-> B ) )
51 simp3 
 |-  ( ( ph /\ x e. A /\ w = -u B ) -> w = -u B )
52 3 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. RR )
53 52 3adant3 
 |-  ( ( ph /\ x e. A /\ w = -u B ) -> -u B e. RR )
54 51 53 eqeltrd 
 |-  ( ( ph /\ x e. A /\ w = -u B ) -> w e. RR )
55 simp2 
 |-  ( ( ph /\ x e. A /\ w = -u B ) -> x e. A )
56 51 negeqd 
 |-  ( ( ph /\ x e. A /\ w = -u B ) -> -u w = -u -u B )
57 3 recnd 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
58 57 negnegd 
 |-  ( ( ph /\ x e. A ) -> -u -u B = B )
59 58 3adant3 
 |-  ( ( ph /\ x e. A /\ w = -u B ) -> -u -u B = B )
60 56 59 eqtrd 
 |-  ( ( ph /\ x e. A /\ w = -u B ) -> -u w = B )
61 rspe 
 |-  ( ( x e. A /\ -u w = B ) -> E. x e. A -u w = B )
62 55 60 61 syl2anc 
 |-  ( ( ph /\ x e. A /\ w = -u B ) -> E. x e. A -u w = B )
63 14 a1i 
 |-  ( ( ph /\ x e. A /\ w = -u B ) -> -u w e. _V )
64 5 62 63 elrnmptd 
 |-  ( ( ph /\ x e. A /\ w = -u B ) -> -u w e. ran ( x e. A |-> B ) )
65 54 64 jca 
 |-  ( ( ph /\ x e. A /\ w = -u B ) -> ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) )
66 65 3exp 
 |-  ( ph -> ( x e. A -> ( w = -u B -> ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) ) ) )
67 1 50 66 rexlimd 
 |-  ( ph -> ( E. x e. A w = -u B -> ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) ) )
68 67 imp 
 |-  ( ( ph /\ E. x e. A w = -u B ) -> ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) )
69 48 68 syldan 
 |-  ( ( ph /\ w e. ran ( x e. A |-> -u B ) ) -> ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) )
70 rabid 
 |-  ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } <-> ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) )
71 69 70 sylibr 
 |-  ( ( ph /\ w e. ran ( x e. A |-> -u B ) ) -> w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } )
72 71 ex 
 |-  ( ph -> ( w e. ran ( x e. A |-> -u B ) -> w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) )
73 43 72 impbid 
 |-  ( ph -> ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } <-> w e. ran ( x e. A |-> -u B ) ) )
74 73 alrimiv 
 |-  ( ph -> A. w ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } <-> w e. ran ( x e. A |-> -u B ) ) )
75 nfrab1 
 |-  F/_ w { w e. RR | -u w e. ran ( x e. A |-> B ) }
76 nfcv 
 |-  F/_ w ran ( x e. A |-> -u B )
77 75 76 cleqf 
 |-  ( { w e. RR | -u w e. ran ( x e. A |-> B ) } = ran ( x e. A |-> -u B ) <-> A. w ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } <-> w e. ran ( x e. A |-> -u B ) ) )
78 74 77 sylibr 
 |-  ( ph -> { w e. RR | -u w e. ran ( x e. A |-> B ) } = ran ( x e. A |-> -u B ) )
79 78 supeq1d 
 |-  ( ph -> sup ( { w e. RR | -u w e. ran ( x e. A |-> B ) } , RR , < ) = sup ( ran ( x e. A |-> -u B ) , RR , < ) )
80 79 negeqd 
 |-  ( ph -> -u sup ( { w e. RR | -u w e. ran ( x e. A |-> B ) } , RR , < ) = -u sup ( ran ( x e. A |-> -u B ) , RR , < ) )
81 eqidd 
 |-  ( ph -> -u sup ( ran ( x e. A |-> -u B ) , RR , < ) = -u sup ( ran ( x e. A |-> -u B ) , RR , < ) )
82 10 80 81 3eqtrd 
 |-  ( ph -> inf ( ran ( x e. A |-> B ) , RR , < ) = -u sup ( ran ( x e. A |-> -u B ) , RR , < ) )