Step | Hyp | Ref
| Expression |
1 | | sibfof.1 |
. . . . . . . 8
⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶) |
2 | | sibfof.0 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ TopSp) |
3 | | sitgval.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝑊) |
4 | | sitgval.j |
. . . . . . . . . . . 12
⊢ 𝐽 = (TopOpen‘𝑊) |
5 | 3, 4 | tpsuni 20740 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ TopSp → 𝐵 = ∪
𝐽) |
6 | 2, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 = ∪ 𝐽) |
7 | 6 | sqxpeqd 5141 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 × 𝐵) = (∪ 𝐽 × ∪ 𝐽)) |
8 | 7 | feq2d 6031 |
. . . . . . . 8
⊢ (𝜑 → ( + :(𝐵 × 𝐵)⟶𝐶 ↔ + :(∪ 𝐽
× ∪ 𝐽)⟶𝐶)) |
9 | 1, 8 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → + :(∪ 𝐽
× ∪ 𝐽)⟶𝐶) |
10 | 9 | fovrnda 6805 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ ∪ 𝐽 ∧ 𝑥 ∈ ∪ 𝐽)) → (𝑧 + 𝑥) ∈ 𝐶) |
11 | | sitgval.s |
. . . . . . 7
⊢ 𝑆 = (sigaGen‘𝐽) |
12 | | sitgval.0 |
. . . . . . 7
⊢ 0 =
(0g‘𝑊) |
13 | | sitgval.x |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑊) |
14 | | sitgval.h |
. . . . . . 7
⊢ 𝐻 =
(ℝHom‘(Scalar‘𝑊)) |
15 | | sitgval.1 |
. . . . . . 7
⊢ (𝜑 → 𝑊 ∈ 𝑉) |
16 | | sitgval.2 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ∪ ran
measures) |
17 | | sibfmbl.1 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) |
18 | 3, 4, 11, 12, 13, 14, 15, 16, 17 | sibff 30398 |
. . . . . 6
⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶∪ 𝐽) |
19 | | sibfof.2 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀)) |
20 | 3, 4, 11, 12, 13, 14, 15, 16, 19 | sibff 30398 |
. . . . . 6
⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶∪ 𝐽) |
21 | | dmexg 7097 |
. . . . . . 7
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ V) |
22 | | uniexg 6955 |
. . . . . . 7
⊢ (dom
𝑀 ∈ V → ∪ dom 𝑀 ∈ V) |
23 | 16, 21, 22 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ∪ dom 𝑀 ∈ V) |
24 | | inidm 3822 |
. . . . . 6
⊢ (∪ dom 𝑀 ∩ ∪ dom
𝑀) = ∪ dom 𝑀 |
25 | 10, 18, 20, 23, 23, 24 | off 6912 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):∪
dom 𝑀⟶𝐶) |
26 | | sibfof.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ TopSp) |
27 | | sibfof.c |
. . . . . . . . 9
⊢ 𝐶 = (Base‘𝐾) |
28 | | eqid 2622 |
. . . . . . . . 9
⊢
(TopOpen‘𝐾) =
(TopOpen‘𝐾) |
29 | 27, 28 | tpsuni 20740 |
. . . . . . . 8
⊢ (𝐾 ∈ TopSp → 𝐶 = ∪
(TopOpen‘𝐾)) |
30 | 26, 29 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐶 = ∪
(TopOpen‘𝐾)) |
31 | | fvex 6201 |
. . . . . . . 8
⊢
(TopOpen‘𝐾)
∈ V |
32 | | unisg 30206 |
. . . . . . . 8
⊢
((TopOpen‘𝐾)
∈ V → ∪
(sigaGen‘(TopOpen‘𝐾)) = ∪
(TopOpen‘𝐾)) |
33 | 31, 32 | ax-mp 5 |
. . . . . . 7
⊢ ∪ (sigaGen‘(TopOpen‘𝐾)) = ∪
(TopOpen‘𝐾) |
34 | 30, 33 | syl6eqr 2674 |
. . . . . 6
⊢ (𝜑 → 𝐶 = ∪
(sigaGen‘(TopOpen‘𝐾))) |
35 | 34 | feq3d 6032 |
. . . . 5
⊢ (𝜑 → ((𝐹 ∘𝑓 + 𝐺):∪
dom 𝑀⟶𝐶 ↔ (𝐹 ∘𝑓 + 𝐺):∪
dom 𝑀⟶∪ (sigaGen‘(TopOpen‘𝐾)))) |
36 | 25, 35 | mpbid 222 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):∪
dom 𝑀⟶∪ (sigaGen‘(TopOpen‘𝐾))) |
37 | 31 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (TopOpen‘𝐾) ∈ V) |
38 | 37 | sgsiga 30205 |
. . . . . 6
⊢ (𝜑 →
(sigaGen‘(TopOpen‘𝐾)) ∈ ∪ ran
sigAlgebra) |
39 | | uniexg 6955 |
. . . . . 6
⊢
((sigaGen‘(TopOpen‘𝐾)) ∈ ∪ ran
sigAlgebra → ∪
(sigaGen‘(TopOpen‘𝐾)) ∈ V) |
40 | 38, 39 | syl 17 |
. . . . 5
⊢ (𝜑 → ∪ (sigaGen‘(TopOpen‘𝐾)) ∈ V) |
41 | 40, 23 | elmapd 7871 |
. . . 4
⊢ (𝜑 → ((𝐹 ∘𝑓 + 𝐺) ∈ (∪ (sigaGen‘(TopOpen‘𝐾)) ↑𝑚 ∪ dom 𝑀) ↔ (𝐹 ∘𝑓 + 𝐺):∪
dom 𝑀⟶∪ (sigaGen‘(TopOpen‘𝐾)))) |
42 | 36, 41 | mpbird 247 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ (∪ (sigaGen‘(TopOpen‘𝐾)) ↑𝑚 ∪ dom 𝑀)) |
43 | | inundif 4046 |
. . . . . . 7
⊢ ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ∪ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) = 𝑏 |
44 | 43 | imaeq2i 5464 |
. . . . . 6
⊢ (◡(𝐹 ∘𝑓 + 𝐺) “ ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ∪ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))) = (◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) |
45 | | ffun 6048 |
. . . . . . . 8
⊢ ((𝐹 ∘𝑓
+ 𝐺):∪
dom 𝑀⟶𝐶 → Fun (𝐹 ∘𝑓 + 𝐺)) |
46 | | unpreima 6341 |
. . . . . . . 8
⊢ (Fun
(𝐹
∘𝑓 + 𝐺) → (◡(𝐹 ∘𝑓 + 𝐺) “ ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ∪ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))) = ((◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∪ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))))) |
47 | 25, 45, 46 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (◡(𝐹 ∘𝑓 + 𝐺) “ ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ∪ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))) = ((◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∪ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))))) |
48 | 47 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → (◡(𝐹 ∘𝑓 + 𝐺) “ ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ∪ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))) = ((◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∪ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))))) |
49 | 44, 48 | syl5eqr 2670 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → (◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) = ((◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∪ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))))) |
50 | | dmmeas 30264 |
. . . . . . . 8
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
51 | 16, 50 | syl 17 |
. . . . . . 7
⊢ (𝜑 → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
52 | 51 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
53 | | imaiun 6503 |
. . . . . . . 8
⊢ (◡(𝐹 ∘𝑓 + 𝐺) “ ∪ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)){𝑧}) = ∪
𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) |
54 | | iunid 4575 |
. . . . . . . . 9
⊢ ∪ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)){𝑧} = (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) |
55 | 54 | imaeq2i 5464 |
. . . . . . . 8
⊢ (◡(𝐹 ∘𝑓 + 𝐺) “ ∪ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)){𝑧}) = (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) |
56 | 53, 55 | eqtr3i 2646 |
. . . . . . 7
⊢ ∪ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) = (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) |
57 | | inss2 3834 |
. . . . . . . . . 10
⊢ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ⊆ ran (𝐹 ∘𝑓
+ 𝐺) |
58 | 6 | feq3d 6032 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹:∪ dom 𝑀⟶𝐵 ↔ 𝐹:∪ dom 𝑀⟶∪ 𝐽)) |
59 | 18, 58 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶𝐵) |
60 | 6 | feq3d 6032 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺:∪ dom 𝑀⟶𝐵 ↔ 𝐺:∪ dom 𝑀⟶∪ 𝐽)) |
61 | 20, 60 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶𝐵) |
62 | | ffn 6045 |
. . . . . . . . . . . . . . 15
⊢ ( + :(𝐵 × 𝐵)⟶𝐶 → + Fn (𝐵 × 𝐵)) |
63 | 1, 62 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → + Fn (𝐵 × 𝐵)) |
64 | 59, 61, 23, 63 | ofpreima2 29466 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) = ∪
𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
65 | 64 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) = ∪
𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
66 | 51 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
67 | 51 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
68 | | simpll 790 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝜑) |
69 | | inss1 3833 |
. . . . . . . . . . . . . . . . . 18
⊢ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (◡ + “ {𝑧}) |
70 | | cnvimass 5485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (◡ + “ {𝑧}) ⊆ dom + |
71 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ( + :(𝐵 × 𝐵)⟶𝐶 → dom + = (𝐵 × 𝐵)) |
72 | 1, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → dom + = (𝐵 × 𝐵)) |
73 | 70, 72 | syl5sseq 3653 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (◡ + “ {𝑧}) ⊆ (𝐵 × 𝐵)) |
74 | 73 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → (◡ + “ {𝑧}) ⊆ (𝐵 × 𝐵)) |
75 | 69, 74 | syl5ss 3614 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (𝐵 × 𝐵)) |
76 | 75 | sselda 3603 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ (𝐵 × 𝐵)) |
77 | 51 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
78 | | sibfof.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐽 ∈ Fre) |
79 | 78 | sgsiga 30205 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (sigaGen‘𝐽) ∈ ∪ ran sigAlgebra) |
80 | 11, 79 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑆 ∈ ∪ ran
sigAlgebra) |
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → 𝑆 ∈ ∪ ran
sigAlgebra) |
82 | 3, 4, 11, 12, 13, 14, 15, 16, 17 | sibfmbl 30397 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ∈ (dom 𝑀MblFnM𝑆)) |
83 | 82 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → 𝐹 ∈ (dom 𝑀MblFnM𝑆)) |
84 | 4 | tpstop 20741 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑊 ∈ TopSp → 𝐽 ∈ Top) |
85 | | cldssbrsiga 30250 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐽 ∈ Top →
(Clsd‘𝐽) ⊆
(sigaGen‘𝐽)) |
86 | 2, 84, 85 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (Clsd‘𝐽) ⊆ (sigaGen‘𝐽)) |
87 | 86 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (Clsd‘𝐽) ⊆ (sigaGen‘𝐽)) |
88 | 78 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → 𝐽 ∈ Fre) |
89 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 ∈ (𝐵 × 𝐵) → (1st ‘𝑝) ∈ 𝐵) |
90 | 89 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (1st ‘𝑝) ∈ 𝐵) |
91 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → 𝐵 = ∪ 𝐽) |
92 | 90, 91 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (1st ‘𝑝) ∈ ∪ 𝐽) |
93 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∪ 𝐽 =
∪ 𝐽 |
94 | 93 | t1sncld 21130 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ Fre ∧
(1st ‘𝑝)
∈ ∪ 𝐽) → {(1st ‘𝑝)} ∈ (Clsd‘𝐽)) |
95 | 88, 92, 94 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → {(1st ‘𝑝)} ∈ (Clsd‘𝐽)) |
96 | 87, 95 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → {(1st ‘𝑝)} ∈ (sigaGen‘𝐽)) |
97 | 96, 11 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → {(1st ‘𝑝)} ∈ 𝑆) |
98 | 77, 81, 83, 97 | mbfmcnvima 30319 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (◡𝐹 “ {(1st ‘𝑝)}) ∈ dom 𝑀) |
99 | 68, 76, 98 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (◡𝐹 “ {(1st ‘𝑝)}) ∈ dom 𝑀) |
100 | 3, 4, 11, 12, 13, 14, 15, 16, 19 | sibfmbl 30397 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺 ∈ (dom 𝑀MblFnM𝑆)) |
101 | 100 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → 𝐺 ∈ (dom 𝑀MblFnM𝑆)) |
102 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 ∈ (𝐵 × 𝐵) → (2nd ‘𝑝) ∈ 𝐵) |
103 | 102 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (2nd ‘𝑝) ∈ 𝐵) |
104 | 103, 91 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (2nd ‘𝑝) ∈ ∪ 𝐽) |
105 | 93 | t1sncld 21130 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ Fre ∧
(2nd ‘𝑝)
∈ ∪ 𝐽) → {(2nd ‘𝑝)} ∈ (Clsd‘𝐽)) |
106 | 88, 104, 105 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → {(2nd ‘𝑝)} ∈ (Clsd‘𝐽)) |
107 | 87, 106 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → {(2nd ‘𝑝)} ∈ (sigaGen‘𝐽)) |
108 | 107, 11 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → {(2nd ‘𝑝)} ∈ 𝑆) |
109 | 77, 81, 101, 108 | mbfmcnvima 30319 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (◡𝐺 “ {(2nd ‘𝑝)}) ∈ dom 𝑀) |
110 | 68, 76, 109 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (◡𝐺 “ {(2nd ‘𝑝)}) ∈ dom 𝑀) |
111 | | inelsiga 30198 |
. . . . . . . . . . . . . . 15
⊢ ((dom
𝑀 ∈ ∪ ran sigAlgebra ∧ (◡𝐹 “ {(1st ‘𝑝)}) ∈ dom 𝑀 ∧ (◡𝐺 “ {(2nd ‘𝑝)}) ∈ dom 𝑀) → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀) |
112 | 67, 99, 110, 111 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀) |
113 | 112 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → ∀𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀) |
114 | 3, 4, 11, 12, 13, 14, 15, 16, 17 | sibfrn 30399 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
115 | 3, 4, 11, 12, 13, 14, 15, 16, 19 | sibfrn 30399 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ran 𝐺 ∈ Fin) |
116 | | xpfi 8231 |
. . . . . . . . . . . . . . . . 17
⊢ ((ran
𝐹 ∈ Fin ∧ ran
𝐺 ∈ Fin) → (ran
𝐹 × ran 𝐺) ∈ Fin) |
117 | 114, 115,
116 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin) |
118 | | inss2 3834 |
. . . . . . . . . . . . . . . 16
⊢ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (ran 𝐹 × ran 𝐺) |
119 | | ssdomg 8001 |
. . . . . . . . . . . . . . . 16
⊢ ((ran
𝐹 × ran 𝐺) ∈ Fin → (((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (ran 𝐹 × ran 𝐺) → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ (ran 𝐹 × ran 𝐺))) |
120 | 117, 118,
119 | mpisyl 21 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ (ran 𝐹 × ran 𝐺)) |
121 | | isfinite 8549 |
. . . . . . . . . . . . . . . . 17
⊢ ((ran
𝐹 × ran 𝐺) ∈ Fin ↔ (ran 𝐹 × ran 𝐺) ≺ ω) |
122 | 121 | biimpi 206 |
. . . . . . . . . . . . . . . 16
⊢ ((ran
𝐹 × ran 𝐺) ∈ Fin → (ran 𝐹 × ran 𝐺) ≺ ω) |
123 | | sdomdom 7983 |
. . . . . . . . . . . . . . . 16
⊢ ((ran
𝐹 × ran 𝐺) ≺ ω → (ran
𝐹 × ran 𝐺) ≼
ω) |
124 | 117, 122,
123 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ≼ ω) |
125 | | domtr 8009 |
. . . . . . . . . . . . . . 15
⊢ ((((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ (ran 𝐹 × ran 𝐺) ∧ (ran 𝐹 × ran 𝐺) ≼ ω) → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ ω) |
126 | 120, 124,
125 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ ω) |
127 | 126 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ ω) |
128 | | nfcv 2764 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑝((◡
+ “
{𝑧}) ∩ (ran 𝐹 × ran 𝐺)) |
129 | 128 | sigaclcuni 30181 |
. . . . . . . . . . . . 13
⊢ ((dom
𝑀 ∈ ∪ ran sigAlgebra ∧ ∀𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀 ∧ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ ω) → ∪ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀) |
130 | 66, 113, 127, 129 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → ∪ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀) |
131 | 65, 130 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀) |
132 | 131 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀) |
133 | | ssralv 3666 |
. . . . . . . . . 10
⊢ ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ⊆ ran (𝐹 ∘𝑓
+ 𝐺) → (∀𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀 → ∀𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀)) |
134 | 57, 132, 133 | mpsyl 68 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀) |
135 | 134 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → ∀𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀) |
136 | | ffun 6048 |
. . . . . . . . . . . . . 14
⊢ ( + :(𝐵 × 𝐵)⟶𝐶 → Fun + ) |
137 | 1, 136 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Fun + ) |
138 | | imafi 8259 |
. . . . . . . . . . . . 13
⊢ ((Fun
+ ∧
(ran 𝐹 × ran 𝐺) ∈ Fin) → ( + “ (ran
𝐹 × ran 𝐺)) ∈ Fin) |
139 | 137, 117,
138 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) ∈ Fin) |
140 | 18, 20, 9, 23 | ofrn2 29442 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆ ( + “ (ran 𝐹 × ran 𝐺))) |
141 | | ssfi 8180 |
. . . . . . . . . . . 12
⊢ ((( + “ (ran
𝐹 × ran 𝐺)) ∈ Fin ∧ ran (𝐹 ∘𝑓
+ 𝐺) ⊆ ( + “ (ran 𝐹 × ran 𝐺))) → ran (𝐹 ∘𝑓 + 𝐺) ∈ Fin) |
142 | 139, 140,
141 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ∈ Fin) |
143 | | ssdomg 8001 |
. . . . . . . . . . 11
⊢ (ran
(𝐹
∘𝑓 + 𝐺) ∈ Fin → ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ⊆ ran (𝐹 ∘𝑓
+ 𝐺) → (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼ ran (𝐹 ∘𝑓
+ 𝐺))) |
144 | 142, 57, 143 | mpisyl 21 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼ ran (𝐹 ∘𝑓
+ 𝐺)) |
145 | | isfinite 8549 |
. . . . . . . . . . . 12
⊢ (ran
(𝐹
∘𝑓 + 𝐺) ∈ Fin ↔ ran (𝐹 ∘𝑓 + 𝐺) ≺
ω) |
146 | 142, 145 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ≺
ω) |
147 | | sdomdom 7983 |
. . . . . . . . . . 11
⊢ (ran
(𝐹
∘𝑓 + 𝐺) ≺ ω → ran (𝐹 ∘𝑓
+ 𝐺) ≼
ω) |
148 | 146, 147 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ≼
ω) |
149 | | domtr 8009 |
. . . . . . . . . 10
⊢ (((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼ ran (𝐹 ∘𝑓
+ 𝐺) ∧ ran (𝐹 ∘𝑓 + 𝐺) ≼ ω) → (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼
ω) |
150 | 144, 148,
149 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼
ω) |
151 | 150 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼
ω) |
152 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑧(𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) |
153 | 152 | sigaclcuni 30181 |
. . . . . . . 8
⊢ ((dom
𝑀 ∈ ∪ ran sigAlgebra ∧ ∀𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀 ∧ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼ ω) →
∪ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀) |
154 | 52, 135, 151, 153 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → ∪ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀) |
155 | 56, 154 | syl5eqelr 2706 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∈ dom 𝑀) |
156 | | difpreima 6343 |
. . . . . . . . . 10
⊢ (Fun
(𝐹
∘𝑓 + 𝐺) → (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) = ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ (◡(𝐹 ∘𝑓 + 𝐺) “ ran (𝐹 ∘𝑓 + 𝐺)))) |
157 | 25, 45, 156 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) = ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ (◡(𝐹 ∘𝑓 + 𝐺) “ ran (𝐹 ∘𝑓 + 𝐺)))) |
158 | | cnvimarndm 5486 |
. . . . . . . . . . 11
⊢ (◡(𝐹 ∘𝑓 + 𝐺) “ ran (𝐹 ∘𝑓 + 𝐺)) = dom (𝐹 ∘𝑓 + 𝐺) |
159 | 158 | difeq2i 3725 |
. . . . . . . . . 10
⊢ ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ (◡(𝐹 ∘𝑓 + 𝐺) “ ran (𝐹 ∘𝑓 + 𝐺))) = ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ dom (𝐹 ∘𝑓 + 𝐺)) |
160 | | cnvimass 5485 |
. . . . . . . . . . 11
⊢ (◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ⊆ dom (𝐹 ∘𝑓 + 𝐺) |
161 | | ssdif0 3942 |
. . . . . . . . . . 11
⊢ ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ⊆ dom (𝐹 ∘𝑓 + 𝐺) ↔ ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ dom (𝐹 ∘𝑓 + 𝐺)) = ∅) |
162 | 160, 161 | mpbi 220 |
. . . . . . . . . 10
⊢ ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ dom (𝐹 ∘𝑓 + 𝐺)) = ∅ |
163 | 159, 162 | eqtri 2644 |
. . . . . . . . 9
⊢ ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ (◡(𝐹 ∘𝑓 + 𝐺) “ ran (𝐹 ∘𝑓 + 𝐺))) = ∅ |
164 | 157, 163 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝜑 → (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) = ∅) |
165 | | 0elsiga 30177 |
. . . . . . . . 9
⊢ (dom
𝑀 ∈ ∪ ran sigAlgebra → ∅ ∈ dom 𝑀) |
166 | 16, 50, 165 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ∅ ∈ dom 𝑀) |
167 | 164, 166 | eqeltrd 2701 |
. . . . . . 7
⊢ (𝜑 → (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) ∈ dom 𝑀) |
168 | 167 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) ∈ dom 𝑀) |
169 | | unelsiga 30197 |
. . . . . 6
⊢ ((dom
𝑀 ∈ ∪ ran sigAlgebra ∧ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∈ dom 𝑀 ∧ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) ∈ dom 𝑀) → ((◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∪ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))) ∈ dom 𝑀) |
170 | 52, 155, 168, 169 | syl3anc 1326 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → ((◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∪ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))) ∈ dom 𝑀) |
171 | 49, 170 | eqeltrd 2701 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → (◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∈ dom 𝑀) |
172 | 171 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))(◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∈ dom 𝑀) |
173 | 51, 38 | ismbfm 30314 |
. . 3
⊢ (𝜑 → ((𝐹 ∘𝑓 + 𝐺) ∈ (dom 𝑀MblFnM(sigaGen‘(TopOpen‘𝐾))) ↔ ((𝐹 ∘𝑓 + 𝐺) ∈ (∪ (sigaGen‘(TopOpen‘𝐾)) ↑𝑚 ∪ dom 𝑀) ∧ ∀𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))(◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∈ dom 𝑀))) |
174 | 42, 172, 173 | mpbir2and 957 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ (dom 𝑀MblFnM(sigaGen‘(TopOpen‘𝐾)))) |
175 | 64 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) = ∪
𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
176 | 175 | fveq2d 6195 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ (𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) = (𝑀‘∪
𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) |
177 | | measbasedom 30265 |
. . . . . . . . 9
⊢ (𝑀 ∈ ∪ ran measures ↔ 𝑀 ∈ (measures‘dom 𝑀)) |
178 | 16, 177 | sylib 208 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (measures‘dom 𝑀)) |
179 | 178 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ 𝑀 ∈
(measures‘dom 𝑀)) |
180 | | eldifi 3732 |
. . . . . . . 8
⊢ (𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)})
→ 𝑧 ∈ ran (𝐹 ∘𝑓
+ 𝐺)) |
181 | 180, 113 | sylan2 491 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ ∀𝑝 ∈
((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀) |
182 | 126 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ ω) |
183 | | sneq 4187 |
. . . . . . . . . . 11
⊢ (𝑥 = (1st ‘𝑝) → {𝑥} = {(1st ‘𝑝)}) |
184 | 183 | imaeq2d 5466 |
. . . . . . . . . 10
⊢ (𝑥 = (1st ‘𝑝) → (◡𝐹 “ {𝑥}) = (◡𝐹 “ {(1st ‘𝑝)})) |
185 | | sneq 4187 |
. . . . . . . . . . 11
⊢ (𝑦 = (2nd ‘𝑝) → {𝑦} = {(2nd ‘𝑝)}) |
186 | 185 | imaeq2d 5466 |
. . . . . . . . . 10
⊢ (𝑦 = (2nd ‘𝑝) → (◡𝐺 “ {𝑦}) = (◡𝐺 “ {(2nd ‘𝑝)})) |
187 | | ffun 6048 |
. . . . . . . . . . . 12
⊢ (𝐹:∪
dom 𝑀⟶∪ 𝐽
→ Fun 𝐹) |
188 | 18, 187 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐹) |
189 | | sndisj 4644 |
. . . . . . . . . . 11
⊢
Disj 𝑥 ∈
ran 𝐹{𝑥} |
190 | | disjpreima 29397 |
. . . . . . . . . . 11
⊢ ((Fun
𝐹 ∧ Disj 𝑥 ∈ ran 𝐹{𝑥}) → Disj 𝑥 ∈ ran 𝐹(◡𝐹 “ {𝑥})) |
191 | 188, 189,
190 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝜑 → Disj 𝑥 ∈ ran 𝐹(◡𝐹 “ {𝑥})) |
192 | | ffun 6048 |
. . . . . . . . . . . 12
⊢ (𝐺:∪
dom 𝑀⟶∪ 𝐽
→ Fun 𝐺) |
193 | 20, 192 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐺) |
194 | | sndisj 4644 |
. . . . . . . . . . 11
⊢
Disj 𝑦 ∈
ran 𝐺{𝑦} |
195 | | disjpreima 29397 |
. . . . . . . . . . 11
⊢ ((Fun
𝐺 ∧ Disj 𝑦 ∈ ran 𝐺{𝑦}) → Disj 𝑦 ∈ ran 𝐺(◡𝐺 “ {𝑦})) |
196 | 193, 194,
195 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝜑 → Disj 𝑦 ∈ ran 𝐺(◡𝐺 “ {𝑦})) |
197 | 184, 186,
191, 196 | disjxpin 29401 |
. . . . . . . . 9
⊢ (𝜑 → Disj 𝑝 ∈ (ran 𝐹 × ran 𝐺)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
198 | | disjss1 4626 |
. . . . . . . . 9
⊢ (((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (ran 𝐹 × ran 𝐺) → (Disj 𝑝 ∈ (ran 𝐹 × ran 𝐺)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) → Disj 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) |
199 | 118, 197,
198 | mpsyl 68 |
. . . . . . . 8
⊢ (𝜑 → Disj 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
200 | 199 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ Disj 𝑝 ∈
((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
201 | | measvuni 30277 |
. . . . . . 7
⊢ ((𝑀 ∈ (measures‘dom
𝑀) ∧ ∀𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀 ∧ (((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ ω ∧ Disj 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) → (𝑀‘∪
𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) = Σ*𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) |
202 | 179, 181,
182, 200, 201 | syl112anc 1330 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ (𝑀‘∪ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) = Σ*𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) |
203 | | ssfi 8180 |
. . . . . . . . 9
⊢ (((ran
𝐹 × ran 𝐺) ∈ Fin ∧ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (ran 𝐹 × ran 𝐺)) → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ∈ Fin) |
204 | 117, 118,
203 | sylancl 694 |
. . . . . . . 8
⊢ (𝜑 → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ∈ Fin) |
205 | 204 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ∈ Fin) |
206 | | simpll 790 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝜑) |
207 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) |
208 | 118, 207 | sseldi 3601 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ (ran 𝐹 × ran 𝐺)) |
209 | | xp1st 7198 |
. . . . . . . . 9
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (1st ‘𝑝) ∈ ran 𝐹) |
210 | 208, 209 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (1st ‘𝑝) ∈ ran 𝐹) |
211 | | xp2nd 7199 |
. . . . . . . . 9
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (2nd ‘𝑝) ∈ ran 𝐺) |
212 | 208, 211 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (2nd ‘𝑝) ∈ ran 𝐺) |
213 | | oveq12 6659 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 0 ∧ 𝑦 = 0 ) → (𝑥 + 𝑦) = ( 0 + 0 )) |
214 | | sibfof.5 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ( 0 + 0 ) =
(0g‘𝐾)) |
215 | 213, 214 | sylan9eqr 2678 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 = 0 ∧ 𝑦 = 0 )) → (𝑥 + 𝑦) = (0g‘𝐾)) |
216 | 215 | ex 450 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 = 0 ∧ 𝑦 = 0 ) → (𝑥 + 𝑦) = (0g‘𝐾))) |
217 | 216 | necon3ad 2807 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑥 + 𝑦) ≠ (0g‘𝐾) → ¬ (𝑥 = 0 ∧ 𝑦 = 0 ))) |
218 | | neorian 2888 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ) ↔ ¬ (𝑥 = 0 ∧ 𝑦 = 0 )) |
219 | 217, 218 | syl6ibr 242 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ))) |
220 | 219 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ))) |
221 | 220 | ralrimivva 2971 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ))) |
222 | 206, 221 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ))) |
223 | 69 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (◡ + “ {𝑧})) |
224 | 223 | sselda 3603 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ (◡ + “ {𝑧})) |
225 | | fniniseg 6338 |
. . . . . . . . . . . . 13
⊢ ( + Fn (𝐵 × 𝐵) → (𝑝 ∈ (◡ + “ {𝑧}) ↔ (𝑝 ∈ (𝐵 × 𝐵) ∧ ( + ‘𝑝) = 𝑧))) |
226 | 206, 63, 225 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (𝑝 ∈ (◡ + “ {𝑧}) ↔ (𝑝 ∈ (𝐵 × 𝐵) ∧ ( + ‘𝑝) = 𝑧))) |
227 | 224, 226 | mpbid 222 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (𝑝 ∈ (𝐵 × 𝐵) ∧ ( + ‘𝑝) = 𝑧)) |
228 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ (𝐵 × 𝐵) ∧ ( + ‘𝑝) = 𝑧) → ( + ‘𝑝) = 𝑧) |
229 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ (𝐵 × 𝐵) → 𝑝 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
230 | 229 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈ (𝐵 × 𝐵) → ( + ‘𝑝) = ( +
‘〈(1st ‘𝑝), (2nd ‘𝑝)〉)) |
231 | | df-ov 6653 |
. . . . . . . . . . . . . 14
⊢
((1st ‘𝑝) + (2nd
‘𝑝)) = ( +
‘〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
232 | 230, 231 | syl6eqr 2674 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ (𝐵 × 𝐵) → ( + ‘𝑝) = ((1st ‘𝑝) + (2nd
‘𝑝))) |
233 | 232 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ (𝐵 × 𝐵) ∧ ( + ‘𝑝) = 𝑧) → ( + ‘𝑝) = ((1st ‘𝑝) + (2nd
‘𝑝))) |
234 | 228, 233 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ (𝐵 × 𝐵) ∧ ( + ‘𝑝) = 𝑧) → 𝑧 = ((1st ‘𝑝) + (2nd
‘𝑝))) |
235 | 227, 234 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑧 = ((1st ‘𝑝) + (2nd
‘𝑝))) |
236 | | simplr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)})) |
237 | 236 | eldifbd 3587 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → ¬ 𝑧 ∈ {(0g‘𝐾)}) |
238 | | velsn 4193 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈
{(0g‘𝐾)}
↔ 𝑧 =
(0g‘𝐾)) |
239 | 238 | necon3bbii 2841 |
. . . . . . . . . . 11
⊢ (¬
𝑧 ∈
{(0g‘𝐾)}
↔ 𝑧 ≠
(0g‘𝐾)) |
240 | 237, 239 | sylib 208 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑧 ≠ (0g‘𝐾)) |
241 | 235, 240 | eqnetrrd 2862 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → ((1st ‘𝑝) + (2nd
‘𝑝)) ≠
(0g‘𝐾)) |
242 | 180, 76 | sylanl2 683 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ (𝐵 × 𝐵)) |
243 | 242, 89 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (1st ‘𝑝) ∈ 𝐵) |
244 | 242, 102 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (2nd ‘𝑝) ∈ 𝐵) |
245 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1st ‘𝑝) → (𝑥 + 𝑦) = ((1st ‘𝑝) + 𝑦)) |
246 | 245 | neeq1d 2853 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘𝑝) → ((𝑥 + 𝑦) ≠ (0g‘𝐾) ↔ ((1st ‘𝑝) + 𝑦) ≠ (0g‘𝐾))) |
247 | | neeq1 2856 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1st ‘𝑝) → (𝑥 ≠ 0 ↔ (1st
‘𝑝) ≠ 0
)) |
248 | 247 | orbi1d 739 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘𝑝) → ((𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ) ↔ ((1st
‘𝑝) ≠ 0 ∨ 𝑦 ≠ 0 ))) |
249 | 246, 248 | imbi12d 334 |
. . . . . . . . . . 11
⊢ (𝑥 = (1st ‘𝑝) → (((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 )) ↔
(((1st ‘𝑝)
+ 𝑦) ≠
(0g‘𝐾)
→ ((1st ‘𝑝) ≠ 0 ∨ 𝑦 ≠ 0 )))) |
250 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (2nd ‘𝑝) → ((1st
‘𝑝) + 𝑦) = ((1st
‘𝑝) +
(2nd ‘𝑝))) |
251 | 250 | neeq1d 2853 |
. . . . . . . . . . . 12
⊢ (𝑦 = (2nd ‘𝑝) → (((1st
‘𝑝) + 𝑦) ≠
(0g‘𝐾)
↔ ((1st ‘𝑝) + (2nd
‘𝑝)) ≠
(0g‘𝐾))) |
252 | | neeq1 2856 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (2nd ‘𝑝) → (𝑦 ≠ 0 ↔ (2nd
‘𝑝) ≠ 0
)) |
253 | 252 | orbi2d 738 |
. . . . . . . . . . . 12
⊢ (𝑦 = (2nd ‘𝑝) → (((1st
‘𝑝) ≠ 0 ∨ 𝑦 ≠ 0 ) ↔ ((1st
‘𝑝) ≠ 0 ∨
(2nd ‘𝑝)
≠ 0
))) |
254 | 251, 253 | imbi12d 334 |
. . . . . . . . . . 11
⊢ (𝑦 = (2nd ‘𝑝) → ((((1st
‘𝑝) + 𝑦) ≠
(0g‘𝐾)
→ ((1st ‘𝑝) ≠ 0 ∨ 𝑦 ≠ 0 )) ↔
(((1st ‘𝑝)
+
(2nd ‘𝑝))
≠ (0g‘𝐾) → ((1st ‘𝑝) ≠ 0 ∨ (2nd
‘𝑝) ≠ 0
)))) |
255 | 249, 254 | rspc2v 3322 |
. . . . . . . . . 10
⊢
(((1st ‘𝑝) ∈ 𝐵 ∧ (2nd ‘𝑝) ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 )) →
(((1st ‘𝑝)
+
(2nd ‘𝑝))
≠ (0g‘𝐾) → ((1st ‘𝑝) ≠ 0 ∨ (2nd
‘𝑝) ≠ 0
)))) |
256 | 243, 244,
255 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 )) →
(((1st ‘𝑝)
+
(2nd ‘𝑝))
≠ (0g‘𝐾) → ((1st ‘𝑝) ≠ 0 ∨ (2nd
‘𝑝) ≠ 0
)))) |
257 | 222, 241,
256 | mp2d 49 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → ((1st ‘𝑝) ≠ 0 ∨ (2nd
‘𝑝) ≠ 0
)) |
258 | 3, 4, 11, 12, 13, 14, 15, 16, 17, 19, 2, 78 | sibfinima 30401 |
. . . . . . . 8
⊢ (((𝜑 ∧ (1st
‘𝑝) ∈ ran 𝐹 ∧ (2nd
‘𝑝) ∈ ran 𝐺) ∧ ((1st
‘𝑝) ≠ 0 ∨
(2nd ‘𝑝)
≠ 0 ))
→ (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈
(0[,)+∞)) |
259 | 206, 210,
212, 257, 258 | syl31anc 1329 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈
(0[,)+∞)) |
260 | 205, 259 | esumpfinval 30137 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ Σ*𝑝
∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) = Σ𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) |
261 | 176, 202,
260 | 3eqtrd 2660 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ (𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) = Σ𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) |
262 | | rge0ssre 12280 |
. . . . . . 7
⊢
(0[,)+∞) ⊆ ℝ |
263 | 262, 259 | sseldi 3601 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈
ℝ) |
264 | 205, 263 | fsumrecl 14465 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ Σ𝑝 ∈
((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈
ℝ) |
265 | 261, 264 | eqeltrd 2701 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ (𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) ∈ ℝ) |
266 | 179 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑀 ∈ (measures‘dom 𝑀)) |
267 | 180, 112 | sylanl2 683 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀) |
268 | | measge0 30270 |
. . . . . . 7
⊢ ((𝑀 ∈ (measures‘dom
𝑀) ∧ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀) → 0 ≤ (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) |
269 | 266, 267,
268 | syl2anc 693 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 0 ≤ (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) |
270 | 205, 263,
269 | fsumge0 14527 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ 0 ≤ Σ𝑝
∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) |
271 | 270, 261 | breqtrrd 4681 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ 0 ≤ (𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}))) |
272 | | elrege0 12278 |
. . . 4
⊢ ((𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) ∈ (0[,)+∞) ↔ ((𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) ∈ ℝ ∧ 0 ≤ (𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})))) |
273 | 265, 271,
272 | sylanbrc 698 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)}))
→ (𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) ∈ (0[,)+∞)) |
274 | 273 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)})(𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) ∈ (0[,)+∞)) |
275 | | eqid 2622 |
. . 3
⊢
(sigaGen‘(TopOpen‘𝐾)) = (sigaGen‘(TopOpen‘𝐾)) |
276 | | eqid 2622 |
. . 3
⊢
(0g‘𝐾) = (0g‘𝐾) |
277 | | eqid 2622 |
. . 3
⊢ (
·𝑠 ‘𝐾) = ( ·𝑠
‘𝐾) |
278 | | eqid 2622 |
. . 3
⊢
(ℝHom‘(Scalar‘𝐾)) = (ℝHom‘(Scalar‘𝐾)) |
279 | 27, 28, 275, 276, 277, 278, 26, 16 | issibf 30395 |
. 2
⊢ (𝜑 → ((𝐹 ∘𝑓 + 𝐺) ∈ dom (𝐾sitg𝑀) ↔ ((𝐹 ∘𝑓 + 𝐺) ∈ (dom 𝑀MblFnM(sigaGen‘(TopOpen‘𝐾))) ∧ ran (𝐹 ∘𝑓 + 𝐺) ∈ Fin ∧ ∀𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖
{(0g‘𝐾)})(𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) ∈ (0[,)+∞)))) |
280 | 174, 142,
274, 279 | mpbir3and 1245 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ dom (𝐾sitg𝑀)) |