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 , < ) )