Metamath Proof Explorer

Theorem smfaddlem2

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 smfaddlem2.x 
|- F/ x ph
smfaddlem2.s 
|- ( ph -> S e. SAlg )
smfaddlem2.a 
|- ( ph -> A e. V )
smfaddlem2.b 
|- ( ( ph /\ x e. A ) -> B e. RR )
smfaddlem2.d 
|- ( ( ph /\ x e. C ) -> D e. RR )
smfaddlem2.m 
|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
smfaddlem2.7 
|- ( ph -> ( x e. C |-> D ) e. ( SMblFn ` S ) )
smfaddlem2.r 
|- ( ph -> R e. RR )
smfaddlem2.k 
|- K = ( p e. QQ |-> { q e. QQ | ( p + q ) < R } )
Assertion smfaddlem2 
|- ( ph -> { x e. ( A i^i C ) | ( B + D ) < R } e. ( S |`t ( A i^i C ) ) )

Proof

Step Hyp Ref Expression
1 smfaddlem2.x 
 |-  F/ x ph
2 smfaddlem2.s 
 |-  ( ph -> S e. SAlg )
3 smfaddlem2.a 
 |-  ( ph -> A e. V )
4 smfaddlem2.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
5 smfaddlem2.d 
 |-  ( ( ph /\ x e. C ) -> D e. RR )
6 smfaddlem2.m 
 |-  ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
7 smfaddlem2.7 
 |-  ( ph -> ( x e. C |-> D ) e. ( SMblFn ` S ) )
8 smfaddlem2.r 
 |-  ( ph -> R e. RR )
9 smfaddlem2.k 
 |-  K = ( p e. QQ |-> { q e. QQ | ( p + q ) < R } )
10 1 4 5 8 9 smfaddlem1 
 |-  ( ph -> { x e. ( A i^i C ) | ( B + D ) < R } = U_ p e. QQ U_ q e. ( K ` p ) { x e. ( A i^i C ) | ( B < p /\ D < q ) } )
11 elinel1 
 |-  ( x e. ( A i^i C ) -> x e. A )
12 11 adantl 
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> x e. A )
13 1 12 ssdf 
 |-  ( ph -> ( A i^i C ) C_ A )
14 3 13 ssexd 
 |-  ( ph -> ( A i^i C ) e. _V )
15 eqid 
 |-  ( S |`t ( A i^i C ) ) = ( S |`t ( A i^i C ) )
16 2 14 15 subsalsal 
 |-  ( ph -> ( S |`t ( A i^i C ) ) e. SAlg )
17 qct 
 |-  QQ ~<_ _om
18 17 a1i 
 |-  ( ph -> QQ ~<_ _om )
19 16 adantr 
 |-  ( ( ph /\ p e. QQ ) -> ( S |`t ( A i^i C ) ) e. SAlg )
20 qex 
 |-  QQ e. _V
21 20 a1i 
 |-  ( ( ph /\ p e. QQ ) -> QQ e. _V )
22 9 a1i 
 |-  ( ph -> K = ( p e. QQ |-> { q e. QQ | ( p + q ) < R } ) )
23 20 rabex 
 |-  { q e. QQ | ( p + q ) < R } e. _V
24 23 a1i 
 |-  ( ( ph /\ p e. QQ ) -> { q e. QQ | ( p + q ) < R } e. _V )
25 22 24 fvmpt2d 
 |-  ( ( ph /\ p e. QQ ) -> ( K ` p ) = { q e. QQ | ( p + q ) < R } )
26 ssrab2 
 |-  { q e. QQ | ( p + q ) < R } C_ QQ
27 25 26 eqsstrdi 
 |-  ( ( ph /\ p e. QQ ) -> ( K ` p ) C_ QQ )
28 ssdomg 
 |-  ( QQ e. _V -> ( ( K ` p ) C_ QQ -> ( K ` p ) ~<_ QQ ) )
