Metamath Proof Explorer

Theorem smfmullem3

Description: The multiplication of two sigma-measurable functions is measurable: this is the step (i) of the proof of Proposition 121E (d) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfmullem3.r 
|- ( ph -> R e. RR )
smfmullem3.k 
|- K = { q e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < R }
smfmullem3.u 
|- ( ph -> U e. RR )
smfmullem3.v 
|- ( ph -> V e. RR )
smfmullem3.l 
|- ( ph -> ( U x. V ) < R )
smfmullem3.x 
|- X = ( ( R - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) )
smfmullem3.y 
|- Y = if ( 1 <_ X , 1 , X )
Assertion smfmullem3 
|- ( ph -> E. q e. K ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) )

Proof

Step Hyp Ref Expression
1 smfmullem3.r 
 |-  ( ph -> R e. RR )
2 smfmullem3.k 
 |-  K = { q e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < R }
3 smfmullem3.u 
 |-  ( ph -> U e. RR )
4 smfmullem3.v 
 |-  ( ph -> V e. RR )
5 smfmullem3.l 
 |-  ( ph -> ( U x. V ) < R )
6 smfmullem3.x 
 |-  X = ( ( R - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) )
7 smfmullem3.y 
 |-  Y = if ( 1 <_ X , 1 , X )
8 7 a1i 
 |-  ( ph -> Y = if ( 1 <_ X , 1 , X ) )
9 1rp 
 |-  1 e. RR+
10 9 a1i 
 |-  ( ph -> 1 e. RR+ )
11 6 a1i 
 |-  ( ph -> X = ( ( R - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) ) )
12 3 4 remulcld 
 |-  ( ph -> ( U x. V ) e. RR )
13 difrp 
 |-  ( ( ( U x. V ) e. RR /\ R e. RR ) -> ( ( U x. V ) < R <-> ( R - ( U x. V ) ) e. RR+ ) )
14 12 1 13 syl2anc 
 |-  ( ph -> ( ( U x. V ) < R <-> ( R - ( U x. V ) ) e. RR+ ) )
15 5 14 mpbid 
 |-  ( ph -> ( R - ( U x. V ) ) e. RR+ )
16 1re 
 |-  1 e. RR
17 16 a1i 
 |-  ( ph -> 1 e. RR )
18 3 recnd 
 |-  ( ph -> U e. CC )
19 18 abscld 
 |-  ( ph -> ( abs ` U ) e. RR )
20 4 recnd 
 |-  ( ph -> V e. CC )
21 20 abscld 
 |-  ( ph -> ( abs ` V ) e. RR )
22 19 21 readdcld 
 |-  ( ph -> ( ( abs ` U ) + ( abs ` V ) ) e. RR )
23 17 22 readdcld 
 |-  ( ph -> ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) e. RR )
24 0re 
 |-  0 e. RR
25 24 a1i 
 |-  ( ph -> 0 e. RR )
26 10 rpgt0d 
 |-  ( ph -> 0 < 1 )
27 0red 
 |-  ( ph -> 0 e. RR )
28 18 absge0d 
 |-  ( ph -> 0 <_ ( abs ` U ) )
29 20 absge0d 
 |-  ( ph -> 0 <_ ( abs ` V ) )
30 19 21 addge01d 
 |-  ( ph -> ( 0 <_ ( abs ` V ) <-> ( abs ` U ) <_ ( ( abs ` U ) + ( abs ` V ) ) ) )
