Metamath Proof Explorer


Theorem supmul1

Description: The supremum function distributes over multiplication, in the sense that A x. ( sup B ) = sup ( A x. B ) , where A x. B is shorthand for { A x. b | b e. B } and is defined as C below. This is the simple version, with only one set argument; see supmul for the more general case with two set arguments. (Contributed by Mario Carneiro, 5-Jul-2013)

Ref Expression
Hypotheses supmul1.1
|- C = { z | E. v e. B z = ( A x. v ) }
supmul1.2
|- ( ph <-> ( ( A e. RR /\ 0 <_ A /\ A. x e. B 0 <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) )
Assertion supmul1
|- ( ph -> ( A x. sup ( B , RR , < ) ) = sup ( C , RR , < ) )

Proof

Step Hyp Ref Expression
1 supmul1.1
 |-  C = { z | E. v e. B z = ( A x. v ) }
2 supmul1.2
 |-  ( ph <-> ( ( A e. RR /\ 0 <_ A /\ A. x e. B 0 <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) )
3 vex
 |-  w e. _V
4 oveq2
 |-  ( v = b -> ( A x. v ) = ( A x. b ) )
5 4 eqeq2d
 |-  ( v = b -> ( z = ( A x. v ) <-> z = ( A x. b ) ) )
6 5 cbvrexvw
 |-  ( E. v e. B z = ( A x. v ) <-> E. b e. B z = ( A x. b ) )
7 eqeq1
 |-  ( z = w -> ( z = ( A x. b ) <-> w = ( A x. b ) ) )
8 7 rexbidv
 |-  ( z = w -> ( E. b e. B z = ( A x. b ) <-> E. b e. B w = ( A x. b ) ) )
9 6 8 syl5bb
 |-  ( z = w -> ( E. v e. B z = ( A x. v ) <-> E. b e. B w = ( A x. b ) ) )
10 3 9 1 elab2
 |-  ( w e. C <-> E. b e. B w = ( A x. b ) )
11 simpr
 |-  ( ( ( A e. RR /\ 0 <_ A /\ A. x e. B 0 <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) -> ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) )
12 2 11 sylbi
 |-  ( ph -> ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) )
13 12 simp1d
 |-  ( ph -> B C_ RR )
14 13 sselda
 |-  ( ( ph /\ b e. B ) -> b e. RR )
15 suprcl
 |-  ( ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) -> sup ( B , RR , < ) e. RR )
16 12 15 syl
 |-  ( ph -> sup ( B , RR , < ) e. RR )
17 16 adantr
 |-  ( ( ph /\ b e. B ) -> sup ( B , RR , < ) e. RR )
