This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )