Theorem mbfconst

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

	Ref	Expression
Assertion	mbfconst	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( 𝐴 × { 𝐵 } ) ∈ MblFn )

Proof

Step	Hyp	Ref	Expression
1		simplr	⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
2		fconstmpt	⊢ ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3	1 2	fmptd	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ ℂ )
4		mblss	⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
5	4	adantr	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → 𝐴 ⊆ ℝ )
6		cnex	⊢ ℂ ∈ V
7		reex	⊢ ℝ ∈ V
8		elpm2r	⊢ ( ( ( ℂ ∈ V ∧ ℝ ∈ V ) ∧ ( ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ) → ( 𝐴 × { 𝐵 } ) ∈ ( ℂ ↑pm ℝ ) )
9	6 7 8	mpanl12	⊢ ( ( ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → ( 𝐴 × { 𝐵 } ) ∈ ( ℂ ↑pm ℝ ) )
10	3 5 9	syl2anc	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( 𝐴 × { 𝐵 } ) ∈ ( ℂ ↑pm ℝ ) )
11	2	a1i	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( 𝐴 × { 𝐵 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
12		ref	⊢ ℜ : ℂ ⟶ ℝ
13	12	a1i	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ℜ : ℂ ⟶ ℝ )
14	13	feqmptd	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ℜ = ( 𝑦 ∈ ℂ ↦ ( ℜ ‘ 𝑦 ) ) )
15		fveq2	⊢ ( 𝑦 = 𝐵 → ( ℜ ‘ 𝑦 ) = ( ℜ ‘ 𝐵 ) )
16	1 11 14 15	fmptco	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( ℜ ∘ ( 𝐴 × { 𝐵 } ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) )
17		fconstmpt	⊢ ( 𝐴 × { ( ℜ ‘ 𝐵 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) )
18	16 17	eqtr4di	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( ℜ ∘ ( 𝐴 × { 𝐵 } ) ) = ( 𝐴 × { ( ℜ ‘ 𝐵 ) } ) )
19	18	cnveqd	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ◡ ( ℜ ∘ ( 𝐴 × { 𝐵 } ) ) = ◡ ( 𝐴 × { ( ℜ ‘ 𝐵 ) } ) )
20	19	imaeq1d	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( ◡ ( ℜ ∘ ( 𝐴 × { 𝐵 } ) ) “ 𝑦 ) = ( ◡ ( 𝐴 × { ( ℜ ‘ 𝐵 ) } ) “ 𝑦 ) )
21		recl	⊢ ( 𝐵 ∈ ℂ → ( ℜ ‘ 𝐵 ) ∈ ℝ )
22		mbfconstlem	⊢ ( ( 𝐴 ∈ dom vol ∧ ( ℜ ‘ 𝐵 ) ∈ ℝ ) → ( ◡ ( 𝐴 × { ( ℜ ‘ 𝐵 ) } ) “ 𝑦 ) ∈ dom vol )
23	21 22	sylan2	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( ◡ ( 𝐴 × { ( ℜ ‘ 𝐵 ) } ) “ 𝑦 ) ∈ dom vol )
24	20 23	eqeltrd	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( ◡ ( ℜ ∘ ( 𝐴 × { 𝐵 } ) ) “ 𝑦 ) ∈ dom vol )
25		imf	⊢ ℑ : ℂ ⟶ ℝ
26	25	a1i	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ℑ : ℂ ⟶ ℝ )
27	26	feqmptd	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ℑ = ( 𝑦 ∈ ℂ ↦ ( ℑ ‘ 𝑦 ) ) )
28		fveq2	⊢ ( 𝑦 = 𝐵 → ( ℑ ‘ 𝑦 ) = ( ℑ ‘ 𝐵 ) )
29	1 11 27 28	fmptco	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( ℑ ∘ ( 𝐴 × { 𝐵 } ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) )
30		fconstmpt	⊢ ( 𝐴 × { ( ℑ ‘ 𝐵 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) )
31	29 30	eqtr4di	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( ℑ ∘ ( 𝐴 × { 𝐵 } ) ) = ( 𝐴 × { ( ℑ ‘ 𝐵 ) } ) )
32	31	cnveqd	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ◡ ( ℑ ∘ ( 𝐴 × { 𝐵 } ) ) = ◡ ( 𝐴 × { ( ℑ ‘ 𝐵 ) } ) )
33	32	imaeq1d	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( ◡ ( ℑ ∘ ( 𝐴 × { 𝐵 } ) ) “ 𝑦 ) = ( ◡ ( 𝐴 × { ( ℑ ‘ 𝐵 ) } ) “ 𝑦 ) )
34		imcl	⊢ ( 𝐵 ∈ ℂ → ( ℑ ‘ 𝐵 ) ∈ ℝ )
35		mbfconstlem	⊢ ( ( 𝐴 ∈ dom vol ∧ ( ℑ ‘ 𝐵 ) ∈ ℝ ) → ( ◡ ( 𝐴 × { ( ℑ ‘ 𝐵 ) } ) “ 𝑦 ) ∈ dom vol )
36	34 35	sylan2	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( ◡ ( 𝐴 × { ( ℑ ‘ 𝐵 ) } ) “ 𝑦 ) ∈ dom vol )
37	33 36	eqeltrd	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( ◡ ( ℑ ∘ ( 𝐴 × { 𝐵 } ) ) “ 𝑦 ) ∈ dom vol )
38	24 37	jca	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( ( ◡ ( ℜ ∘ ( 𝐴 × { 𝐵 } ) ) “ 𝑦 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ ( 𝐴 × { 𝐵 } ) ) “ 𝑦 ) ∈ dom vol ) )
39	38	ralrimivw	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ∀ 𝑦 ∈ ran (,) ( ( ◡ ( ℜ ∘ ( 𝐴 × { 𝐵 } ) ) “ 𝑦 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ ( 𝐴 × { 𝐵 } ) ) “ 𝑦 ) ∈ dom vol ) )
40		ismbf1	⊢ ( ( 𝐴 × { 𝐵 } ) ∈ MblFn ↔ ( ( 𝐴 × { 𝐵 } ) ∈ ( ℂ ↑pm ℝ ) ∧ ∀ 𝑦 ∈ ran (,) ( ( ◡ ( ℜ ∘ ( 𝐴 × { 𝐵 } ) ) “ 𝑦 ) ∈ dom vol ∧ ( ◡ ( ℑ ∘ ( 𝐴 × { 𝐵 } ) ) “ 𝑦 ) ∈ dom vol ) ) )
41	10 39 40	sylanbrc	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℂ ) → ( 𝐴 × { 𝐵 } ) ∈ MblFn )