18 simpl1
 |-  ( ( ( A e. RR /\ 0 <_ A /\ A. x e. B 0 <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) -> A e. RR )
19 2 18 sylbi
 |-  ( ph -> A e. RR )
20 simpl2
 |-  ( ( ( A e. RR /\ 0 <_ A /\ A. x e. B 0 <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) -> 0 <_ A )
21 2 20 sylbi
 |-  ( ph -> 0 <_ A )
22 19 21 jca
 |-  ( ph -> ( A e. RR /\ 0 <_ A ) )
23 22 adantr
 |-  ( ( ph /\ b e. B ) -> ( A e. RR /\ 0 <_ A ) )
24 suprub
 |-  ( ( ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) /\ b e. B ) -> b <_ sup ( B , RR , < ) )
25 12 24 sylan
 |-  ( ( ph /\ b e. B ) -> b <_ sup ( B , RR , < ) )
26 lemul2a
 |-  ( ( ( b e. RR /\ sup ( B , RR , < ) e. RR /\ ( A e. RR /\ 0 <_ A ) ) /\ b <_ sup ( B , RR , < ) ) -> ( A x. b ) <_ ( A x. sup ( B , RR , < ) ) )
27 14 17 23 25 26 syl31anc
 |-  ( ( ph /\ b e. B ) -> ( A x. b ) <_ ( A x. sup ( B , RR , < ) ) )
28 breq1
 |-  ( w = ( A x. b ) -> ( w <_ ( A x. sup ( B , RR , < ) ) <-> ( A x. b ) <_ ( A x. sup ( B , RR , < ) ) ) )
29 27 28 syl5ibrcom
 |-  ( ( ph /\ b e. B ) -> ( w = ( A x. b ) -> w <_ ( A x. sup ( B , RR , < ) ) ) )
30 29 rexlimdva
 |-  ( ph -> ( E. b e. B w = ( A x. b ) -> w <_ ( A x. sup ( B , RR , < ) ) ) )
31 10 30 syl5bi
 |-  ( ph -> ( w e. C -> w <_ ( A x. sup ( B , RR , < ) ) ) )
32 31 ralrimiv
 |-  ( ph -> A. w e. C w <_ ( A x. sup ( B , RR , < ) ) )
33 19 adantr
 |-  ( ( ph /\ b e. B ) -> A e. RR )
34 33 14 remulcld
 |-  ( ( ph /\ b e. B ) -> ( A x. b ) e. RR )
35 eleq1a
 |-  ( ( A x. b ) e. RR -> ( w = ( A x. b ) -> w e. RR ) )
36 34 35 syl
 |-  ( ( ph /\ b e. B ) -> ( w = ( A x. b ) -> w e. RR ) )
37 36 rexlimdva
 |-  ( ph -> ( E. b e. B w = ( A x. b ) -> w e. RR ) )
38 10 37 syl5bi
 |-  ( ph -> ( w e. C -> w e. RR ) )
39 38 ssrdv
 |-  ( ph -> C C_ RR )
40 simpr2
 |-  ( ( ( A e. RR /\ 0 <_ A /\ A. x e. B 0 <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) -> B =/= (/) )
41 2 40 sylbi
 |-  ( ph -> B =/= (/) )
42 ovex
 |-  ( A x. b ) e. _V
43 42 isseti
 |-  E. w w = ( A x. b )
44 43 rgenw
 |-  A. b e. B E. w w = ( A x. b )
45 r19.2z
 |-  ( ( B =/= (/) /\ A. b e. B E. w w = ( A x. b ) ) -> E. b e. B E. w w = ( A x. b ) )
46 41 44 45 sylancl
 |-  ( ph -> E. b e. B E. w w = ( A x. b ) )
47 10 exbii
 |-  ( E. w w e. C <-> E. w E. b e. B w = ( A x. b ) )
48 n0
 |-  ( C =/= (/) <-> E. w w e. C )
49 rexcom4
 |-  ( E. b e. B E. w w = ( A x. b ) <-> E. w E. b e. B w = ( A x. b ) )
50 47 48 49 3bitr4i
 |-  ( C =/= (/) <-> E. b e. B E. w w = ( A x. b ) )
51 46 50 sylibr
 |-  ( ph -> C =/= (/) )
52 19 16 remulcld
 |-  ( ph -> ( A x. sup ( B , RR , < ) ) e. RR )
53 brralrspcev
 |-  ( ( ( A x. sup ( B , RR , < ) ) e. RR /\ A. w e. C w <_ ( A x. sup ( B , RR , < ) ) ) -> E. x e. RR A. w e. C w <_ x )
54 52 32 53 syl2anc
 |-  ( ph -> E. x e. RR A. w e. C w <_ x )
55 39 51 54 3jca
 |-  ( ph -> ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) )
56 suprleub
 |-  ( ( ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) /\ ( A x. sup ( B , RR , < ) ) e. RR ) -> ( sup ( C , RR , < ) <_ ( A x. sup ( B , RR , < ) ) <-> A. w e. C w <_ ( A x. sup ( B , RR , < ) ) ) )
57 55 52 56 syl2anc
 |-  ( ph -> ( sup ( C , RR , < ) <_ ( A x. sup ( B , RR , < ) ) <-> A. w e. C w <_ ( A x. sup ( B , RR , < ) ) ) )
58 32 57 mpbird
 |-  ( ph -> sup ( C , RR , < ) <_ ( A x. sup ( B , RR , < ) ) )
59 simpr
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) )
60 suprcl
 |-  ( ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) -> sup ( C , RR , < ) e. RR )
61 55 60 syl
 |-  ( ph -> sup ( C , RR , < ) e. RR )
62 61 adantr
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> sup ( C , RR , < ) e. RR )
63 16 adantr
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> sup ( B , RR , < ) e. RR )
64 19 adantr
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> A e. RR )
65 n0
 |-  ( B =/= (/) <-> E. b b e. B )
66 0red
 |-  ( ( ph /\ b e. B ) -> 0 e. RR )
67 simpl3
 |-  ( ( ( A e. RR /\ 0 <_ A /\ A. x e. B 0 <_ x ) /\ ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) ) -> A. x e. B 0 <_ x )
68 2 67 sylbi
 |-  ( ph -> A. x e. B 0 <_ x )
69 breq2
 |-  ( x = b -> ( 0 <_ x <-> 0 <_ b ) )
70 69 rspccva
 |-  ( ( A. x e. B 0 <_ x /\ b e. B ) -> 0 <_ b )
71 68 70 sylan
 |-  ( ( ph /\ b e. B ) -> 0 <_ b )
