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 ⊢ Ⅎ 𝑥 𝜑
infnsuprnmpt.a ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
infnsuprnmpt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
infnsuprnmpt.l ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 )
Assertion infnsuprnmpt ( 𝜑 → inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) = - sup ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 infnsuprnmpt.x ⊢ Ⅎ 𝑥 𝜑
2 infnsuprnmpt.a ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3 infnsuprnmpt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4 infnsuprnmpt.l ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑦 ≤ 𝐵 )
5 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6 1 5 3 rnmptssd ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
7 1 3 5 2 rnmptn0 ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ )
8 4 rnmptlb ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 )
9 infrenegsup ⊢ ( ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ∧ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑦 ≤ 𝑧 ) → inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) = - sup ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ , < ) )
10 6 7 8 9 syl3anc ⊢ ( 𝜑 → inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) = - sup ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ , < ) )
11 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ - 𝐵 )
12 rabidim2 ⊢ ( 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } → - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
13 12 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ) → - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
14 negex ⊢ - 𝑤 ∈ V
15 5 elrnmpt ⊢ ( - 𝑤 ∈ V → ( - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 ) )
16 14 15 ax-mp ⊢ ( - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 )
17 13 16 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ) → ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 )
18 nfcv ⊢ Ⅎ 𝑥 𝑤
19 18 nfneg ⊢ Ⅎ 𝑥 - 𝑤
20 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
21 20 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
22 19 21 nfel ⊢ Ⅎ 𝑥 - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
23 nfcv ⊢ Ⅎ 𝑥 ℝ
24 22 23 nfrabw ⊢ Ⅎ 𝑥 { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) }
25 18 24 nfel ⊢ Ⅎ 𝑥 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) }
26 1 25 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } )
27 rabidim1 ⊢ ( 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } → 𝑤 ∈ ℝ )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ) → 𝑤 ∈ ℝ )
29 negeq ⊢ ( - 𝑤 = 𝐵 → - - 𝑤 = - 𝐵 )
30 29 eqcomd ⊢ ( - 𝑤 = 𝐵 → - 𝐵 = - - 𝑤 )
31 30 3ad2ant3 ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ - 𝑤 = 𝐵 ) → - 𝐵 = - - 𝑤 )
32 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ - 𝑤 = 𝐵 ) → 𝑤 ∈ ℝ )
33 recn ⊢ ( 𝑤 ∈ ℝ → 𝑤 ∈ ℂ )
34 33 negnegd ⊢ ( 𝑤 ∈ ℝ → - - 𝑤 = 𝑤 )
35 32 34 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ - 𝑤 = 𝐵 ) → - - 𝑤 = 𝑤 )
36 31 35 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ - 𝑤 = 𝐵 ) → 𝑤 = - 𝐵 )
37 36 3exp ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( 𝑥 ∈ 𝐴 → ( - 𝑤 = 𝐵 → 𝑤 = - 𝐵 ) ) )
38 28 37 syldan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ) → ( 𝑥 ∈ 𝐴 → ( - 𝑤 = 𝐵 → 𝑤 = - 𝐵 ) ) )
39 26 38 reximdai ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ) → ( ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 ) )
40 17 39 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ) → ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 )
41 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ) → 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } )
42 11 40 41 elrnmptd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ) → 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) )
43 42 ex ⊢ ( 𝜑 → ( 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } → 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) )
44 vex ⊢ 𝑤 ∈ V
45 11 elrnmpt ⊢ ( 𝑤 ∈ V → ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 ) )
46 44 45 ax-mp ⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 )
47 46 bilani ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 )
48 18 23 nfel ⊢ Ⅎ 𝑥 𝑤 ∈ ℝ
49 48 22 nfan ⊢ Ⅎ 𝑥 ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
50 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → 𝑤 = - 𝐵 )
51 3 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
52 51 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → - 𝐵 ∈ ℝ )
53 50 52 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → 𝑤 ∈ ℝ )
54 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → 𝑥 ∈ 𝐴 )
55 50 negeqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → - 𝑤 = - - 𝐵 )
56 3 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
57 56 negnegd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - - 𝐵 = 𝐵 )
58 57 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → - - 𝐵 = 𝐵 )
59 55 58 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → - 𝑤 = 𝐵 )
60 rspe ⊢ ( ( 𝑥 ∈ 𝐴 ∧ - 𝑤 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 )
61 54 59 60 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 )
62 14 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → - 𝑤 ∈ V )
63 5 61 62 elrnmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
64 53 63 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
65 64 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑤 = - 𝐵 → ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ) ) )
66 1 49 65 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 → ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ) )
67 66 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 ) → ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
68 47 67 syldan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) → ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
69 rabid ⊢ ( 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ↔ ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
70 68 69 sylibr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) → 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } )
71 70 ex ⊢ ( 𝜑 → ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) → 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ) )
72 43 71 impbid ⊢ ( 𝜑 → ( 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ↔ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) )
73 72 alrimiv ⊢ ( 𝜑 → ∀ 𝑤 ( 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ↔ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) )
74 nfrab1 ⊢ Ⅎ 𝑤 { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) }
75 nfcv ⊢ Ⅎ 𝑤 ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 )
76 74 75 cleqf ⊢ ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } = ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ↔ ∀ 𝑤 ( 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ↔ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) )
77 73 76 sylibr ⊢ ( 𝜑 → { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } = ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) )
78 77 supeq1d ⊢ ( 𝜑 → sup ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ , < ) = sup ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )
79 78 negeqd ⊢ ( 𝜑 → - sup ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ , < ) = - sup ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )
80 eqidd ⊢ ( 𝜑 → - sup ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) = - sup ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )
81 10 79 80 3eqtrd ⊢ ( 𝜑 → inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) = - sup ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )