mbfmul

Description: The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014)

	Ref	Expression
Hypotheses	mbfmul.1	$⊢ φ \to F \in MblFn$
	mbfmul.2	$⊢ φ \to G \in MblFn$
Assertion	mbfmul	$⊢ φ \to F \times_{f} G \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		mbfmul.1	$⊢ φ \to F \in MblFn$
2		mbfmul.2	$⊢ φ \to G \in MblFn$
3		mbff	$⊢ F \in MblFn \to F : dom F ⟶ ℂ$
4	1 3	syl	$⊢ φ \to F : dom F ⟶ ℂ$
5	4	ffnd	$⊢ φ \to F Fn dom F$
6		mbff	$⊢ G \in MblFn \to G : dom G ⟶ ℂ$
7	2 6	syl	$⊢ φ \to G : dom G ⟶ ℂ$
8	7	ffnd	$⊢ φ \to G Fn dom G$
9		mbfdm	$⊢ F \in MblFn \to dom F \in dom vol$
10	1 9	syl	$⊢ φ \to dom F \in dom vol$
11		mbfdm	$⊢ G \in MblFn \to dom G \in dom vol$
12	2 11	syl	$⊢ φ \to dom G \in dom vol$
13		eqid	$⊢ dom F \cap dom G = dom F \cap dom G$
14		eqidd	$⊢ (φ \land x \in dom F) \to F (x) = F (x)$
15		eqidd	$⊢ (φ \land x \in dom G) \to G (x) = G (x)$
16	5 8 10 12 13 14 15	offval	$⊢ φ \to F \times_{f} G = (x \in (dom F \cap dom G) ⟼ F (x) G (x))$
17		elinel1	$⊢ x \in (dom F \cap dom G) \to x \in dom F$
18		ffvelcdm	$⊢ (F : dom F ⟶ ℂ \land x \in dom F) \to F (x) \in ℂ$
19	4 17 18	syl2an	$⊢ (φ \land x \in (dom F \cap dom G)) \to F (x) \in ℂ$
20		elinel2	$⊢ x \in (dom F \cap dom G) \to x \in dom G$
21		ffvelcdm	$⊢ (G : dom G ⟶ ℂ \land x \in dom G) \to G (x) \in ℂ$
22	7 20 21	syl2an	$⊢ (φ \land x \in (dom F \cap dom G)) \to G (x) \in ℂ$
23	19 22	remuld	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℜ (F (x) G (x)) = ℜ (F (x)) ℜ (G (x)) - ℑ (F (x)) ℑ (G (x))$
24	23	mpteq2dva	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x) G (x))) = (x \in (dom F \cap dom G) ⟼ ℜ (F (x)) ℜ (G (x)) - ℑ (F (x)) ℑ (G (x)))$
25		inmbl	$⊢ (dom F \in dom vol \land dom G \in dom vol) \to dom F \cap dom G \in dom vol$
26	10 12 25	syl2anc	$⊢ φ \to dom F \cap dom G \in dom vol$
27		ovexd	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℜ (F (x)) ℜ (G (x)) \in V$
28		ovexd	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℑ (F (x)) ℑ (G (x)) \in V$
29	19	recld	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℜ (F (x)) \in ℝ$
30	22	recld	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℜ (G (x)) \in ℝ$
31		eqidd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x))) = (x \in (dom F \cap dom G) ⟼ ℜ (F (x)))$
32		eqidd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (G (x))) = (x \in (dom F \cap dom G) ⟼ ℜ (G (x)))$
33	26 29 30 31 32	offval2	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℜ (G (x))) = (x \in (dom F \cap dom G) ⟼ ℜ (F (x)) ℜ (G (x)))$
34	19	imcld	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℑ (F (x)) \in ℝ$
35	22	imcld	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℑ (G (x)) \in ℝ$
36		eqidd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) = (x \in (dom F \cap dom G) ⟼ ℑ (F (x)))$
37		eqidd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) = (x \in (dom F \cap dom G) ⟼ ℑ (G (x)))$
38	26 34 35 36 37	offval2	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) = (x \in (dom F \cap dom G) ⟼ ℑ (F (x)) ℑ (G (x)))$
39	26 27 28 33 38	offval2	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℜ (G (x)))) -_{f} ((x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℑ (G (x)))) = (x \in (dom F \cap dom G) ⟼ ℜ (F (x)) ℜ (G (x)) - ℑ (F (x)) ℑ (G (x)))$
40	24 39	eqtr4d	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x) G (x))) = ((x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℜ (G (x)))) -_{f} ((x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℑ (G (x))))$
41		inss1	$⊢ dom F \cap dom G \subseteq dom F$
42		resmpt	$⊢ dom F \cap dom G \subseteq dom F \to {(x \in dom F ⟼ F (x)) ↾}_{(dom F \cap dom G)} = (x \in (dom F \cap dom G) ⟼ F (x))$
43	41 42	ax-mp	$⊢ {(x \in dom F ⟼ F (x)) ↾}_{(dom F \cap dom G)} = (x \in (dom F \cap dom G) ⟼ F (x))$
44	4	feqmptd	$⊢ φ \to F = (x \in dom F ⟼ F (x))$
45	44 1	eqeltrrd	$⊢ φ \to (x \in dom F ⟼ F (x)) \in MblFn$
46		mbfres	$⊢ ((x \in dom F ⟼ F (x)) \in MblFn \land dom F \cap dom G \in dom vol) \to {(x \in dom F ⟼ F (x)) ↾}_{(dom F \cap dom G)} \in MblFn$
47	45 26 46	syl2anc	$⊢ φ \to {(x \in dom F ⟼ F (x)) ↾}_{(dom F \cap dom G)} \in MblFn$
48	43 47	eqeltrrid	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ F (x)) \in MblFn$
49	19	ismbfcn2	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ F (x)) \in MblFn \leftrightarrow ((x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \in MblFn \land (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \in MblFn))$
50	48 49	mpbid	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \in MblFn \land (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \in MblFn)$
51	50	simpld	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \in MblFn$
52		inss2	$⊢ dom F \cap dom G \subseteq dom G$
53		resmpt	$⊢ dom F \cap dom G \subseteq dom G \to {(x \in dom G ⟼ G (x)) ↾}_{(dom F \cap dom G)} = (x \in (dom F \cap dom G) ⟼ G (x))$
54	52 53	ax-mp	$⊢ {(x \in dom G ⟼ G (x)) ↾}_{(dom F \cap dom G)} = (x \in (dom F \cap dom G) ⟼ G (x))$
55	7	feqmptd	$⊢ φ \to G = (x \in dom G ⟼ G (x))$
56	55 2	eqeltrrd	$⊢ φ \to (x \in dom G ⟼ G (x)) \in MblFn$
57		mbfres	$⊢ ((x \in dom G ⟼ G (x)) \in MblFn \land dom F \cap dom G \in dom vol) \to {(x \in dom G ⟼ G (x)) ↾}_{(dom F \cap dom G)} \in MblFn$
58	56 26 57	syl2anc	$⊢ φ \to {(x \in dom G ⟼ G (x)) ↾}_{(dom F \cap dom G)} \in MblFn$
59	54 58	eqeltrrid	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ G (x)) \in MblFn$
60	22	ismbfcn2	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ G (x)) \in MblFn \leftrightarrow ((x \in (dom F \cap dom G) ⟼ ℜ (G (x))) \in MblFn \land (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) \in MblFn))$
61	59 60	mpbid	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ ℜ (G (x))) \in MblFn \land (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) \in MblFn)$
62	61	simpld	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (G (x))) \in MblFn$
63	29	fmpttd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x))) : dom F \cap dom G ⟶ ℝ$
64	30	fmpttd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (G (x))) : dom F \cap dom G ⟶ ℝ$
65	51 62 63 64	mbfmullem	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℜ (G (x))) \in MblFn$
66	50	simprd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \in MblFn$
67	61	simprd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) \in MblFn$
68	34	fmpttd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) : dom F \cap dom G ⟶ ℝ$
69	35	fmpttd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) : dom F \cap dom G ⟶ ℝ$
70	66 67 68 69	mbfmullem	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) \in MblFn$
71	65 70	mbfsub	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℜ (G (x)))) -_{f} ((x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℑ (G (x)))) \in MblFn$
72	40 71	eqeltrd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x) G (x))) \in MblFn$
73	19 22	immuld	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℑ (F (x) G (x)) = ℜ (F (x)) ℑ (G (x)) + ℑ (F (x)) ℜ (G (x))$
74	73	mpteq2dva	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x) G (x))) = (x \in (dom F \cap dom G) ⟼ ℜ (F (x)) ℑ (G (x)) + ℑ (F (x)) ℜ (G (x)))$
75		ovexd	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℜ (F (x)) ℑ (G (x)) \in V$
76		ovexd	$⊢ (φ \land x \in (dom F \cap dom G)) \to ℑ (F (x)) ℜ (G (x)) \in V$
77	26 29 35 31 37	offval2	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) = (x \in (dom F \cap dom G) ⟼ ℜ (F (x)) ℑ (G (x)))$
78	26 34 30 36 32	offval2	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℜ (G (x))) = (x \in (dom F \cap dom G) ⟼ ℑ (F (x)) ℜ (G (x)))$
79	26 75 76 77 78	offval2	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℑ (G (x)))) +_{f} ((x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℜ (G (x)))) = (x \in (dom F \cap dom G) ⟼ ℜ (F (x)) ℑ (G (x)) + ℑ (F (x)) ℜ (G (x)))$
80	74 79	eqtr4d	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x) G (x))) = ((x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℑ (G (x)))) +_{f} ((x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℜ (G (x))))$
81	51 67 63 69	mbfmullem	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℑ (G (x))) \in MblFn$
82	66 62 68 64	mbfmullem	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℜ (G (x))) \in MblFn$
83	81 82	mbfadd	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ ℜ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℑ (G (x)))) +_{f} ((x \in (dom F \cap dom G) ⟼ ℑ (F (x))) \times_{f} (x \in (dom F \cap dom G) ⟼ ℜ (G (x)))) \in MblFn$
84	80 83	eqeltrd	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ ℑ (F (x) G (x))) \in MblFn$
85	19 22	mulcld	$⊢ (φ \land x \in (dom F \cap dom G)) \to F (x) G (x) \in ℂ$
86	85	ismbfcn2	$⊢ φ \to ((x \in (dom F \cap dom G) ⟼ F (x) G (x)) \in MblFn \leftrightarrow ((x \in (dom F \cap dom G) ⟼ ℜ (F (x) G (x))) \in MblFn \land (x \in (dom F \cap dom G) ⟼ ℑ (F (x) G (x))) \in MblFn))$
87	72 84 86	mpbir2and	$⊢ φ \to (x \in (dom F \cap dom G) ⟼ F (x) G (x)) \in MblFn$
88	16 87	eqeltrd	$⊢ φ \to F \times_{f} G \in MblFn$

Metamath Proof Explorer

Theorem mbfmul

Proof