Metamath Proof Explorer

Theorem smfmul

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

Ref Expression
Hypotheses smfmul.x 
|- F/ x ph
smfmul.s 
|- ( ph -> S e. SAlg )
smfmul.a 
|- ( ph -> A e. V )
smfmul.b 
|- ( ( ph /\ x e. A ) -> B e. RR )
smfmul.d 
|- ( ( ph /\ x e. C ) -> D e. RR )
smfmul.m 
|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
smfmul.n 
|- ( ph -> ( x e. C |-> D ) e. ( SMblFn ` S ) )
Assertion smfmul 
|- ( ph -> ( x e. ( A i^i C ) |-> ( B x. D ) ) e. ( SMblFn ` S ) )

Proof

Step Hyp Ref Expression
1 smfmul.x 
 |-  F/ x ph
2 smfmul.s 
 |-  ( ph -> S e. SAlg )
3 smfmul.a 
 |-  ( ph -> A e. V )
4 smfmul.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
5 smfmul.d 
 |-  ( ( ph /\ x e. C ) -> D e. RR )
6 smfmul.m 
 |-  ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
7 smfmul.n 
 |-  ( ph -> ( x e. C |-> D ) e. ( SMblFn ` S ) )
8 nfv 
 |-  F/ a ph
9 elinel1 
 |-  ( x e. ( A i^i C ) -> x e. A )
10 9 adantl 
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> x e. A )
11 1 10 ssdf 
 |-  ( ph -> ( A i^i C ) C_ A )
12 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
13 1 12 4 dmmptdf 
 |-  ( ph -> dom ( x e. A |-> B ) = A )
14 13 eqcomd 
 |-  ( ph -> A = dom ( x e. A |-> B ) )
15 eqid 
 |-  dom ( x e. A |-> B ) = dom ( x e. A |-> B )
16 2 6 15 smfdmss 
 |-  ( ph -> dom ( x e. A |-> B ) C_ U. S )
17 14 16 eqsstrd 
 |-  ( ph -> A C_ U. S )
18 11 17 sstrd 
 |-  ( ph -> ( A i^i C ) C_ U. S )
19 10 4 syldan 
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> B e. RR )
20 elinel2 
 |-  ( x e. ( A i^i C ) -> x e. C )
21 20 adantl 
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> x e. C )
22 21 5 syldan 
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> D e. RR )
23 19 22 remulcld 
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> ( B x. D ) e. RR )
24 nfv 
 |-  F/ x a e. RR
25 1 24 nfan 
 |-  F/ x ( ph /\ a e. RR )
26 2 adantr 
 |-  ( ( ph /\ a e. RR ) -> S e. SAlg )
27 3 adantr 
 |-  ( ( ph /\ a e. RR ) -> A e. V )
28 4 adantlr 
 |-  ( ( ( ph /\ a e. RR ) /\ x e. A ) -> B e. RR )
29 5 adantlr 
 |-  ( ( ( ph /\ a e. RR ) /\ x e. C ) -> D e. RR )
30 6 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
31 7 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( x e. C |-> D ) e. ( SMblFn ` S ) )
32 simpr 
 |-  ( ( ph /\ a e. RR ) -> a e. RR )
33 fveq1 
 |-  ( p = q -> ( p ` 2 ) = ( q ` 2 ) )
34 fveq1 
 |-  ( p = q -> ( p ` 3 ) = ( q ` 3 ) )
35 33 34 oveq12d 
 |-  ( p = q -> ( ( p ` 2 ) (,) ( p ` 3 ) ) = ( ( q ` 2 ) (,) ( q ` 3 ) ) )
36 35 raleqdv 
 |-  ( p = q -> ( A. v e. ( ( p ` 2 ) (,) ( p ` 3 ) ) ( u x. v ) < a <-> A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < a ) )
37 36 ralbidv 
 |-  ( p = q -> ( A. u e. ( ( p ` 0 ) (,) ( p ` 1 ) ) A. v e. ( ( p ` 2 ) (,) ( p ` 3 ) ) ( u x. v ) < a <-> A. u e. ( ( p ` 0 ) (,) ( p ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < a ) )
38 fveq1 
 |-  ( p = q -> ( p ` 0 ) = ( q ` 0 ) )
39 fveq1 
 |-  ( p = q -> ( p ` 1 ) = ( q ` 1 ) )
40 38 39 oveq12d 
 |-  ( p = q -> ( ( p ` 0 ) (,) ( p ` 1 ) ) = ( ( q ` 0 ) (,) ( q ` 1 ) ) )
41 40 raleqdv 
 |-  ( p = q -> ( A. u e. ( ( p ` 0 ) (,) ( p ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < a <-> A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < a ) )
42 37 41 bitrd 
 |-  ( p = q -> ( A. u e. ( ( p ` 0 ) (,) ( p ` 1 ) ) A. v e. ( ( p ` 2 ) (,) ( p ` 3 ) ) ( u x. v ) < a <-> A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < a ) )
43 42 cbvrabv 
 |-  { p e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( p ` 0 ) (,) ( p ` 1 ) ) A. v e. ( ( p ` 2 ) (,) ( p ` 3 ) ) ( u x. v ) < a } = { q e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( q ` 0 ) (,) ( q ` 1 ) ) A. v e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ( u x. v ) < a }
44 eqid 
 |-  ( q e. { p e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( p ` 0 ) (,) ( p ` 1 ) ) A. v e. ( ( p ` 2 ) (,) ( p ` 3 ) ) ( u x. v ) < a } |-> { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } ) = ( q e. { p e. ( QQ ^m ( 0 ... 3 ) ) | A. u e. ( ( p ` 0 ) (,) ( p ` 1 ) ) A. v e. ( ( p ` 2 ) (,) ( p ` 3 ) ) ( u x. v ) < a } |-> { x e. ( A i^i C ) | ( B e. ( ( q ` 0 ) (,) ( q ` 1 ) ) /\ D e. ( ( q ` 2 ) (,) ( q ` 3 ) ) ) } )
45 25 26 27 28 29 30 31 32 43 44 smfmullem4 
 |-  ( ( ph /\ a e. RR ) -> { x e. ( A i^i C ) | ( B x. D ) < a } e. ( S |`t ( A i^i C ) ) )
46 1 8 2 18 23 45 issmfdmpt 
 |-  ( ph -> ( x e. ( A i^i C ) |-> ( B x. D ) ) e. ( SMblFn ` S ) )