Step | Hyp | Ref
| Expression |
1 | | simp3 1063 |
. . . . 5
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → 𝐺 ∈ (𝐵–cn→ℂ)) |
2 | | cncff 22696 |
. . . . 5
⊢ (𝐺 ∈ (𝐵–cn→ℂ) → 𝐺:𝐵⟶ℂ) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → 𝐺:𝐵⟶ℂ) |
4 | | simp2 1062 |
. . . 4
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → 𝐹:𝐴⟶𝐵) |
5 | | fco 6058 |
. . . 4
⊢ ((𝐺:𝐵⟶ℂ ∧ 𝐹:𝐴⟶𝐵) → (𝐺 ∘ 𝐹):𝐴⟶ℂ) |
6 | 3, 4, 5 | syl2anc 693 |
. . 3
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → (𝐺 ∘ 𝐹):𝐴⟶ℂ) |
7 | | fdm 6051 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
8 | 4, 7 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → dom 𝐹 = 𝐴) |
9 | | mbfdm 23395 |
. . . . . 6
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
10 | 9 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → dom 𝐹 ∈ dom vol) |
11 | 8, 10 | eqeltrrd 2702 |
. . . 4
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → 𝐴 ∈ dom vol) |
12 | | mblss 23299 |
. . . 4
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
13 | 11, 12 | syl 17 |
. . 3
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → 𝐴 ⊆ ℝ) |
14 | | cnex 10017 |
. . . 4
⊢ ℂ
∈ V |
15 | | reex 10027 |
. . . 4
⊢ ℝ
∈ V |
16 | | elpm2r 7875 |
. . . 4
⊢
(((ℂ ∈ V ∧ ℝ ∈ V) ∧ ((𝐺 ∘ 𝐹):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ)) → (𝐺 ∘ 𝐹) ∈ (ℂ ↑pm
ℝ)) |
17 | 14, 15, 16 | mpanl12 718 |
. . 3
⊢ (((𝐺 ∘ 𝐹):𝐴⟶ℂ ∧ 𝐴 ⊆ ℝ) → (𝐺 ∘ 𝐹) ∈ (ℂ ↑pm
ℝ)) |
18 | 6, 13, 17 | syl2anc 693 |
. 2
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → (𝐺 ∘ 𝐹) ∈ (ℂ ↑pm
ℝ)) |
19 | | recncf 22705 |
. . . . . . . 8
⊢ ℜ
∈ (ℂ–cn→ℝ) |
20 | 19 | a1i 11 |
. . . . . . 7
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → ℜ ∈
(ℂ–cn→ℝ)) |
21 | 1, 20 | cncfco 22710 |
. . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → (ℜ ∘ 𝐺) ∈ (𝐵–cn→ℝ)) |
22 | 21 | adantr 481 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (ℜ ∘ 𝐺) ∈ (𝐵–cn→ℝ)) |
23 | | cnvco 5308 |
. . . . . . . . . 10
⊢ ◡(𝑔 ∘ 𝐹) = (◡𝐹 ∘ ◡𝑔) |
24 | 23 | imaeq1i 5463 |
. . . . . . . . 9
⊢ (◡(𝑔 ∘ 𝐹) “ 𝑥) = ((◡𝐹 ∘ ◡𝑔) “ 𝑥) |
25 | | imaco 5640 |
. . . . . . . . 9
⊢ ((◡𝐹 ∘ ◡𝑔) “ 𝑥) = (◡𝐹 “ (◡𝑔 “ 𝑥)) |
26 | 24, 25 | eqtri 2644 |
. . . . . . . 8
⊢ (◡(𝑔 ∘ 𝐹) “ 𝑥) = (◡𝐹 “ (◡𝑔 “ 𝑥)) |
27 | | simplll 798 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝐹 ∈ MblFn) |
28 | | simpllr 799 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝐹:𝐴⟶𝐵) |
29 | | cncfrss 22694 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (𝐵–cn→ℝ) → 𝐵 ⊆ ℂ) |
30 | 29 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝐵 ⊆ ℂ) |
31 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝑔 ∈ (𝐵–cn→ℝ)) |
32 | | ax-resscn 9993 |
. . . . . . . . . . . 12
⊢ ℝ
⊆ ℂ |
33 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
34 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ↾t 𝐵) =
((TopOpen‘ℂfld) ↾t 𝐵) |
35 | 33 | tgioo2 22606 |
. . . . . . . . . . . . 13
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
36 | 33, 34, 35 | cncfcn 22712 |
. . . . . . . . . . . 12
⊢ ((𝐵 ⊆ ℂ ∧ ℝ
⊆ ℂ) → (𝐵–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t 𝐵) Cn (topGen‘ran
(,)))) |
37 | 30, 32, 36 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → (𝐵–cn→ℝ) =
(((TopOpen‘ℂfld) ↾t 𝐵) Cn (topGen‘ran
(,)))) |
38 | 31, 37 | eleqtrd 2703 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝑔 ∈
(((TopOpen‘ℂfld) ↾t 𝐵) Cn (topGen‘ran
(,)))) |
39 | | retopbas 22564 |
. . . . . . . . . . . 12
⊢ ran (,)
∈ TopBases |
40 | | bastg 20770 |
. . . . . . . . . . . 12
⊢ (ran (,)
∈ TopBases → ran (,) ⊆ (topGen‘ran (,))) |
41 | 39, 40 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ran (,)
⊆ (topGen‘ran (,)) |
42 | | simplr 792 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝑥 ∈ ran (,)) |
43 | 41, 42 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → 𝑥 ∈ (topGen‘ran
(,))) |
44 | | cnima 21069 |
. . . . . . . . . 10
⊢ ((𝑔 ∈
(((TopOpen‘ℂfld) ↾t 𝐵) Cn (topGen‘ran (,))) ∧ 𝑥 ∈ (topGen‘ran (,)))
→ (◡𝑔 “ 𝑥) ∈
((TopOpen‘ℂfld) ↾t 𝐵)) |
45 | 38, 43, 44 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → (◡𝑔 “ 𝑥) ∈
((TopOpen‘ℂfld) ↾t 𝐵)) |
46 | 33, 34 | mbfimaopn2 23424 |
. . . . . . . . 9
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ ℂ) ∧ (◡𝑔 “ 𝑥) ∈
((TopOpen‘ℂfld) ↾t 𝐵)) → (◡𝐹 “ (◡𝑔 “ 𝑥)) ∈ dom vol) |
47 | 27, 28, 30, 45, 46 | syl31anc 1329 |
. . . . . . . 8
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → (◡𝐹 “ (◡𝑔 “ 𝑥)) ∈ dom vol) |
48 | 26, 47 | syl5eqel 2705 |
. . . . . . 7
⊢ ((((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) ∧ 𝑔 ∈ (𝐵–cn→ℝ)) → (◡(𝑔 ∘ 𝐹) “ 𝑥) ∈ dom vol) |
49 | 48 | ralrimiva 2966 |
. . . . . 6
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵) ∧ 𝑥 ∈ ran (,)) → ∀𝑔 ∈ (𝐵–cn→ℝ)(◡(𝑔 ∘ 𝐹) “ 𝑥) ∈ dom vol) |
50 | 49 | 3adantl3 1219 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → ∀𝑔 ∈ (𝐵–cn→ℝ)(◡(𝑔 ∘ 𝐹) “ 𝑥) ∈ dom vol) |
51 | | coeq1 5279 |
. . . . . . . . . 10
⊢ (𝑔 = (ℜ ∘ 𝐺) → (𝑔 ∘ 𝐹) = ((ℜ ∘ 𝐺) ∘ 𝐹)) |
52 | | coass 5654 |
. . . . . . . . . 10
⊢ ((ℜ
∘ 𝐺) ∘ 𝐹) = (ℜ ∘ (𝐺 ∘ 𝐹)) |
53 | 51, 52 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑔 = (ℜ ∘ 𝐺) → (𝑔 ∘ 𝐹) = (ℜ ∘ (𝐺 ∘ 𝐹))) |
54 | 53 | cnveqd 5298 |
. . . . . . . 8
⊢ (𝑔 = (ℜ ∘ 𝐺) → ◡(𝑔 ∘ 𝐹) = ◡(ℜ ∘ (𝐺 ∘ 𝐹))) |
55 | 54 | imaeq1d 5465 |
. . . . . . 7
⊢ (𝑔 = (ℜ ∘ 𝐺) → (◡(𝑔 ∘ 𝐹) “ 𝑥) = (◡(ℜ ∘ (𝐺 ∘ 𝐹)) “ 𝑥)) |
56 | 55 | eleq1d 2686 |
. . . . . 6
⊢ (𝑔 = (ℜ ∘ 𝐺) → ((◡(𝑔 ∘ 𝐹) “ 𝑥) ∈ dom vol ↔ (◡(ℜ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol)) |
57 | 56 | rspcv 3305 |
. . . . 5
⊢ ((ℜ
∘ 𝐺) ∈ (𝐵–cn→ℝ) → (∀𝑔 ∈ (𝐵–cn→ℝ)(◡(𝑔 ∘ 𝐹) “ 𝑥) ∈ dom vol → (◡(ℜ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol)) |
58 | 22, 50, 57 | sylc 65 |
. . . 4
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (◡(ℜ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol) |
59 | | imcncf 22706 |
. . . . . . . 8
⊢ ℑ
∈ (ℂ–cn→ℝ) |
60 | 59 | a1i 11 |
. . . . . . 7
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → ℑ ∈
(ℂ–cn→ℝ)) |
61 | 1, 60 | cncfco 22710 |
. . . . . 6
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → (ℑ ∘ 𝐺) ∈ (𝐵–cn→ℝ)) |
62 | 61 | adantr 481 |
. . . . 5
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (ℑ ∘
𝐺) ∈ (𝐵–cn→ℝ)) |
63 | | coeq1 5279 |
. . . . . . . . . 10
⊢ (𝑔 = (ℑ ∘ 𝐺) → (𝑔 ∘ 𝐹) = ((ℑ ∘ 𝐺) ∘ 𝐹)) |
64 | | coass 5654 |
. . . . . . . . . 10
⊢ ((ℑ
∘ 𝐺) ∘ 𝐹) = (ℑ ∘ (𝐺 ∘ 𝐹)) |
65 | 63, 64 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑔 = (ℑ ∘ 𝐺) → (𝑔 ∘ 𝐹) = (ℑ ∘ (𝐺 ∘ 𝐹))) |
66 | 65 | cnveqd 5298 |
. . . . . . . 8
⊢ (𝑔 = (ℑ ∘ 𝐺) → ◡(𝑔 ∘ 𝐹) = ◡(ℑ ∘ (𝐺 ∘ 𝐹))) |
67 | 66 | imaeq1d 5465 |
. . . . . . 7
⊢ (𝑔 = (ℑ ∘ 𝐺) → (◡(𝑔 ∘ 𝐹) “ 𝑥) = (◡(ℑ ∘ (𝐺 ∘ 𝐹)) “ 𝑥)) |
68 | 67 | eleq1d 2686 |
. . . . . 6
⊢ (𝑔 = (ℑ ∘ 𝐺) → ((◡(𝑔 ∘ 𝐹) “ 𝑥) ∈ dom vol ↔ (◡(ℑ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol)) |
69 | 68 | rspcv 3305 |
. . . . 5
⊢ ((ℑ
∘ 𝐺) ∈ (𝐵–cn→ℝ) → (∀𝑔 ∈ (𝐵–cn→ℝ)(◡(𝑔 ∘ 𝐹) “ 𝑥) ∈ dom vol → (◡(ℑ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol)) |
70 | 62, 50, 69 | sylc 65 |
. . . 4
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → (◡(ℑ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol) |
71 | 58, 70 | jca 554 |
. . 3
⊢ (((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) ∧ 𝑥 ∈ ran (,)) → ((◡(ℜ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol)) |
72 | 71 | ralrimiva 2966 |
. 2
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → ∀𝑥 ∈ ran (,)((◡(ℜ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol)) |
73 | | ismbf1 23393 |
. 2
⊢ ((𝐺 ∘ 𝐹) ∈ MblFn ↔ ((𝐺 ∘ 𝐹) ∈ (ℂ ↑pm
ℝ) ∧ ∀𝑥
∈ ran (,)((◡(ℜ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol ∧ (◡(ℑ ∘ (𝐺 ∘ 𝐹)) “ 𝑥) ∈ dom vol))) |
74 | 18, 72, 73 | sylanbrc 698 |
1
⊢ ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺 ∈ (𝐵–cn→ℂ)) → (𝐺 ∘ 𝐹) ∈ MblFn) |