29 21 27 28 sylc 
 |-  ( ( ph /\ p e. QQ ) -> ( K ` p ) ~<_ QQ )
30 17 a1i 
 |-  ( ( ph /\ p e. QQ ) -> QQ ~<_ _om )
31 domtr 
 |-  ( ( ( K ` p ) ~<_ QQ /\ QQ ~<_ _om ) -> ( K ` p ) ~<_ _om )
32 29 30 31 syl2anc 
 |-  ( ( ph /\ p e. QQ ) -> ( K ` p ) ~<_ _om )
33 inrab 
 |-  ( { x e. ( A i^i C ) | B < p } i^i { x e. ( A i^i C ) | D < q } ) = { x e. ( A i^i C ) | ( B < p /\ D < q ) }
34 16 ad2antrr 
 |-  ( ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) ) -> ( S |`t ( A i^i C ) ) e. SAlg )
35 nfv 
 |-  F/ x p e. QQ
36 1 35 nfan 
 |-  F/ x ( ph /\ p e. QQ )
37 nfv 
 |-  F/ x q e. ( K ` p )
38 36 37 nfan 
 |-  F/ x ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) )
39 2 ad2antrr 
 |-  ( ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) ) -> S e. SAlg )
40 12 4 syldan 
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> B e. RR )
41 40 ad4ant14 
 |-  ( ( ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) ) /\ x e. ( A i^i C ) ) -> B e. RR )
42 2 6 13 sssmfmpt 
 |-  ( ph -> ( x e. ( A i^i C ) |-> B ) e. ( SMblFn ` S ) )
43 42 ad2antrr 
 |-  ( ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) ) -> ( x e. ( A i^i C ) |-> B ) e. ( SMblFn ` S ) )
44 qre 
 |-  ( p e. QQ -> p e. RR )
45 44 ad2antlr 
 |-  ( ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) ) -> p e. RR )
46 38 39 41 43 45 smfpimltmpt 
 |-  ( ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) ) -> { x e. ( A i^i C ) | B < p } e. ( S |`t ( A i^i C ) ) )
47 elinel2 
 |-  ( x e. ( A i^i C ) -> x e. C )
48 47 adantl 
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> x e. C )
49 48 5 syldan 
 |-  ( ( ph /\ x e. ( A i^i C ) ) -> D e. RR )
50 49 ad4ant14 
 |-  ( ( ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) ) /\ x e. ( A i^i C ) ) -> D e. RR )
51 1 48 ssdf 
 |-  ( ph -> ( A i^i C ) C_ C )
52 2 7 51 sssmfmpt 
 |-  ( ph -> ( x e. ( A i^i C ) |-> D ) e. ( SMblFn ` S ) )
53 52 ad2antrr 
 |-  ( ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) ) -> ( x e. ( A i^i C ) |-> D ) e. ( SMblFn ` S ) )
54 44 ssriv 
 |-  QQ C_ RR
55 27 sselda 
 |-  ( ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) ) -> q e. QQ )
56 54 55 sseldi 
 |-  ( ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) ) -> q e. RR )
57 38 39 50 53 56 smfpimltmpt 
 |-  ( ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) ) -> { x e. ( A i^i C ) | D < q } e. ( S |`t ( A i^i C ) ) )
58 34 46 57 salincld 
 |-  ( ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) ) -> ( { x e. ( A i^i C ) | B < p } i^i { x e. ( A i^i C ) | D < q } ) e. ( S |`t ( A i^i C ) ) )
59 33 58 eqeltrrid 
 |-  ( ( ( ph /\ p e. QQ ) /\ q e. ( K ` p ) ) -> { x e. ( A i^i C ) | ( B < p /\ D < q ) } e. ( S |`t ( A i^i C ) ) )
60 19 32 59 saliuncl 
 |-  ( ( ph /\ p e. QQ ) -> U_ q e. ( K ` p ) { x e. ( A i^i C ) | ( B < p /\ D < q ) } e. ( S |`t ( A i^i C ) ) )
61 16 18 60 saliuncl 
 |-  ( ph -> U_ p e. QQ U_ q e. ( K ` p ) { x e. ( A i^i C ) | ( B < p /\ D < q ) } e. ( S |`t ( A i^i C ) ) )
62 10 61 eqeltrd 
 |-  ( ph -> { x e. ( A i^i C ) | ( B + D ) < R } e. ( S |`t ( A i^i C ) ) )