31 29 30 mpbid 
 |-  ( ph -> ( abs ` U ) <_ ( ( abs ` U ) + ( abs ` V ) ) )
32 27 19 22 28 31 letrd 
 |-  ( ph -> 0 <_ ( ( abs ` U ) + ( abs ` V ) ) )
33 17 22 addge01d 
 |-  ( ph -> ( 0 <_ ( ( abs ` U ) + ( abs ` V ) ) <-> 1 <_ ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) ) )
34 32 33 mpbid 
 |-  ( ph -> 1 <_ ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) )
35 25 17 23 26 34 ltletrd 
 |-  ( ph -> 0 < ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) )
36 23 35 elrpd 
 |-  ( ph -> ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) e. RR+ )
37 15 36 rpdivcld 
 |-  ( ph -> ( ( R - ( U x. V ) ) / ( 1 + ( ( abs ` U ) + ( abs ` V ) ) ) ) e. RR+ )
38 11 37 eqeltrd 
 |-  ( ph -> X e. RR+ )
39 10 38 ifcld 
 |-  ( ph -> if ( 1 <_ X , 1 , X ) e. RR+ )
40 8 39 eqeltrd 
 |-  ( ph -> Y e. RR+ )
41 40 rpred 
 |-  ( ph -> Y e. RR )
42 3 41 resubcld 
 |-  ( ph -> ( U - Y ) e. RR )
43 42 rexrd 
 |-  ( ph -> ( U - Y ) e. RR* )
44 3 rexrd 
 |-  ( ph -> U e. RR* )
45 3 40 ltsubrpd 
 |-  ( ph -> ( U - Y ) < U )
46 43 44 45 qelioo 
 |-  ( ph -> E. p e. QQ p e. ( ( U - Y ) (,) U ) )
47 3 41 readdcld 
 |-  ( ph -> ( U + Y ) e. RR )
48 47 rexrd 
 |-  ( ph -> ( U + Y ) e. RR* )
49 3 40 ltaddrpd 
 |-  ( ph -> U < ( U + Y ) )
50 44 48 49 qelioo 
 |-  ( ph -> E. r e. QQ r e. ( U (,) ( U + Y ) ) )
51 50 ad2antrr 
 |-  ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) -> E. r e. QQ r e. ( U (,) ( U + Y ) ) )
52 simp-4l 
 |-  ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) -> ph )
53 4 41 resubcld 
 |-  ( ph -> ( V - Y ) e. RR )
54 53 rexrd 
 |-  ( ph -> ( V - Y ) e. RR* )
55 4 rexrd 
 |-  ( ph -> V e. RR* )
56 4 40 ltsubrpd 
 |-  ( ph -> ( V - Y ) < V )
57 54 55 56 qelioo 
 |-  ( ph -> E. s e. QQ s e. ( ( V - Y ) (,) V ) )
58 52 57 syl 
 |-  ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) -> E. s e. QQ s e. ( ( V - Y ) (,) V ) )
59 52 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) -> ph )
60 4 41 readdcld 
 |-  ( ph -> ( V + Y ) e. RR )
61 60 rexrd 
 |-  ( ph -> ( V + Y ) e. RR* )
62 4 40 ltaddrpd 
 |-  ( ph -> V < ( V + Y ) )
63 55 61 62 qelioo 
 |-  ( ph -> E. z e. QQ z e. ( V (,) ( V + Y ) ) )
64 59 63 syl 
 |-  ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) -> E. z e. QQ z e. ( V (,) ( V + Y ) ) )
65 1 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) /\ z e. QQ ) /\ z e. ( V (,) ( V + Y ) ) ) -> R e. RR )
66 3 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) /\ z e. QQ ) /\ z e. ( V (,) ( V + Y ) ) ) -> U e. RR )
67 4 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) /\ z e. QQ ) /\ z e. ( V (,) ( V + Y ) ) ) -> V e. RR )
68 5 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) /\ z e. QQ ) /\ z e. ( V (,) ( V + Y ) ) ) -> ( U x. V ) < R )
69 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) /\ z e. QQ ) /\ z e. ( V (,) ( V + Y ) ) ) -> p e. QQ )
70 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) /\ z e. QQ ) /\ z e. ( V (,) ( V + Y ) ) ) -> r e. QQ )
71 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) /\ z e. QQ ) /\ z e. ( V (,) ( V + Y ) ) ) -> s e. QQ )
72 simplr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) /\ z e. QQ ) /\ z e. ( V (,) ( V + Y ) ) ) -> z e. QQ )
73 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) /\ z e. QQ ) /\ z e. ( V (,) ( V + Y ) ) ) -> p e. ( ( U - Y ) (,) U ) )
74 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) /\ z e. QQ ) /\ z e. ( V (,) ( V + Y ) ) ) -> r e. ( U (,) ( U + Y ) ) )
75 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) /\ z e. QQ ) /\ z e. ( V (,) ( V + Y ) ) ) -> s e. ( ( V - Y ) (,) V ) )
76 simpr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) /\ z e. QQ ) /\ z e. ( V (,) ( V + Y ) ) ) -> z e. ( V (,) ( V + Y ) ) )
77 65 2 66 67 68 69 70 71 72 73 74 75 76 6 7 smfmullem2 
 |-  ( ( ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) /\ z e. QQ ) /\ z e. ( V (,) ( V + Y ) ) ) -> E. q e. K ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) )
78 77 rexlimdva2 
 |-  ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) -> ( E. z e. QQ z e. ( V (,) ( V + Y ) ) -> E. q e. K ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) ) )
79 64 78 mpd 
 |-  ( ( ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) /\ s e. QQ ) /\ s e. ( ( V - Y ) (,) V ) ) -> E. q e. K ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) )
80 79 rexlimdva2 
 |-  ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) -> ( E. s e. QQ s e. ( ( V - Y ) (,) V ) -> E. q e. K ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) ) )
81 58 80 mpd 
 |-  ( ( ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) /\ r e. QQ ) /\ r e. ( U (,) ( U + Y ) ) ) -> E. q e. K ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) )
82 81 rexlimdva2 
 |-  ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) -> ( E. r e. QQ r e. ( U (,) ( U + Y ) ) -> E. q e. K ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) ) )
83 51 82 mpd 
 |-  ( ( ( ph /\ p e. QQ ) /\ p e. ( ( U - Y ) (,) U ) ) -> E. q e. K ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) )
84 83 rexlimdva2 
 |-  ( ph -> ( E. p e. QQ p e. ( ( U - Y ) (,) U ) -> E. q e. K ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) ) )
85 46 84 mpd 
 |-  ( ph -> E. q e. K ( U e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ V e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) )