Metamath Proof Explorer

Theorem mbfmco2

Description: The pair building of two measurable functions is measurable. ( cf. cnmpt1t ). (Contributed by Thierry Arnoux, 6-Jun-2017)

Ref Expression
Hypotheses mbfmco.1 
|- ( ph -> R e. U. ran sigAlgebra )
mbfmco.2 
|- ( ph -> S e. U. ran sigAlgebra )
mbfmco.3 
|- ( ph -> T e. U. ran sigAlgebra )
mbfmco2.4 
|- ( ph -> F e. ( R MblFnM S ) )
mbfmco2.5 
|- ( ph -> G e. ( R MblFnM T ) )
mbfmco2.6 
|- H = ( x e. U. R |-> <. ( F ` x ) , ( G ` x ) >. )
Assertion mbfmco2 
|- ( ph -> H e. ( R MblFnM ( S sX T ) ) )

Proof

Step Hyp Ref Expression
1 mbfmco.1 
 |-  ( ph -> R e. U. ran sigAlgebra )
2 mbfmco.2 
 |-  ( ph -> S e. U. ran sigAlgebra )
3 mbfmco.3 
 |-  ( ph -> T e. U. ran sigAlgebra )
4 mbfmco2.4 
 |-  ( ph -> F e. ( R MblFnM S ) )
5 mbfmco2.5 
 |-  ( ph -> G e. ( R MblFnM T ) )
6 mbfmco2.6 
 |-  H = ( x e. U. R |-> <. ( F ` x ) , ( G ` x ) >. )
7 1 2 4 mbfmf 
 |-  ( ph -> F : U. R --> U. S )
8 7 ffvelrnda 
 |-  ( ( ph /\ x e. U. R ) -> ( F ` x ) e. U. S )
9 1 3 5 mbfmf 
 |-  ( ph -> G : U. R --> U. T )
10 9 ffvelrnda 
 |-  ( ( ph /\ x e. U. R ) -> ( G ` x ) e. U. T )
11 opelxpi 
 |-  ( ( ( F ` x ) e. U. S /\ ( G ` x ) e. U. T ) -> <. ( F ` x ) , ( G ` x ) >. e. ( U. S X. U. T ) )
12 8 10 11 syl2anc 
 |-  ( ( ph /\ x e. U. R ) -> <. ( F ` x ) , ( G ` x ) >. e. ( U. S X. U. T ) )
13 sxuni 
 |-  ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( U. S X. U. T ) = U. ( S sX T ) )
14 2 3 13 syl2anc 
 |-  ( ph -> ( U. S X. U. T ) = U. ( S sX T ) )
15 14 adantr 
 |-  ( ( ph /\ x e. U. R ) -> ( U. S X. U. T ) = U. ( S sX T ) )
16 12 15 eleqtrd 
 |-  ( ( ph /\ x e. U. R ) -> <. ( F ` x ) , ( G ` x ) >. e. U. ( S sX T ) )
17 16 6 fmptd 
 |-  ( ph -> H : U. R --> U. ( S sX T ) )
18 eqid 
 |-  ( a e. S , b e. T |-> ( a X. b ) ) = ( a e. S , b e. T |-> ( a X. b ) )
19 vex 
 |-  a e. _V
20 vex 
 |-  b e. _V
21 19 20 xpex 
 |-  ( a X. b ) e. _V
22 18 21 elrnmpo 
 |-  ( c e. ran ( a e. S , b e. T |-> ( a X. b ) ) <-> E. a e. S E. b e. T c = ( a X. b ) )
23 simp3 
 |-  ( ( ph /\ ( a e. S /\ b e. T ) /\ c = ( a X. b ) ) -> c = ( a X. b ) )