72 66 14 17 71 25 letrd
 |-  ( ( ph /\ b e. B ) -> 0 <_ sup ( B , RR , < ) )
73 72 ex
 |-  ( ph -> ( b e. B -> 0 <_ sup ( B , RR , < ) ) )
74 73 exlimdv
 |-  ( ph -> ( E. b b e. B -> 0 <_ sup ( B , RR , < ) ) )
75 65 74 syl5bi
 |-  ( ph -> ( B =/= (/) -> 0 <_ sup ( B , RR , < ) ) )
76 41 75 mpd
 |-  ( ph -> 0 <_ sup ( B , RR , < ) )
77 76 adantr
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> 0 <_ sup ( B , RR , < ) )
78 0red
 |-  ( ( ph /\ w e. C ) -> 0 e. RR )
79 38 imp
 |-  ( ( ph /\ w e. C ) -> w e. RR )
80 61 adantr
 |-  ( ( ph /\ w e. C ) -> sup ( C , RR , < ) e. RR )
81 21 adantr
 |-  ( ( ph /\ b e. B ) -> 0 <_ A )
82 33 14 81 71 mulge0d
 |-  ( ( ph /\ b e. B ) -> 0 <_ ( A x. b ) )
83 breq2
 |-  ( w = ( A x. b ) -> ( 0 <_ w <-> 0 <_ ( A x. b ) ) )
84 82 83 syl5ibrcom
 |-  ( ( ph /\ b e. B ) -> ( w = ( A x. b ) -> 0 <_ w ) )
85 84 rexlimdva
 |-  ( ph -> ( E. b e. B w = ( A x. b ) -> 0 <_ w ) )
86 10 85 syl5bi
 |-  ( ph -> ( w e. C -> 0 <_ w ) )
87 86 imp
 |-  ( ( ph /\ w e. C ) -> 0 <_ w )
88 suprub
 |-  ( ( ( C C_ RR /\ C =/= (/) /\ E. x e. RR A. w e. C w <_ x ) /\ w e. C ) -> w <_ sup ( C , RR , < ) )
89 55 88 sylan
 |-  ( ( ph /\ w e. C ) -> w <_ sup ( C , RR , < ) )
90 78 79 80 87 89 letrd
 |-  ( ( ph /\ w e. C ) -> 0 <_ sup ( C , RR , < ) )
91 90 ex
 |-  ( ph -> ( w e. C -> 0 <_ sup ( C , RR , < ) ) )
92 91 exlimdv
 |-  ( ph -> ( E. w w e. C -> 0 <_ sup ( C , RR , < ) ) )
93 48 92 syl5bi
 |-  ( ph -> ( C =/= (/) -> 0 <_ sup ( C , RR , < ) ) )
94 51 93 mpd
 |-  ( ph -> 0 <_ sup ( C , RR , < ) )
95 94 anim1i
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> ( 0 <_ sup ( C , RR , < ) /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) )
96 0red
 |-  ( ph -> 0 e. RR )
97 lelttr
 |-  ( ( 0 e. RR /\ sup ( C , RR , < ) e. RR /\ ( A x. sup ( B , RR , < ) ) e. RR ) -> ( ( 0 <_ sup ( C , RR , < ) /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> 0 < ( A x. sup ( B , RR , < ) ) ) )
98 96 61 52 97 syl3anc
 |-  ( ph -> ( ( 0 <_ sup ( C , RR , < ) /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> 0 < ( A x. sup ( B , RR , < ) ) ) )
99 98 adantr
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> ( ( 0 <_ sup ( C , RR , < ) /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> 0 < ( A x. sup ( B , RR , < ) ) ) )
100 95 99 mpd
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> 0 < ( A x. sup ( B , RR , < ) ) )
101 prodgt02
 |-  ( ( ( A e. RR /\ sup ( B , RR , < ) e. RR ) /\ ( 0 <_ sup ( B , RR , < ) /\ 0 < ( A x. sup ( B , RR , < ) ) ) ) -> 0 < A )
102 64 63 77 100 101 syl22anc
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> 0 < A )
103 ltdivmul
 |-  ( ( sup ( C , RR , < ) e. RR /\ sup ( B , RR , < ) e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( sup ( C , RR , < ) / A ) < sup ( B , RR , < ) <-> sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) )
