Metamath Proof Explorer

Theorem smfadd

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

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

Proof

Step Hyp Ref Expression
1 smfadd.x 
 |-  F/ x ph
2 smfadd.s 
 |-  ( ph -> S e. SAlg )
3 smfadd.a 
 |-  ( ph -> A e. V )
4 smfadd.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
5 smfadd.d 
 |-  ( ( ph /\ x e. C ) -> D e. RR )
6 smfadd.m 
 |-  ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
7 smfadd.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 readdcld 
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> ( B + D ) e. RR )
24 eqid 
 |-  ( x e. ( A i^i C ) |-> ( B + D ) ) = ( x e. ( A i^i C ) |-> ( B + D ) )
25 1 23 24 fmptdf 
 |-  ( ph -> ( x e. ( A i^i C ) |-> ( B + D ) ) : ( A i^i C ) --> RR )
26 25 fvmptelcdm 
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> ( B + D ) e. RR )
27 nfv 
 |-  F/ x a e. RR
28 1 27 nfan 
 |-  F/ x ( ph /\ a e. RR )
29 2 adantr 
 |-  ( ( ph /\ a e. RR ) -> S e. SAlg )
30 3 adantr 
 |-  ( ( ph /\ a e. RR ) -> A e. V )
31 4 adantlr 
 |-  ( ( ( ph /\ a e. RR ) /\ x e. A ) -> B e. RR )
32 5 adantlr 
 |-  ( ( ( ph /\ a e. RR ) /\ x e. C ) -> D e. RR )
33 6 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
34 7 adantr 
 |-  ( ( ph /\ a e. RR ) -> ( x e. C |-> D ) e. ( SMblFn ` S ) )
35 simpr 
 |-  ( ( ph /\ a e. RR ) -> a e. RR )
36 oveq2 
 |-  ( r = q -> ( p + r ) = ( p + q ) )
37 36 breq1d 
 |-  ( r = q -> ( ( p + r ) < a <-> ( p + q ) < a ) )
38 37 cbvrabv 
 |-  { r e. QQ | ( p + r ) < a } = { q e. QQ | ( p + q ) < a }
39 38 mpteq2i 
 |-  ( p e. QQ |-> { r e. QQ | ( p + r ) < a } ) = ( p e. QQ |-> { q e. QQ | ( p + q ) < a } )
40 28 29 30 31 32 33 34 35 39 smfaddlem2 
 |-  ( ( ph /\ a e. RR ) -> { x e. ( A i^i C ) | ( B + D ) < a } e. ( S |`t ( A i^i C ) ) )
41 1 8 2 18 26 40 issmfdmpt 
 |-  ( ph -> ( x e. ( A i^i C ) |-> ( B + D ) ) e. ( SMblFn ` S ) )