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 biimpi ⊢ ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 )
48 47 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 )
49 18 23 nfel ⊢ Ⅎ 𝑥 𝑤 ∈ ℝ
50 49 22 nfan ⊢ Ⅎ 𝑥 ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
51 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → 𝑤 = - 𝐵 )
52 3 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
53 52 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → - 𝐵 ∈ ℝ )
54 51 53 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → 𝑤 ∈ ℝ )
55 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → 𝑥 ∈ 𝐴 )
56 51 negeqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → - 𝑤 = - - 𝐵 )
57 3 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
58 57 negnegd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - - 𝐵 = 𝐵 )
59 58 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → - - 𝐵 = 𝐵 )
60 56 59 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → - 𝑤 = 𝐵 )
61 rspe ⊢ ( ( 𝑥 ∈ 𝐴 ∧ - 𝑤 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 )
62 55 60 61 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 )
63 14 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → - 𝑤 ∈ V )
64 5 62 63 elrnmptd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
65 54 64 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑤 = - 𝐵 ) → ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
66 65 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑤 = - 𝐵 → ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ) ) )
67 1 50 66 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 → ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ) )
68 67 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 ) → ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
69 48 68 syldan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) → ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
70 rabid ⊢ ( 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ↔ ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
71 69 70 sylibr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) → 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } )
72 71 ex ⊢ ( 𝜑 → ( 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) → 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ) )
73 43 72 impbid ⊢ ( 𝜑 → ( 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ↔ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) )
74 73 alrimiv ⊢ ( 𝜑 → ∀ 𝑤 ( 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ↔ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) )
75 nfrab1 ⊢ Ⅎ 𝑤 { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) }
76 nfcv ⊢ Ⅎ 𝑤 ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 )
77 75 76 cleqf ⊢ ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } = ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ↔ ∀ 𝑤 ( 𝑤 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ↔ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) )
78 74 77 sylibr ⊢ ( 𝜑 → { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } = ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) )
79 78 supeq1d ⊢ ( 𝜑 → sup ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ , < ) = sup ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )
80 79 negeqd ⊢ ( 𝜑 → - sup ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ , < ) = - sup ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )
81 eqidd ⊢ ( 𝜑 → - sup ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) = - sup ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )
82 10 80 81 3eqtrd ⊢ ( 𝜑 → inf ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) = - sup ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )