Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mbfmco Structured version   Visualization version   GIF version

Theorem mbfmco 32239
Description: The composition of two measurable functions is measurable. See cnmpt11 22824. (Contributed by Thierry Arnoux, 4-Jun-2017.)
Hypotheses
Ref Expression
mbfmco.1 (𝜑𝑅 ran sigAlgebra)
mbfmco.2 (𝜑𝑆 ran sigAlgebra)
mbfmco.3 (𝜑𝑇 ran sigAlgebra)
mbfmco.4 (𝜑𝐹 ∈ (𝑅MblFnM𝑆))
mbfmco.5 (𝜑𝐺 ∈ (𝑆MblFnM𝑇))
Assertion
Ref Expression
mbfmco (𝜑 → (𝐺𝐹) ∈ (𝑅MblFnM𝑇))

Proof of Theorem mbfmco
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 mbfmco.2 . . . . 5 (𝜑𝑆 ran sigAlgebra)
2 mbfmco.3 . . . . 5 (𝜑𝑇 ran sigAlgebra)
3 mbfmco.5 . . . . 5 (𝜑𝐺 ∈ (𝑆MblFnM𝑇))
41, 2, 3mbfmf 32230 . . . 4 (𝜑𝐺: 𝑆 𝑇)
5 mbfmco.1 . . . . 5 (𝜑𝑅 ran sigAlgebra)
6 mbfmco.4 . . . . 5 (𝜑𝐹 ∈ (𝑅MblFnM𝑆))
75, 1, 6mbfmf 32230 . . . 4 (𝜑𝐹: 𝑅 𝑆)
8 fco 6616 . . . 4 ((𝐺: 𝑆 𝑇𝐹: 𝑅 𝑆) → (𝐺𝐹): 𝑅 𝑇)
94, 7, 8syl2anc 584 . . 3 (𝜑 → (𝐺𝐹): 𝑅 𝑇)
10 unielsiga 32104 . . . . 5 (𝑇 ran sigAlgebra → 𝑇𝑇)
112, 10syl 17 . . . 4 (𝜑 𝑇𝑇)
12 unielsiga 32104 . . . . 5 (𝑅 ran sigAlgebra → 𝑅𝑅)
135, 12syl 17 . . . 4 (𝜑 𝑅𝑅)
1411, 13elmapd 8616 . . 3 (𝜑 → ((𝐺𝐹) ∈ ( 𝑇m 𝑅) ↔ (𝐺𝐹): 𝑅 𝑇))
159, 14mpbird 256 . 2 (𝜑 → (𝐺𝐹) ∈ ( 𝑇m 𝑅))
16 cnvco 5787 . . . . . 6 (𝐺𝐹) = (𝐹𝐺)
1716imaeq1i 5959 . . . . 5 ((𝐺𝐹) “ 𝑎) = ((𝐹𝐺) “ 𝑎)
18 imaco 6148 . . . . 5 ((𝐹𝐺) “ 𝑎) = (𝐹 “ (𝐺𝑎))
1917, 18eqtri 2766 . . . 4 ((𝐺𝐹) “ 𝑎) = (𝐹 “ (𝐺𝑎))
205adantr 481 . . . . 5 ((𝜑𝑎𝑇) → 𝑅 ran sigAlgebra)
211adantr 481 . . . . 5 ((𝜑𝑎𝑇) → 𝑆 ran sigAlgebra)
226adantr 481 . . . . 5 ((𝜑𝑎𝑇) → 𝐹 ∈ (𝑅MblFnM𝑆))
232adantr 481 . . . . . 6 ((𝜑𝑎𝑇) → 𝑇 ran sigAlgebra)
243adantr 481 . . . . . 6 ((𝜑𝑎𝑇) → 𝐺 ∈ (𝑆MblFnM𝑇))
25 simpr 485 . . . . . 6 ((𝜑𝑎𝑇) → 𝑎𝑇)
2621, 23, 24, 25mbfmcnvima 32232 . . . . 5 ((𝜑𝑎𝑇) → (𝐺𝑎) ∈ 𝑆)
2720, 21, 22, 26mbfmcnvima 32232 . . . 4 ((𝜑𝑎𝑇) → (𝐹 “ (𝐺𝑎)) ∈ 𝑅)
2819, 27eqeltrid 2843 . . 3 ((𝜑𝑎𝑇) → ((𝐺𝐹) “ 𝑎) ∈ 𝑅)
2928ralrimiva 3108 . 2 (𝜑 → ∀𝑎𝑇 ((𝐺𝐹) “ 𝑎) ∈ 𝑅)
305, 2ismbfm 32227 . 2 (𝜑 → ((𝐺𝐹) ∈ (𝑅MblFnM𝑇) ↔ ((𝐺𝐹) ∈ ( 𝑇m 𝑅) ∧ ∀𝑎𝑇 ((𝐺𝐹) “ 𝑎) ∈ 𝑅)))
3115, 29, 30mpbir2and 710 1 (𝜑 → (𝐺𝐹) ∈ (𝑅MblFnM𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2106  wral 3064   cuni 4839  ccnv 5583  ran crn 5585  cima 5587  ccom 5588  wf 6422  (class class class)co 7267  m cmap 8602  sigAlgebracsiga 32084  MblFnMcmbfm 32225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5221  ax-nul 5228  ax-pow 5286  ax-pr 5350  ax-un 7578
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3431  df-sbc 3716  df-csb 3832  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5074  df-opab 5136  df-mpt 5157  df-id 5484  df-xp 5590  df-rel 5591  df-cnv 5592  df-co 5593  df-dm 5594  df-rn 5595  df-res 5596  df-ima 5597  df-iota 6384  df-fun 6428  df-fn 6429  df-f 6430  df-fv 6434  df-ov 7270  df-oprab 7271  df-mpo 7272  df-1st 7820  df-2nd 7821  df-map 8604  df-siga 32085  df-mbfm 32226
This theorem is referenced by:  rrvadd  32427  rrvmulc  32428
  Copyright terms: Public domain W3C validator