24 23 imaeq2d 
 |-  ( ( ph /\ ( a e. S /\ b e. T ) /\ c = ( a X. b ) ) -> ( `' H " c ) = ( `' H " ( a X. b ) ) )
25 simp1 
 |-  ( ( ph /\ ( a e. S /\ b e. T ) /\ c = ( a X. b ) ) -> ph )
26 simp2l 
 |-  ( ( ph /\ ( a e. S /\ b e. T ) /\ c = ( a X. b ) ) -> a e. S )
27 simp2r 
 |-  ( ( ph /\ ( a e. S /\ b e. T ) /\ c = ( a X. b ) ) -> b e. T )
28 7 9 6 xppreima2 
 |-  ( ph -> ( `' H " ( a X. b ) ) = ( ( `' F " a ) i^i ( `' G " b ) ) )
29 28 3ad2ant1 
 |-  ( ( ph /\ a e. S /\ b e. T ) -> ( `' H " ( a X. b ) ) = ( ( `' F " a ) i^i ( `' G " b ) ) )
30 1 3ad2ant1 
 |-  ( ( ph /\ a e. S /\ b e. T ) -> R e. U. ran sigAlgebra )
31 2 3ad2ant1 
 |-  ( ( ph /\ a e. S /\ b e. T ) -> S e. U. ran sigAlgebra )
32 4 3ad2ant1 
 |-  ( ( ph /\ a e. S /\ b e. T ) -> F e. ( R MblFnM S ) )
33 simp2 
 |-  ( ( ph /\ a e. S /\ b e. T ) -> a e. S )
34 30 31 32 33 mbfmcnvima 
 |-  ( ( ph /\ a e. S /\ b e. T ) -> ( `' F " a ) e. R )
35 3 3ad2ant1 
 |-  ( ( ph /\ a e. S /\ b e. T ) -> T e. U. ran sigAlgebra )
36 5 3ad2ant1 
 |-  ( ( ph /\ a e. S /\ b e. T ) -> G e. ( R MblFnM T ) )
37 simp3 
 |-  ( ( ph /\ a e. S /\ b e. T ) -> b e. T )
38 30 35 36 37 mbfmcnvima 
 |-  ( ( ph /\ a e. S /\ b e. T ) -> ( `' G " b ) e. R )
39 inelsiga 
 |-  ( ( R e. U. ran sigAlgebra /\ ( `' F " a ) e. R /\ ( `' G " b ) e. R ) -> ( ( `' F " a ) i^i ( `' G " b ) ) e. R )
40 30 34 38 39 syl3anc 
 |-  ( ( ph /\ a e. S /\ b e. T ) -> ( ( `' F " a ) i^i ( `' G " b ) ) e. R )
41 29 40 eqeltrd 
 |-  ( ( ph /\ a e. S /\ b e. T ) -> ( `' H " ( a X. b ) ) e. R )
42 25 26 27 41 syl3anc 
 |-  ( ( ph /\ ( a e. S /\ b e. T ) /\ c = ( a X. b ) ) -> ( `' H " ( a X. b ) ) e. R )
43 24 42 eqeltrd 
 |-  ( ( ph /\ ( a e. S /\ b e. T ) /\ c = ( a X. b ) ) -> ( `' H " c ) e. R )
44 43 3expia 
 |-  ( ( ph /\ ( a e. S /\ b e. T ) ) -> ( c = ( a X. b ) -> ( `' H " c ) e. R ) )
45 44 rexlimdvva 
 |-  ( ph -> ( E. a e. S E. b e. T c = ( a X. b ) -> ( `' H " c ) e. R ) )
46 45 imp 
 |-  ( ( ph /\ E. a e. S E. b e. T c = ( a X. b ) ) -> ( `' H " c ) e. R )
47 22 46 sylan2b 
 |-  ( ( ph /\ c e. ran ( a e. S , b e. T |-> ( a X. b ) ) ) -> ( `' H " c ) e. R )
48 47 ralrimiva 
 |-  ( ph -> A. c e. ran ( a e. S , b e. T |-> ( a X. b ) ) ( `' H " c ) e. R )
49 eqid 
 |-  ran ( a e. S , b e. T |-> ( a X. b ) ) = ran ( a e. S , b e. T |-> ( a X. b ) )
50 49 txbasex 
 |-  ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ran ( a e. S , b e. T |-> ( a X. b ) ) e. _V )
51 2 3 50 syl2anc 
 |-  ( ph -> ran ( a e. S , b e. T |-> ( a X. b ) ) e. _V )
52 49 sxval 
 |-  ( ( S e. U. ran sigAlgebra /\ T e. U. ran sigAlgebra ) -> ( S sX T ) = ( sigaGen ` ran ( a e. S , b e. T |-> ( a X. b ) ) ) )
53 2 3 52 syl2anc 
 |-  ( ph -> ( S sX T ) = ( sigaGen ` ran ( a e. S , b e. T |-> ( a X. b ) ) ) )
54 51 1 53 imambfm 
 |-  ( ph -> ( H e. ( R MblFnM ( S sX T ) ) <-> ( H : U. R --> U. ( S sX T ) /\ A. c e. ran ( a e. S , b e. T |-> ( a X. b ) ) ( `' H " c ) e. R ) ) )
55 17 48 54 mpbir2and 
 |-  ( ph -> H e. ( R MblFnM ( S sX T ) ) )