| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp3 1138 | . . . . 5
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → 𝐺 ∈ (𝐵–cn→ℂ)) | 
| 2 |  | cncff 24920 | . . . . 5
⊢ (𝐺 ∈ (𝐵–cn→ℂ) → 𝐺:𝐵⟶ℂ) | 
| 3 | 1, 2 | syl 17 | . . . 4
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → 𝐺:𝐵⟶ℂ) | 
| 4 |  | simp2 1137 | . . . 4
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → 𝐹:𝐴⟶𝐵) | 
| 5 |  | fco 6759 | . . . 4
⊢ ((𝐺:𝐵⟶ℂ ∧ 𝐹:𝐴⟶𝐵) → (𝐺 ∘ 𝐹):𝐴⟶ℂ) | 
| 6 | 3, 4, 5 | syl2anc 584 | . . 3
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → (𝐺 ∘ 𝐹):𝐴⟶ℂ) | 
| 7 | 4 | fdmd 6745 | . . . . 5
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → dom 𝐹 = 𝐴) | 
| 8 |  | mbfdm 25662 | . . . . . 6
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) | 
| 9 | 8 | 3ad2ant1 1133 | . . . . 5
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → dom 𝐹 ∈ dom vol) | 
| 10 | 7, 9 | eqeltrrd 2841 | . . . 4
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → 𝐴 ∈ dom vol) | 
| 11 |  | mblss 25567 | . . . 4
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) | 
| 12 | 10, 11 | syl 17 | . . 3
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → 𝐴 ⊆ ℝ) | 
| 13 |  | cnex 11237 | . . . 4
⊢ ℂ
∈ V | 
| 14 |  | reex 11247 | . . . 4
⊢ ℝ
∈ V | 
| 15 |  | elpm2r 8886 | . . . 4
⊢
(((ℂ ∈ V ∧ ℝ ∈ V) ∧ ((𝐺 ∘ 𝐹):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → (𝐺 ∘ 𝐹) ∈ (ℂ ↑pm
ℝ)) | 
| 16 | 13, 14, 15 | mpanl12 702 | . . 3
⊢ (((𝐺 ∘ 𝐹):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → (𝐺 ∘ 𝐹) ∈ (ℂ ↑pm
ℝ)) | 
| 17 | 6, 12, 16 | syl2anc 584 | . 2
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → (𝐺 ∘ 𝐹) ∈ (ℂ ↑pm
ℝ)) | 
| 18 |  | coeq1 5867 | . . . . . . . . 9
⊢ (𝑔 = (ℜ ∘ 𝐺) → (𝑔 ∘ 𝐹) = ((ℜ ∘ 𝐺) ∘ 𝐹)) | 
| 19 |  | coass 6284 | . . . . . . . . 9
⊢ ((ℜ
∘ 𝐺) ∘ 𝐹) = (ℜ ∘ (𝐺 ∘ 𝐹)) | 
| 20 | 18, 19 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑔 = (ℜ ∘ 𝐺) → (𝑔 ∘ 𝐹) = (ℜ ∘ (𝐺 ∘ 𝐹))) | 
| 21 | 20 | cnveqd 5885 | . . . . . . 7
⊢ (𝑔 = (ℜ ∘ 𝐺) → ◡(𝑔 ∘ 𝐹) = ◡(ℜ ∘ (𝐺 ∘ 𝐹))) | 
| 22 | 21 | imaeq1d 6076 | . . . . . 6
⊢ (𝑔 = (ℜ ∘ 𝐺) → (◡(𝑔 ∘ 𝐹) “ 𝑥) = (◡(ℜ ∘ (𝐺 ∘ 𝐹)) “ 𝑥)) | 
| 23 | 22 | eleq1d 2825 | . . . . 5
⊢ (𝑔 = (ℜ ∘ 𝐺) → ((◡(𝑔 ∘ 𝐹) “ 𝑥) ∈ dom vol ↔ (◡(ℜ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol)) | 
| 24 |  | cnvco 5895 | . . . . . . . . . 10
⊢ ◡(𝑔 ∘ 𝐹) = (◡𝐹 ∘ ◡𝑔) | 
| 25 | 24 | imaeq1i 6074 | . . . . . . . . 9
⊢ (◡(𝑔 ∘ 𝐹) “ 𝑥) = ((◡𝐹 ∘ ◡𝑔) “ 𝑥) | 
| 26 |  | imaco 6270 | . . . . . . . . 9
⊢ ((◡𝐹 ∘ ◡𝑔) “ 𝑥) = (◡𝐹 “ (◡𝑔 “ 𝑥)) | 
| 27 | 25, 26 | eqtri 2764 | . . . . . . . 8
⊢ (◡(𝑔 ∘ 𝐹) “ 𝑥) = (◡𝐹 “ (◡𝑔 “ 𝑥)) | 
| 28 |  | simplll 774 | . . . . . . . . 9
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝐹 ∈ MblFn) | 
| 29 |  | simpllr 775 | . . . . . . . . 9
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝐹:𝐴⟶𝐵) | 
| 30 |  | cncfrss 24918 | . . . . . . . . . 10
⊢ (𝑔 ∈ (𝐵–cn→ℝ) → 𝐵 ⊆ ℂ) | 
| 31 | 30 | adantl 481 | . . . . . . . . 9
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝐵 ⊆ ℂ) | 
| 32 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝑔 ∈ (𝐵–cn→ℝ)) | 
| 33 |  | ax-resscn 11213 | . . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ | 
| 34 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 35 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ↾t 𝐵) =
((TopOpen‘ℂfld) ↾t 𝐵) | 
| 36 |  | tgioo4 24827 | . . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) | 
| 37 | 34, 35, 36 | cncfcn 24937 | . . . . . . . . . . . 12
⊢ ((𝐵 ⊆ ℂ ∧ ℝ
⊆ ℂ) → (𝐵–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t 𝐵) Cn (topGen‘ran
(,)))) | 
| 38 | 31, 33, 37 | sylancl 586 | . . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → (𝐵–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t 𝐵) Cn (topGen‘ran
(,)))) | 
| 39 | 32, 38 | eleqtrd 2842 | . . . . . . . . . 10
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝑔 ∈
(((TopOpen‘ℂfld) ↾t 𝐵) Cn (topGen‘ran
(,)))) | 
| 40 |  | retopbas 24782 | . . . . . . . . . . . 12
⊢ ran (,)
∈ TopBases | 
| 41 |  | bastg 22974 | . . . . . . . . . . . 12
⊢ (ran (,)
∈ TopBases → ran (,) ⊆ (topGen‘ran (,))) | 
| 42 | 40, 41 | ax-mp 5 | . . . . . . . . . . 11
⊢ ran (,)
⊆ (topGen‘ran (,)) | 
| 43 |  | simplr 768 | . . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝑥 ∈ ran (,)) | 
| 44 | 42, 43 | sselid 3980 | . . . . . . . . . 10
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝑥 ∈ (topGen‘ran
(,))) | 
| 45 |  | cnima 23274 | . . . . . . . . . 10
⊢ ((𝑔 ∈
(((TopOpen‘ℂfld) ↾t 𝐵) Cn (topGen‘ran (,))) ∧ 𝑥 ∈ (topGen‘ran (,)))
→ (◡𝑔 “ 𝑥) ∈
((TopOpen‘ℂfld) ↾t 𝐵)) | 
| 46 | 39, 44, 45 | syl2anc 584 | . . . . . . . . 9
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → (◡𝑔 “ 𝑥) ∈
((TopOpen‘ℂfld) ↾t 𝐵)) | 
| 47 | 34, 35 | mbfimaopn2 25693 | . . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ ℂ) ∧ (◡𝑔 “ 𝑥) ∈
((TopOpen‘ℂfld) ↾t 𝐵)) → (◡𝐹 “ (◡𝑔 “ 𝑥)) ∈ dom vol) | 
| 48 | 28, 29, 31, 46, 47 | syl31anc 1374 | . . . . . . . 8
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → (◡𝐹 “ (◡𝑔 “ 𝑥)) ∈ dom vol) | 
| 49 | 27, 48 | eqeltrid 2844 | . . . . . . 7
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → (◡(𝑔 ∘ 𝐹) “ 𝑥) ∈ dom vol) | 
| 50 | 49 | ralrimiva 3145 | . . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) → ∀𝑔 ∈ (𝐵–cn→ℝ)(◡(𝑔 ∘ 𝐹) “ 𝑥) ∈ dom vol) | 
| 51 | 50 | 3adantl3 1168 | . . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → ∀𝑔 ∈ (𝐵–cn→ℝ)(◡(𝑔 ∘ 𝐹) “ 𝑥) ∈ dom vol) | 
| 52 |  | recncf 24929 | . . . . . . . 8
⊢ ℜ
∈ (ℂ–cn→ℝ) | 
| 53 | 52 | a1i 11 | . . . . . . 7
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → ℜ ∈
(ℂ–cn→ℝ)) | 
| 54 | 1, 53 | cncfco 24934 | . . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → (ℜ ∘ 𝐺) ∈ (𝐵–cn→ℝ)) | 
| 55 | 54 | adantr 480 | . . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (ℜ ∘ 𝐺) ∈ (𝐵–cn→ℝ)) | 
| 56 | 23, 51, 55 | rspcdva 3622 | . . . 4
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (◡(ℜ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol) | 
| 57 |  | coeq1 5867 | . . . . . . . . 9
⊢ (𝑔 = (ℑ ∘ 𝐺) → (𝑔 ∘ 𝐹) = ((ℑ ∘ 𝐺) ∘ 𝐹)) | 
| 58 |  | coass 6284 | . . . . . . . . 9
⊢ ((ℑ
∘ 𝐺) ∘ 𝐹) = (ℑ ∘ (𝐺 ∘ 𝐹)) | 
| 59 | 57, 58 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑔 = (ℑ ∘ 𝐺) → (𝑔 ∘ 𝐹) = (ℑ ∘ (𝐺 ∘ 𝐹))) | 
| 60 | 59 | cnveqd 5885 | . . . . . . 7
⊢ (𝑔 = (ℑ ∘ 𝐺) → ◡(𝑔 ∘ 𝐹) = ◡(ℑ ∘ (𝐺 ∘ 𝐹))) | 
| 61 | 60 | imaeq1d 6076 | . . . . . 6
⊢ (𝑔 = (ℑ ∘ 𝐺) → (◡(𝑔 ∘ 𝐹) “ 𝑥) = (◡(ℑ ∘ (𝐺 ∘ 𝐹)) “ 𝑥)) | 
| 62 | 61 | eleq1d 2825 | . . . . 5
⊢ (𝑔 = (ℑ ∘ 𝐺) → ((◡(𝑔 ∘ 𝐹) “ 𝑥) ∈ dom vol ↔ (◡(ℑ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol)) | 
| 63 |  | imcncf 24930 | . . . . . . . 8
⊢ ℑ
∈ (ℂ–cn→ℝ) | 
| 64 | 63 | a1i 11 | . . . . . . 7
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → ℑ ∈
(ℂ–cn→ℝ)) | 
| 65 | 1, 64 | cncfco 24934 | . . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → (ℑ ∘ 𝐺) ∈ (𝐵–cn→ℝ)) | 
| 66 | 65 | adantr 480 | . . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (ℑ ∘
𝐺) ∈ (𝐵–cn→ℝ)) | 
| 67 | 62, 51, 66 | rspcdva 3622 | . . . 4
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (◡(ℑ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol) | 
| 68 | 56, 67 | jca 511 | . . 3
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → ((◡(ℜ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol)) | 
| 69 | 68 | ralrimiva 3145 | . 2
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → ∀𝑥 ∈ ran (,)((◡(ℜ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol)) | 
| 70 |  | ismbf1 25660 | . 2
⊢ ((𝐺 ∘ 𝐹) ∈ MblFn ↔ ((𝐺 ∘ 𝐹) ∈ (ℂ ↑pm
ℝ) ∧ ∀𝑥
∈ ran (,)((◡(ℜ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol))) | 
| 71 | 17, 69, 70 | sylanbrc 583 | 1
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → (𝐺 ∘ 𝐹) ∈ MblFn) |