| Step | Hyp | Ref
| Expression |
| 1 | | cncff 24919 |
. . 3
⊢ (𝐹 ∈ (𝐴–cn→ℂ) → 𝐹:𝐴⟶ℂ) |
| 2 | | mblss 25566 |
. . 3
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
| 3 | | cnex 11236 |
. . . 4
⊢ ℂ
∈ V |
| 4 | | reex 11246 |
. . . 4
⊢ ℝ
∈ V |
| 5 | | elpm2r 8885 |
. . . 4
⊢
(((ℂ ∈ V ∧ ℝ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
| 6 | 3, 4, 5 | mpanl12 702 |
. . 3
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
| 7 | 1, 2, 6 | syl2anr 597 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) → 𝐹 ∈ (ℂ ↑pm
ℝ)) |
| 8 | | simpll 767 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → 𝐴 ∈ dom vol) |
| 9 | | simplr 769 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → 𝐹 ∈ (𝐴–cn→ℂ)) |
| 10 | | recncf 24928 |
. . . . . . . . 9
⊢ ℜ
∈ (ℂ–cn→ℝ) |
| 11 | 10 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → ℜ ∈
(ℂ–cn→ℝ)) |
| 12 | 9, 11 | cncfco 24933 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (ℜ ∘ 𝐹) ∈ (𝐴–cn→ℝ)) |
| 13 | 2 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → 𝐴 ⊆ ℝ) |
| 14 | | ax-resscn 11212 |
. . . . . . . . . 10
⊢ ℝ
⊆ ℂ |
| 15 | 13, 14 | sstrdi 3996 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → 𝐴 ⊆ ℂ) |
| 16 | | eqid 2737 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 17 | | eqid 2737 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t 𝐴) =
((TopOpen‘ℂfld) ↾t 𝐴) |
| 18 | | tgioo4 24826 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 19 | 16, 17, 18 | cncfcn 24936 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℂ ∧ ℝ
⊆ ℂ) → (𝐴–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t 𝐴) Cn (topGen‘ran
(,)))) |
| 20 | 15, 14, 19 | sylancl 586 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (𝐴–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t 𝐴) Cn (topGen‘ran
(,)))) |
| 21 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
| 22 | 16, 21 | rerest 24825 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ℝ →
((TopOpen‘ℂfld) ↾t 𝐴) = ((topGen‘ran (,))
↾t 𝐴)) |
| 23 | 13, 22 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) →
((TopOpen‘ℂfld) ↾t 𝐴) = ((topGen‘ran (,))
↾t 𝐴)) |
| 24 | 23 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) →
(((TopOpen‘ℂfld) ↾t 𝐴) Cn (topGen‘ran (,))) =
(((topGen‘ran (,)) ↾t 𝐴) Cn (topGen‘ran
(,)))) |
| 25 | 20, 24 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (𝐴–cn→ℝ) = (((topGen‘ran (,))
↾t 𝐴) Cn
(topGen‘ran (,)))) |
| 26 | 12, 25 | eleqtrd 2843 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (ℜ ∘ 𝐹) ∈ (((topGen‘ran
(,)) ↾t 𝐴)
Cn (topGen‘ran (,)))) |
| 27 | | retopbas 24781 |
. . . . . . . 8
⊢ ran (,)
∈ TopBases |
| 28 | | bastg 22973 |
. . . . . . . 8
⊢ (ran (,)
∈ TopBases → ran (,) ⊆ (topGen‘ran (,))) |
| 29 | 27, 28 | ax-mp 5 |
. . . . . . 7
⊢ ran (,)
⊆ (topGen‘ran (,)) |
| 30 | | simpr 484 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → 𝑥 ∈ ran (,)) |
| 31 | 29, 30 | sselid 3981 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → 𝑥 ∈ (topGen‘ran
(,))) |
| 32 | | cnima 23273 |
. . . . . 6
⊢ (((ℜ
∘ 𝐹) ∈
(((topGen‘ran (,)) ↾t 𝐴) Cn (topGen‘ran (,))) ∧ 𝑥 ∈ (topGen‘ran (,)))
→ (◡(ℜ ∘ 𝐹) “ 𝑥) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
| 33 | 26, 31, 32 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (◡(ℜ ∘ 𝐹) “ 𝑥) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
| 34 | | eqid 2737 |
. . . . . 6
⊢
((topGen‘ran (,)) ↾t 𝐴) = ((topGen‘ran (,))
↾t 𝐴) |
| 35 | 34 | subopnmbl 25639 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ (◡(ℜ ∘ 𝐹) “ 𝑥) ∈ ((topGen‘ran (,))
↾t 𝐴))
→ (◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol) |
| 36 | 8, 33, 35 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol) |
| 37 | | imcncf 24929 |
. . . . . . . . 9
⊢ ℑ
∈ (ℂ–cn→ℝ) |
| 38 | 37 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → ℑ ∈
(ℂ–cn→ℝ)) |
| 39 | 9, 38 | cncfco 24933 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (ℑ ∘
𝐹) ∈ (𝐴–cn→ℝ)) |
| 40 | 39, 25 | eleqtrd 2843 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (ℑ ∘
𝐹) ∈
(((topGen‘ran (,)) ↾t 𝐴) Cn (topGen‘ran
(,)))) |
| 41 | | cnima 23273 |
. . . . . 6
⊢
(((ℑ ∘ 𝐹) ∈ (((topGen‘ran (,))
↾t 𝐴) Cn
(topGen‘ran (,))) ∧ 𝑥 ∈ (topGen‘ran (,))) → (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
| 42 | 40, 31, 41 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ ((topGen‘ran (,))
↾t 𝐴)) |
| 43 | 34 | subopnmbl 25639 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ ((topGen‘ran (,))
↾t 𝐴))
→ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol) |
| 44 | 8, 42, 43 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol) |
| 45 | 36, 44 | jca 511 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → ((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)) |
| 46 | 45 | ralrimiva 3146 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) → ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol)) |
| 47 | | ismbf1 25659 |
. 2
⊢ (𝐹 ∈ MblFn ↔ (𝐹 ∈ (ℂ
↑pm ℝ) ∧ ∀𝑥 ∈ ran (,)((◡(ℜ ∘ 𝐹) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ 𝐹) “ 𝑥) ∈ dom vol))) |
| 48 | 7, 46, 47 | sylanbrc 583 |
1
⊢ ((𝐴 ∈ dom vol ∧ 𝐹 ∈ (𝐴–cn→ℂ)) → 𝐹 ∈ MblFn) |