mbfconst

Description: A constant function is measurable. (Contributed by Mario Carneiro, 17-Jun-2014)

		Ref	Expression
	Assertion	mbfconst	$⊢ (A \in dom vol \land B \in ℂ) \to A \times \{B\} \in MblFn$

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((A \in dom vol \land B \in ℂ) \land x \in A) \to B \in ℂ$
2		fconstmpt	$⊢ A \times \{B\} = (x \in A ⟼ B)$
3	1 2	fmptd	$⊢ (A \in dom vol \land B \in ℂ) \to (A \times \{B\}) : A ⟶ ℂ$
4		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
5	4	adantr	$⊢ (A \in dom vol \land B \in ℂ) \to A \subseteq ℝ$
6		cnex	$⊢ ℂ \in V$
7		reex	$⊢ ℝ \in V$
8		elpm2r	$⊢ ((ℂ \in V \land ℝ \in V) \land ((A \times \{B\}) : A ⟶ ℂ \land A \subseteq ℝ)) \to A \times \{B\} \in (ℂ ↑_{𝑝𝑚} ℝ)$
9	6 7 8	mpanl12	$⊢ ((A \times \{B\}) : A ⟶ ℂ \land A \subseteq ℝ) \to A \times \{B\} \in (ℂ ↑_{𝑝𝑚} ℝ)$
10	3 5 9	syl2anc	$⊢ (A \in dom vol \land B \in ℂ) \to A \times \{B\} \in (ℂ ↑_{𝑝𝑚} ℝ)$
11	2	a1i	$⊢ (A \in dom vol \land B \in ℂ) \to A \times \{B\} = (x \in A ⟼ B)$
12		ref	$⊢ ℜ : ℂ ⟶ ℝ$
13	12	a1i	$⊢ (A \in dom vol \land B \in ℂ) \to ℜ : ℂ ⟶ ℝ$
14	13	feqmptd	$⊢ (A \in dom vol \land B \in ℂ) \to ℜ = (y \in ℂ ⟼ ℜ (y))$
15		fveq2	$⊢ y = B \to ℜ (y) = ℜ (B)$
16	1 11 14 15	fmptco	$⊢ (A \in dom vol \land B \in ℂ) \to ℜ \circ (A \times \{B\}) = (x \in A ⟼ ℜ (B))$
17		fconstmpt	$⊢ A \times \{ℜ (B)\} = (x \in A ⟼ ℜ (B))$
18	16 17	eqtr4di	$⊢ (A \in dom vol \land B \in ℂ) \to ℜ \circ (A \times \{B\}) = A \times \{ℜ (B)\}$
19	18	cnveqd	$⊢ (A \in dom vol \land B \in ℂ) \to {(ℜ \circ (A \times \{B\}))}^{-1} = {(A \times \{ℜ (B)\})}^{-1}$
20	19	imaeq1d	$⊢ (A \in dom vol \land B \in ℂ) \to {(ℜ \circ (A \times \{B\}))}^{-1} [y] = {(A \times \{ℜ (B)\})}^{-1} [y]$
21		recl	$⊢ B \in ℂ \to ℜ (B) \in ℝ$
22		mbfconstlem	$⊢ (A \in dom vol \land ℜ (B) \in ℝ) \to {(A \times \{ℜ (B)\})}^{-1} [y] \in dom vol$
23	21 22	sylan2	$⊢ (A \in dom vol \land B \in ℂ) \to {(A \times \{ℜ (B)\})}^{-1} [y] \in dom vol$
24	20 23	eqeltrd	$⊢ (A \in dom vol \land B \in ℂ) \to {(ℜ \circ (A \times \{B\}))}^{-1} [y] \in dom vol$
25		imf	$⊢ ℑ : ℂ ⟶ ℝ$
26	25	a1i	$⊢ (A \in dom vol \land B \in ℂ) \to ℑ : ℂ ⟶ ℝ$
27	26	feqmptd	$⊢ (A \in dom vol \land B \in ℂ) \to ℑ = (y \in ℂ ⟼ ℑ (y))$
28		fveq2	$⊢ y = B \to ℑ (y) = ℑ (B)$
29	1 11 27 28	fmptco	$⊢ (A \in dom vol \land B \in ℂ) \to ℑ \circ (A \times \{B\}) = (x \in A ⟼ ℑ (B))$
30		fconstmpt	$⊢ A \times \{ℑ (B)\} = (x \in A ⟼ ℑ (B))$
31	29 30	eqtr4di	$⊢ (A \in dom vol \land B \in ℂ) \to ℑ \circ (A \times \{B\}) = A \times \{ℑ (B)\}$
32	31	cnveqd	$⊢ (A \in dom vol \land B \in ℂ) \to {(ℑ \circ (A \times \{B\}))}^{-1} = {(A \times \{ℑ (B)\})}^{-1}$
33	32	imaeq1d	$⊢ (A \in dom vol \land B \in ℂ) \to {(ℑ \circ (A \times \{B\}))}^{-1} [y] = {(A \times \{ℑ (B)\})}^{-1} [y]$
34		imcl	$⊢ B \in ℂ \to ℑ (B) \in ℝ$
35		mbfconstlem	$⊢ (A \in dom vol \land ℑ (B) \in ℝ) \to {(A \times \{ℑ (B)\})}^{-1} [y] \in dom vol$
36	34 35	sylan2	$⊢ (A \in dom vol \land B \in ℂ) \to {(A \times \{ℑ (B)\})}^{-1} [y] \in dom vol$
37	33 36	eqeltrd	$⊢ (A \in dom vol \land B \in ℂ) \to {(ℑ \circ (A \times \{B\}))}^{-1} [y] \in dom vol$
38	24 37	jca	$⊢ (A \in dom vol \land B \in ℂ) \to ({(ℜ \circ (A \times \{B\}))}^{-1} [y] \in dom vol \land {(ℑ \circ (A \times \{B\}))}^{-1} [y] \in dom vol)$
39	38	ralrimivw	$⊢ (A \in dom vol \land B \in ℂ) \to \forall y \in ran (.) ({(ℜ \circ (A \times \{B\}))}^{-1} [y] \in dom vol \land {(ℑ \circ (A \times \{B\}))}^{-1} [y] \in dom vol)$
40		ismbf1	$⊢ A \times \{B\} \in MblFn \leftrightarrow (A \times \{B\} \in (ℂ ↑_{𝑝𝑚} ℝ) \land \forall y \in ran (.) ({(ℜ \circ (A \times \{B\}))}^{-1} [y] \in dom vol \land {(ℑ \circ (A \times \{B\}))}^{-1} [y] \in dom vol))$
41	10 39 40	sylanbrc	$⊢ (A \in dom vol \land B \in ℂ) \to A \times \{B\} \in MblFn$

Metamath Proof Explorer

Theorem mbfconst

Proof