104 62 63 64 102 103 syl112anc
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> ( ( sup ( C , RR , < ) / A ) < sup ( B , RR , < ) <-> sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) )
105 59 104 mpbird
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> ( sup ( C , RR , < ) / A ) < sup ( B , RR , < ) )
106 12 adantr
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) )
107 102 gt0ne0d
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> A =/= 0 )
108 62 64 107 redivcld
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> ( sup ( C , RR , < ) / A ) e. RR )
109 suprlub
 |-  ( ( ( B C_ RR /\ B =/= (/) /\ E. x e. RR A. y e. B y <_ x ) /\ ( sup ( C , RR , < ) / A ) e. RR ) -> ( ( sup ( C , RR , < ) / A ) < sup ( B , RR , < ) <-> E. b e. B ( sup ( C , RR , < ) / A ) < b ) )
110 106 108 109 syl2anc
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> ( ( sup ( C , RR , < ) / A ) < sup ( B , RR , < ) <-> E. b e. B ( sup ( C , RR , < ) / A ) < b ) )
111 105 110 mpbid
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> E. b e. B ( sup ( C , RR , < ) / A ) < b )
112 34 adantlr
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) /\ b e. B ) -> ( A x. b ) e. RR )
113 61 ad2antrr
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) /\ b e. B ) -> sup ( C , RR , < ) e. RR )
114 rspe
 |-  ( ( b e. B /\ w = ( A x. b ) ) -> E. b e. B w = ( A x. b ) )
115 114 10 sylibr
 |-  ( ( b e. B /\ w = ( A x. b ) ) -> w e. C )
116 115 adantl
 |-  ( ( ph /\ ( b e. B /\ w = ( A x. b ) ) ) -> w e. C )
117 simplrr
 |-  ( ( ( ph /\ ( b e. B /\ w = ( A x. b ) ) ) /\ w e. C ) -> w = ( A x. b ) )
118 89 adantlr
 |-  ( ( ( ph /\ ( b e. B /\ w = ( A x. b ) ) ) /\ w e. C ) -> w <_ sup ( C , RR , < ) )
119 117 118 eqbrtrrd
 |-  ( ( ( ph /\ ( b e. B /\ w = ( A x. b ) ) ) /\ w e. C ) -> ( A x. b ) <_ sup ( C , RR , < ) )
120 116 119 mpdan
 |-  ( ( ph /\ ( b e. B /\ w = ( A x. b ) ) ) -> ( A x. b ) <_ sup ( C , RR , < ) )
121 120 expr
 |-  ( ( ph /\ b e. B ) -> ( w = ( A x. b ) -> ( A x. b ) <_ sup ( C , RR , < ) ) )
122 121 exlimdv
 |-  ( ( ph /\ b e. B ) -> ( E. w w = ( A x. b ) -> ( A x. b ) <_ sup ( C , RR , < ) ) )
123 43 122 mpi
 |-  ( ( ph /\ b e. B ) -> ( A x. b ) <_ sup ( C , RR , < ) )
124 123 adantlr
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) /\ b e. B ) -> ( A x. b ) <_ sup ( C , RR , < ) )
125 112 113 124 lensymd
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) /\ b e. B ) -> -. sup ( C , RR , < ) < ( A x. b ) )
126 14 adantlr
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) /\ b e. B ) -> b e. RR )
127 19 ad2antrr
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) /\ b e. B ) -> A e. RR )
128 102 adantr
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) /\ b e. B ) -> 0 < A )
129 ltdivmul
 |-  ( ( sup ( C , RR , < ) e. RR /\ b e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( sup ( C , RR , < ) / A ) < b <-> sup ( C , RR , < ) < ( A x. b ) ) )
130 113 126 127 128 129 syl112anc
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) /\ b e. B ) -> ( ( sup ( C , RR , < ) / A ) < b <-> sup ( C , RR , < ) < ( A x. b ) ) )
131 125 130 mtbird
 |-  ( ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) /\ b e. B ) -> -. ( sup ( C , RR , < ) / A ) < b )
132 131 nrexdv
 |-  ( ( ph /\ sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) -> -. E. b e. B ( sup ( C , RR , < ) / A ) < b )
133 111 132 pm2.65da
 |-  ( ph -> -. sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) )
134 58 133 jca
 |-  ( ph -> ( sup ( C , RR , < ) <_ ( A x. sup ( B , RR , < ) ) /\ -. sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) )
135 61 52 eqleltd
 |-  ( ph -> ( sup ( C , RR , < ) = ( A x. sup ( B , RR , < ) ) <-> ( sup ( C , RR , < ) <_ ( A x. sup ( B , RR , < ) ) /\ -. sup ( C , RR , < ) < ( A x. sup ( B , RR , < ) ) ) ) )
136 134 135 mpbird
 |-  ( ph -> sup ( C , RR , < ) = ( A x. sup ( B , RR , < ) ) )
137 136 eqcomd
 |-  ( ph -> ( A x. sup ( B , RR , < ) ) = sup ( C , RR , < ) )