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 22301 |
. . . . . . . . . . 11
β’ (π β TopSp β π΅ = βͺ
π½) |
6 | 2, 5 | syl 17 |
. . . . . . . . . 10
β’ (π β π΅ = βͺ π½) |
7 | 6 | sqxpeqd 5670 |
. . . . . . . . 9
β’ (π β (π΅ Γ π΅) = (βͺ π½ Γ βͺ π½)) |
8 | 7 | feq2d 6659 |
. . . . . . . 8
β’ (π β ( + :(π΅ Γ π΅)βΆπΆ β + :(βͺ π½
Γ βͺ π½)βΆπΆ)) |
9 | 1, 8 | mpbid 231 |
. . . . . . 7
β’ (π β + :(βͺ π½
Γ βͺ π½)βΆπΆ) |
10 | 9 | fovcdmda 7530 |
. . . . . 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 32976 |
. . . . . 6
β’ (π β πΉ:βͺ dom πβΆβͺ π½) |
19 | | sibfof.2 |
. . . . . . 7
β’ (π β πΊ β dom (πsitgπ)) |
20 | 3, 4, 11, 12, 13, 14, 15, 16, 19 | sibff 32976 |
. . . . . 6
β’ (π β πΊ:βͺ dom πβΆβͺ π½) |
21 | | dmexg 7845 |
. . . . . . 7
β’ (π β βͺ ran measures β dom π β V) |
22 | | uniexg 7682 |
. . . . . . 7
β’ (dom
π β V β βͺ dom π β V) |
23 | 16, 21, 22 | 3syl 18 |
. . . . . 6
β’ (π β βͺ dom π β V) |
24 | | inidm 4183 |
. . . . . 6
β’ (βͺ dom π β© βͺ dom
π) = βͺ dom π |
25 | 10, 18, 20, 23, 23, 24 | off 7640 |
. . . . 5
β’ (π β (πΉ βf + πΊ):βͺ dom πβΆπΆ) |
26 | | sibfof.3 |
. . . . . . . 8
β’ (π β πΎ β TopSp) |
27 | | sibfof.c |
. . . . . . . . 9
β’ πΆ = (BaseβπΎ) |
28 | | eqid 2737 |
. . . . . . . . 9
β’
(TopOpenβπΎ) =
(TopOpenβπΎ) |
29 | 27, 28 | tpsuni 22301 |
. . . . . . . 8
β’ (πΎ β TopSp β πΆ = βͺ
(TopOpenβπΎ)) |
30 | 26, 29 | syl 17 |
. . . . . . 7
β’ (π β πΆ = βͺ
(TopOpenβπΎ)) |
31 | | fvex 6860 |
. . . . . . . 8
β’
(TopOpenβπΎ)
β V |
32 | | unisg 32782 |
. . . . . . . 8
β’
((TopOpenβπΎ)
β V β βͺ
(sigaGenβ(TopOpenβπΎ)) = βͺ
(TopOpenβπΎ)) |
33 | 31, 32 | ax-mp 5 |
. . . . . . 7
β’ βͺ (sigaGenβ(TopOpenβπΎ)) = βͺ
(TopOpenβπΎ) |
34 | 30, 33 | eqtr4di 2795 |
. . . . . 6
β’ (π β πΆ = βͺ
(sigaGenβ(TopOpenβπΎ))) |
35 | 34 | feq3d 6660 |
. . . . 5
β’ (π β ((πΉ βf + πΊ):βͺ dom πβΆπΆ β (πΉ βf + πΊ):βͺ dom πβΆβͺ (sigaGenβ(TopOpenβπΎ)))) |
36 | 25, 35 | mpbid 231 |
. . . 4
β’ (π β (πΉ βf + πΊ):βͺ dom πβΆβͺ (sigaGenβ(TopOpenβπΎ))) |
37 | 31 | a1i 11 |
. . . . . . 7
β’ (π β (TopOpenβπΎ) β V) |
38 | 37 | sgsiga 32781 |
. . . . . 6
β’ (π β
(sigaGenβ(TopOpenβπΎ)) β βͺ ran
sigAlgebra) |
39 | 38 | uniexd 7684 |
. . . . 5
β’ (π β βͺ (sigaGenβ(TopOpenβπΎ)) β V) |
40 | 39, 23 | elmapd 8786 |
. . . 4
β’ (π β ((πΉ βf + πΊ) β (βͺ
(sigaGenβ(TopOpenβπΎ)) βm βͺ dom π) β (πΉ βf + πΊ):βͺ dom πβΆβͺ (sigaGenβ(TopOpenβπΎ)))) |
41 | 36, 40 | mpbird 257 |
. . 3
β’ (π β (πΉ βf + πΊ) β (βͺ
(sigaGenβ(TopOpenβπΎ)) βm βͺ dom π)) |
42 | | inundif 4443 |
. . . . . . 7
β’ ((π β© ran (πΉ βf + πΊ)) βͺ (π β ran (πΉ βf + πΊ))) = π |
43 | 42 | imaeq2i 6016 |
. . . . . 6
β’ (β‘(πΉ βf + πΊ) β ((π β© ran (πΉ βf + πΊ)) βͺ (π β ran (πΉ βf + πΊ)))) = (β‘(πΉ βf + πΊ) β π) |
44 | | ffun 6676 |
. . . . . . . 8
β’ ((πΉ βf + πΊ):βͺ
dom πβΆπΆ β Fun (πΉ βf + πΊ)) |
45 | | unpreima 7018 |
. . . . . . . 8
β’ (Fun
(πΉ βf
+ πΊ) β (β‘(πΉ βf + πΊ) β ((π β© ran (πΉ βf + πΊ)) βͺ (π β ran (πΉ βf + πΊ)))) = ((β‘(πΉ βf + πΊ) β (π β© ran (πΉ βf + πΊ))) βͺ (β‘(πΉ βf + πΊ) β (π β ran (πΉ βf + πΊ))))) |
46 | 25, 44, 45 | 3syl 18 |
. . . . . . 7
β’ (π β (β‘(πΉ βf + πΊ) β ((π β© ran (πΉ βf + πΊ)) βͺ (π β ran (πΉ βf + πΊ)))) = ((β‘(πΉ βf + πΊ) β (π β© ran (πΉ βf + πΊ))) βͺ (β‘(πΉ βf + πΊ) β (π β ran (πΉ βf + πΊ))))) |
47 | 46 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (sigaGenβ(TopOpenβπΎ))) β (β‘(πΉ βf + πΊ) β ((π β© ran (πΉ βf + πΊ)) βͺ (π β ran (πΉ βf + πΊ)))) = ((β‘(πΉ βf + πΊ) β (π β© ran (πΉ βf + πΊ))) βͺ (β‘(πΉ βf + πΊ) β (π β ran (πΉ βf + πΊ))))) |
48 | 43, 47 | eqtr3id 2791 |
. . . . 5
β’ ((π β§ π β (sigaGenβ(TopOpenβπΎ))) β (β‘(πΉ βf + πΊ) β π) = ((β‘(πΉ βf + πΊ) β (π β© ran (πΉ βf + πΊ))) βͺ (β‘(πΉ βf + πΊ) β (π β ran (πΉ βf + πΊ))))) |
49 | | dmmeas 32840 |
. . . . . . . 8
β’ (π β βͺ ran measures β dom π β βͺ ran
sigAlgebra) |
50 | 16, 49 | syl 17 |
. . . . . . 7
β’ (π β dom π β βͺ ran
sigAlgebra) |
51 | 50 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (sigaGenβ(TopOpenβπΎ))) β dom π β βͺ ran
sigAlgebra) |
52 | | imaiun 7197 |
. . . . . . . 8
β’ (β‘(πΉ βf + πΊ) β βͺ π§ β (π β© ran (πΉ βf + πΊ)){π§}) = βͺ
π§ β (π β© ran (πΉ βf + πΊ))(β‘(πΉ βf + πΊ) β {π§}) |
53 | | iunid 5025 |
. . . . . . . . 9
β’ βͺ π§ β (π β© ran (πΉ βf + πΊ)){π§} = (π β© ran (πΉ βf + πΊ)) |
54 | 53 | imaeq2i 6016 |
. . . . . . . 8
β’ (β‘(πΉ βf + πΊ) β βͺ π§ β (π β© ran (πΉ βf + πΊ)){π§}) = (β‘(πΉ βf + πΊ) β (π β© ran (πΉ βf + πΊ))) |
55 | 52, 54 | eqtr3i 2767 |
. . . . . . 7
β’ βͺ π§ β (π β© ran (πΉ βf + πΊ))(β‘(πΉ βf + πΊ) β {π§}) = (β‘(πΉ βf + πΊ) β (π β© ran (πΉ βf + πΊ))) |
56 | | inss2 4194 |
. . . . . . . . . 10
β’ (π β© ran (πΉ βf + πΊ)) β ran (πΉ βf + πΊ) |
57 | 6 | feq3d 6660 |
. . . . . . . . . . . . . . 15
β’ (π β (πΉ:βͺ dom πβΆπ΅ β πΉ:βͺ dom πβΆβͺ π½)) |
58 | 18, 57 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (π β πΉ:βͺ dom πβΆπ΅) |
59 | 6 | feq3d 6660 |
. . . . . . . . . . . . . . 15
β’ (π β (πΊ:βͺ dom πβΆπ΅ β πΊ:βͺ dom πβΆβͺ π½)) |
60 | 20, 59 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (π β πΊ:βͺ dom πβΆπ΅) |
61 | 1 | ffnd 6674 |
. . . . . . . . . . . . . 14
β’ (π β + Fn (π΅ Γ π΅)) |
62 | 58, 60, 23, 61 | ofpreima2 31624 |
. . . . . . . . . . . . 13
β’ (π β (β‘(πΉ βf + πΊ) β {π§}) = βͺ
π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)}))) |
63 | 62 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β ran (πΉ βf + πΊ)) β (β‘(πΉ βf + πΊ) β {π§}) = βͺ
π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)}))) |
64 | 50 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β ran (πΉ βf + πΊ)) β dom π β βͺ ran
sigAlgebra) |
65 | 50 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β ran (πΉ βf + πΊ)) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β dom π β βͺ ran
sigAlgebra) |
66 | | simpll 766 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β ran (πΉ βf + πΊ)) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β π) |
67 | | inss1 4193 |
. . . . . . . . . . . . . . . . . 18
β’ ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) β (β‘ + β {π§}) |
68 | | cnvimass 6038 |
. . . . . . . . . . . . . . . . . . . 20
β’ (β‘ + β {π§}) β dom + |
69 | 68, 1 | fssdm 6693 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (β‘ + β {π§}) β (π΅ Γ π΅)) |
70 | 69 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β ran (πΉ βf + πΊ)) β (β‘ + β {π§}) β (π΅ Γ π΅)) |
71 | 67, 70 | sstrid 3960 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β ran (πΉ βf + πΊ)) β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) β (π΅ Γ π΅)) |
72 | 71 | sselda 3949 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π§ β ran (πΉ βf + πΊ)) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β π β (π΅ Γ π΅)) |
73 | 50 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΅ Γ π΅)) β dom π β βͺ ran
sigAlgebra) |
74 | | sibfof.4 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π½ β Fre) |
75 | 74 | sgsiga 32781 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (sigaGenβπ½) β βͺ ran sigAlgebra) |
76 | 11, 75 | eqeltrid 2842 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β βͺ ran
sigAlgebra) |
77 | 76 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΅ Γ π΅)) β π β βͺ ran
sigAlgebra) |
78 | 3, 4, 11, 12, 13, 14, 15, 16, 17 | sibfmbl 32975 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΉ β (dom πMblFnMπ)) |
79 | 78 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΅ Γ π΅)) β πΉ β (dom πMblFnMπ)) |
80 | 4 | tpstop 22302 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β TopSp β π½ β Top) |
81 | | cldssbrsiga 32826 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π½ β Top β
(Clsdβπ½) β
(sigaGenβπ½)) |
82 | 2, 80, 81 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (Clsdβπ½) β (sigaGenβπ½)) |
83 | 82 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π΅ Γ π΅)) β (Clsdβπ½) β (sigaGenβπ½)) |
84 | 74 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (π΅ Γ π΅)) β π½ β Fre) |
85 | | xp1st 7958 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π΅ Γ π΅) β (1st βπ) β π΅) |
86 | 85 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (π΅ Γ π΅)) β (1st βπ) β π΅) |
87 | 6 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (π΅ Γ π΅)) β π΅ = βͺ π½) |
88 | 86, 87 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (π΅ Γ π΅)) β (1st βπ) β βͺ π½) |
89 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
β’ βͺ π½ =
βͺ π½ |
90 | 89 | t1sncld 22693 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ β Fre β§
(1st βπ)
β βͺ π½) β {(1st βπ)} β (Clsdβπ½)) |
91 | 84, 88, 90 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π΅ Γ π΅)) β {(1st βπ)} β (Clsdβπ½)) |
92 | 83, 91 | sseldd 3950 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π΅ Γ π΅)) β {(1st βπ)} β (sigaGenβπ½)) |
93 | 92, 11 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΅ Γ π΅)) β {(1st βπ)} β π) |
94 | 73, 77, 79, 93 | mbfmcnvima 32895 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΅ Γ π΅)) β (β‘πΉ β {(1st βπ)}) β dom π) |
95 | 66, 72, 94 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β ran (πΉ βf + πΊ)) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β (β‘πΉ β {(1st βπ)}) β dom π) |
96 | 3, 4, 11, 12, 13, 14, 15, 16, 19 | sibfmbl 32975 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΊ β (dom πMblFnMπ)) |
97 | 96 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΅ Γ π΅)) β πΊ β (dom πMblFnMπ)) |
98 | | xp2nd 7959 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π΅ Γ π΅) β (2nd βπ) β π΅) |
99 | 98 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (π΅ Γ π΅)) β (2nd βπ) β π΅) |
100 | 99, 87 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (π΅ Γ π΅)) β (2nd βπ) β βͺ π½) |
101 | 89 | t1sncld 22693 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ β Fre β§
(2nd βπ)
β βͺ π½) β {(2nd βπ)} β (Clsdβπ½)) |
102 | 84, 100, 101 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π΅ Γ π΅)) β {(2nd βπ)} β (Clsdβπ½)) |
103 | 83, 102 | sseldd 3950 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π΅ Γ π΅)) β {(2nd βπ)} β (sigaGenβπ½)) |
104 | 103, 11 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π΅ Γ π΅)) β {(2nd βπ)} β π) |
105 | 73, 77, 97, 104 | mbfmcnvima 32895 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π΅ Γ π΅)) β (β‘πΊ β {(2nd βπ)}) β dom π) |
106 | 66, 72, 105 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π§ β ran (πΉ βf + πΊ)) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β (β‘πΊ β {(2nd βπ)}) β dom π) |
107 | | inelsiga 32774 |
. . . . . . . . . . . . . . 15
β’ ((dom
π β βͺ ran sigAlgebra β§ (β‘πΉ β {(1st βπ)}) β dom π β§ (β‘πΊ β {(2nd βπ)}) β dom π) β ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})) β dom π) |
108 | 65, 95, 106, 107 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β§ π§ β ran (πΉ βf + πΊ)) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})) β dom π) |
109 | 108 | ralrimiva 3144 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β ran (πΉ βf + πΊ)) β βπ β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})) β dom π) |
110 | 3, 4, 11, 12, 13, 14, 15, 16, 17 | sibfrn 32977 |
. . . . . . . . . . . . . . . . 17
β’ (π β ran πΉ β Fin) |
111 | 3, 4, 11, 12, 13, 14, 15, 16, 19 | sibfrn 32977 |
. . . . . . . . . . . . . . . . 17
β’ (π β ran πΊ β Fin) |
112 | | xpfi 9268 |
. . . . . . . . . . . . . . . . 17
β’ ((ran
πΉ β Fin β§ ran
πΊ β Fin) β (ran
πΉ Γ ran πΊ) β Fin) |
113 | 110, 111,
112 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (π β (ran πΉ Γ ran πΊ) β Fin) |
114 | | inss2 4194 |
. . . . . . . . . . . . . . . 16
β’ ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) β (ran πΉ Γ ran πΊ) |
115 | | ssdomg 8947 |
. . . . . . . . . . . . . . . 16
β’ ((ran
πΉ Γ ran πΊ) β Fin β (((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) β (ran πΉ Γ ran πΊ) β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) βΌ (ran πΉ Γ ran πΊ))) |
116 | 113, 114,
115 | mpisyl 21 |
. . . . . . . . . . . . . . 15
β’ (π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) βΌ (ran πΉ Γ ran πΊ)) |
117 | | isfinite 9595 |
. . . . . . . . . . . . . . . . 17
β’ ((ran
πΉ Γ ran πΊ) β Fin β (ran πΉ Γ ran πΊ) βΊ Ο) |
118 | 117 | biimpi 215 |
. . . . . . . . . . . . . . . 16
β’ ((ran
πΉ Γ ran πΊ) β Fin β (ran πΉ Γ ran πΊ) βΊ Ο) |
119 | | sdomdom 8927 |
. . . . . . . . . . . . . . . 16
β’ ((ran
πΉ Γ ran πΊ) βΊ Ο β (ran
πΉ Γ ran πΊ) βΌ
Ο) |
120 | 113, 118,
119 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ (π β (ran πΉ Γ ran πΊ) βΌ Ο) |
121 | | domtr 8954 |
. . . . . . . . . . . . . . 15
β’ ((((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) βΌ (ran πΉ Γ ran πΊ) β§ (ran πΉ Γ ran πΊ) βΌ Ο) β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) βΌ Ο) |
122 | 116, 120,
121 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) βΌ Ο) |
123 | 122 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β ran (πΉ βf + πΊ)) β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) βΌ Ο) |
124 | | nfcv 2908 |
. . . . . . . . . . . . . 14
β’
β²π((β‘
+ β
{π§}) β© (ran πΉ Γ ran πΊ)) |
125 | 124 | sigaclcuni 32757 |
. . . . . . . . . . . . 13
β’ ((dom
π β βͺ ran sigAlgebra β§ βπ β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})) β dom π β§ ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) βΌ Ο) β βͺ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})) β dom π) |
126 | 64, 109, 123, 125 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β ran (πΉ βf + πΊ)) β βͺ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})) β dom π) |
127 | 63, 126 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ ((π β§ π§ β ran (πΉ βf + πΊ)) β (β‘(πΉ βf + πΊ) β {π§}) β dom π) |
128 | 127 | ralrimiva 3144 |
. . . . . . . . . 10
β’ (π β βπ§ β ran (πΉ βf + πΊ)(β‘(πΉ βf + πΊ) β {π§}) β dom π) |
129 | | ssralv 4015 |
. . . . . . . . . 10
β’ ((π β© ran (πΉ βf + πΊ)) β ran (πΉ βf + πΊ) β (βπ§ β ran (πΉ βf + πΊ)(β‘(πΉ βf + πΊ) β {π§}) β dom π β βπ§ β (π β© ran (πΉ βf + πΊ))(β‘(πΉ βf + πΊ) β {π§}) β dom π)) |
130 | 56, 128, 129 | mpsyl 68 |
. . . . . . . . 9
β’ (π β βπ§ β (π β© ran (πΉ βf + πΊ))(β‘(πΉ βf + πΊ) β {π§}) β dom π) |
131 | 130 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (sigaGenβ(TopOpenβπΎ))) β βπ§ β (π β© ran (πΉ βf + πΊ))(β‘(πΉ βf + πΊ) β {π§}) β dom π) |
132 | 1 | ffund 6677 |
. . . . . . . . . . . . 13
β’ (π β Fun + ) |
133 | | imafi 9126 |
. . . . . . . . . . . . 13
β’ ((Fun
+ β§
(ran πΉ Γ ran πΊ) β Fin) β ( + β (ran
πΉ Γ ran πΊ)) β Fin) |
134 | 132, 113,
133 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ( + β (ran πΉ Γ ran πΊ)) β Fin) |
135 | 18, 20, 9, 23 | ofrn2 31598 |
. . . . . . . . . . . 12
β’ (π β ran (πΉ βf + πΊ) β ( + β (ran πΉ Γ ran πΊ))) |
136 | | ssfi 9124 |
. . . . . . . . . . . 12
β’ ((( + β (ran
πΉ Γ ran πΊ)) β Fin β§ ran (πΉ βf + πΊ) β ( + β (ran πΉ Γ ran πΊ))) β ran (πΉ βf + πΊ) β Fin) |
137 | 134, 135,
136 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β ran (πΉ βf + πΊ) β Fin) |
138 | | ssdomg 8947 |
. . . . . . . . . . 11
β’ (ran
(πΉ βf
+ πΊ) β Fin β ((π β© ran (πΉ βf + πΊ)) β ran (πΉ βf + πΊ) β (π β© ran (πΉ βf + πΊ)) βΌ ran (πΉ βf + πΊ))) |
139 | 137, 56, 138 | mpisyl 21 |
. . . . . . . . . 10
β’ (π β (π β© ran (πΉ βf + πΊ)) βΌ ran (πΉ βf + πΊ)) |
140 | | isfinite 9595 |
. . . . . . . . . . . 12
β’ (ran
(πΉ βf
+ πΊ) β Fin β ran (πΉ βf + πΊ) βΊ
Ο) |
141 | 137, 140 | sylib 217 |
. . . . . . . . . . 11
β’ (π β ran (πΉ βf + πΊ) βΊ Ο) |
142 | | sdomdom 8927 |
. . . . . . . . . . 11
β’ (ran
(πΉ βf
+ πΊ) βΊ Ο β ran
(πΉ βf
+ πΊ) βΌ
Ο) |
143 | 141, 142 | syl 17 |
. . . . . . . . . 10
β’ (π β ran (πΉ βf + πΊ) βΌ Ο) |
144 | | domtr 8954 |
. . . . . . . . . 10
β’ (((π β© ran (πΉ βf + πΊ)) βΌ ran (πΉ βf + πΊ) β§ ran (πΉ βf + πΊ) βΌ Ο) β (π β© ran (πΉ βf + πΊ)) βΌ Ο) |
145 | 139, 143,
144 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π β© ran (πΉ βf + πΊ)) βΌ Ο) |
146 | 145 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (sigaGenβ(TopOpenβπΎ))) β (π β© ran (πΉ βf + πΊ)) βΌ Ο) |
147 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π§(π β© ran (πΉ βf + πΊ)) |
148 | 147 | sigaclcuni 32757 |
. . . . . . . 8
β’ ((dom
π β βͺ ran sigAlgebra β§ βπ§ β (π β© ran (πΉ βf + πΊ))(β‘(πΉ βf + πΊ) β {π§}) β dom π β§ (π β© ran (πΉ βf + πΊ)) βΌ Ο) β βͺ π§ β (π β© ran (πΉ βf + πΊ))(β‘(πΉ βf + πΊ) β {π§}) β dom π) |
149 | 51, 131, 146, 148 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β (sigaGenβ(TopOpenβπΎ))) β βͺ π§ β (π β© ran (πΉ βf + πΊ))(β‘(πΉ βf + πΊ) β {π§}) β dom π) |
150 | 55, 149 | eqeltrrid 2843 |
. . . . . 6
β’ ((π β§ π β (sigaGenβ(TopOpenβπΎ))) β (β‘(πΉ βf + πΊ) β (π β© ran (πΉ βf + πΊ))) β dom π) |
151 | | difpreima 7020 |
. . . . . . . . . 10
β’ (Fun
(πΉ βf
+ πΊ) β (β‘(πΉ βf + πΊ) β (π β ran (πΉ βf + πΊ))) = ((β‘(πΉ βf + πΊ) β π) β (β‘(πΉ βf + πΊ) β ran (πΉ βf + πΊ)))) |
152 | 25, 44, 151 | 3syl 18 |
. . . . . . . . 9
β’ (π β (β‘(πΉ βf + πΊ) β (π β ran (πΉ βf + πΊ))) = ((β‘(πΉ βf + πΊ) β π) β (β‘(πΉ βf + πΊ) β ran (πΉ βf + πΊ)))) |
153 | | cnvimarndm 6039 |
. . . . . . . . . . 11
β’ (β‘(πΉ βf + πΊ) β ran (πΉ βf + πΊ)) = dom (πΉ βf + πΊ) |
154 | 153 | difeq2i 4084 |
. . . . . . . . . 10
β’ ((β‘(πΉ βf + πΊ) β π) β (β‘(πΉ βf + πΊ) β ran (πΉ βf + πΊ))) = ((β‘(πΉ βf + πΊ) β π) β dom (πΉ βf + πΊ)) |
155 | | cnvimass 6038 |
. . . . . . . . . . 11
β’ (β‘(πΉ βf + πΊ) β π) β dom (πΉ βf + πΊ) |
156 | | ssdif0 4328 |
. . . . . . . . . . 11
β’ ((β‘(πΉ βf + πΊ) β π) β dom (πΉ βf + πΊ) β ((β‘(πΉ βf + πΊ) β π) β dom (πΉ βf + πΊ)) = β
) |
157 | 155, 156 | mpbi 229 |
. . . . . . . . . 10
β’ ((β‘(πΉ βf + πΊ) β π) β dom (πΉ βf + πΊ)) = β
|
158 | 154, 157 | eqtri 2765 |
. . . . . . . . 9
β’ ((β‘(πΉ βf + πΊ) β π) β (β‘(πΉ βf + πΊ) β ran (πΉ βf + πΊ))) = β
|
159 | 152, 158 | eqtrdi 2793 |
. . . . . . . 8
β’ (π β (β‘(πΉ βf + πΊ) β (π β ran (πΉ βf + πΊ))) = β
) |
160 | | 0elsiga 32753 |
. . . . . . . . 9
β’ (dom
π β βͺ ran sigAlgebra β β
β dom π) |
161 | 16, 49, 160 | 3syl 18 |
. . . . . . . 8
β’ (π β β
β dom π) |
162 | 159, 161 | eqeltrd 2838 |
. . . . . . 7
β’ (π β (β‘(πΉ βf + πΊ) β (π β ran (πΉ βf + πΊ))) β dom π) |
163 | 162 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (sigaGenβ(TopOpenβπΎ))) β (β‘(πΉ βf + πΊ) β (π β ran (πΉ βf + πΊ))) β dom π) |
164 | | unelsiga 32773 |
. . . . . 6
β’ ((dom
π β βͺ ran sigAlgebra β§ (β‘(πΉ βf + πΊ) β (π β© ran (πΉ βf + πΊ))) β dom π β§ (β‘(πΉ βf + πΊ) β (π β ran (πΉ βf + πΊ))) β dom π) β ((β‘(πΉ βf + πΊ) β (π β© ran (πΉ βf + πΊ))) βͺ (β‘(πΉ βf + πΊ) β (π β ran (πΉ βf + πΊ)))) β dom π) |
165 | 51, 150, 163, 164 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π β (sigaGenβ(TopOpenβπΎ))) β ((β‘(πΉ βf + πΊ) β (π β© ran (πΉ βf + πΊ))) βͺ (β‘(πΉ βf + πΊ) β (π β ran (πΉ βf + πΊ)))) β dom π) |
166 | 48, 165 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π β (sigaGenβ(TopOpenβπΎ))) β (β‘(πΉ βf + πΊ) β π) β dom π) |
167 | 166 | ralrimiva 3144 |
. . 3
β’ (π β βπ β (sigaGenβ(TopOpenβπΎ))(β‘(πΉ βf + πΊ) β π) β dom π) |
168 | 50, 38 | ismbfm 32890 |
. . 3
β’ (π β ((πΉ βf + πΊ) β (dom πMblFnM(sigaGenβ(TopOpenβπΎ))) β ((πΉ βf + πΊ) β (βͺ
(sigaGenβ(TopOpenβπΎ)) βm βͺ dom π) β§ βπ β (sigaGenβ(TopOpenβπΎ))(β‘(πΉ βf + πΊ) β π) β dom π))) |
169 | 41, 167, 168 | mpbir2and 712 |
. 2
β’ (π β (πΉ βf + πΊ) β (dom πMblFnM(sigaGenβ(TopOpenβπΎ)))) |
170 | 62 | adantr 482 |
. . . . . . 7
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β (β‘(πΉ βf + πΊ) β {π§}) = βͺ
π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)}))) |
171 | 170 | fveq2d 6851 |
. . . . . 6
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β (πβ(β‘(πΉ βf + πΊ) β {π§})) = (πββͺ
π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})))) |
172 | | measbasedom 32841 |
. . . . . . . . 9
β’ (π β βͺ ran measures β π β (measuresβdom π)) |
173 | 16, 172 | sylib 217 |
. . . . . . . 8
β’ (π β π β (measuresβdom π)) |
174 | 173 | adantr 482 |
. . . . . . 7
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β π β (measuresβdom π)) |
175 | | eldifi 4091 |
. . . . . . . 8
β’ (π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)}) β π§ β ran (πΉ βf + πΊ)) |
176 | 175, 109 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β βπ β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})) β dom π) |
177 | 122 | adantr 482 |
. . . . . . 7
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) βΌ Ο) |
178 | | sneq 4601 |
. . . . . . . . . . 11
β’ (π₯ = (1st βπ) β {π₯} = {(1st βπ)}) |
179 | 178 | imaeq2d 6018 |
. . . . . . . . . 10
β’ (π₯ = (1st βπ) β (β‘πΉ β {π₯}) = (β‘πΉ β {(1st βπ)})) |
180 | | sneq 4601 |
. . . . . . . . . . 11
β’ (π¦ = (2nd βπ) β {π¦} = {(2nd βπ)}) |
181 | 180 | imaeq2d 6018 |
. . . . . . . . . 10
β’ (π¦ = (2nd βπ) β (β‘πΊ β {π¦}) = (β‘πΊ β {(2nd βπ)})) |
182 | 18 | ffund 6677 |
. . . . . . . . . . 11
β’ (π β Fun πΉ) |
183 | | sndisj 5101 |
. . . . . . . . . . 11
β’
Disj π₯ β
ran πΉ{π₯} |
184 | | disjpreima 31544 |
. . . . . . . . . . 11
β’ ((Fun
πΉ β§ Disj π₯ β ran πΉ{π₯}) β Disj π₯ β ran πΉ(β‘πΉ β {π₯})) |
185 | 182, 183,
184 | sylancl 587 |
. . . . . . . . . 10
β’ (π β Disj π₯ β ran πΉ(β‘πΉ β {π₯})) |
186 | 20 | ffund 6677 |
. . . . . . . . . . 11
β’ (π β Fun πΊ) |
187 | | sndisj 5101 |
. . . . . . . . . . 11
β’
Disj π¦ β
ran πΊ{π¦} |
188 | | disjpreima 31544 |
. . . . . . . . . . 11
β’ ((Fun
πΊ β§ Disj π¦ β ran πΊ{π¦}) β Disj π¦ β ran πΊ(β‘πΊ β {π¦})) |
189 | 186, 187,
188 | sylancl 587 |
. . . . . . . . . 10
β’ (π β Disj π¦ β ran πΊ(β‘πΊ β {π¦})) |
190 | 179, 181,
185, 189 | disjxpin 31548 |
. . . . . . . . 9
β’ (π β Disj π β (ran πΉ Γ ran πΊ)((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)}))) |
191 | | disjss1 5081 |
. . . . . . . . 9
β’ (((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) β (ran πΉ Γ ran πΊ) β (Disj π β (ran πΉ Γ ran πΊ)((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})) β Disj π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})))) |
192 | 114, 190,
191 | mpsyl 68 |
. . . . . . . 8
β’ (π β Disj π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)}))) |
193 | 192 | adantr 482 |
. . . . . . 7
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β Disj π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)}))) |
194 | | measvuni 32853 |
. . . . . . 7
β’ ((π β (measuresβdom
π) β§ βπ β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})) β dom π β§ (((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) βΌ Ο β§ Disj π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})))) β (πββͺ
π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)}))) = Ξ£*π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))(πβ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})))) |
195 | 174, 176,
177, 193, 194 | syl112anc 1375 |
. . . . . 6
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β (πββͺ
π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)}))) = Ξ£*π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))(πβ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})))) |
196 | | ssfi 9124 |
. . . . . . . . 9
β’ (((ran
πΉ Γ ran πΊ) β Fin β§ ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) β (ran πΉ Γ ran πΊ)) β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) β Fin) |
197 | 113, 114,
196 | sylancl 587 |
. . . . . . . 8
β’ (π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) β Fin) |
198 | 197 | adantr 482 |
. . . . . . 7
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) β Fin) |
199 | | simpll 766 |
. . . . . . . 8
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β π) |
200 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) |
201 | 114, 200 | sselid 3947 |
. . . . . . . . 9
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β π β (ran πΉ Γ ran πΊ)) |
202 | | xp1st 7958 |
. . . . . . . . 9
β’ (π β (ran πΉ Γ ran πΊ) β (1st βπ) β ran πΉ) |
203 | 201, 202 | syl 17 |
. . . . . . . 8
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β (1st βπ) β ran πΉ) |
204 | | xp2nd 7959 |
. . . . . . . . 9
β’ (π β (ran πΉ Γ ran πΊ) β (2nd βπ) β ran πΊ) |
205 | 201, 204 | syl 17 |
. . . . . . . 8
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β (2nd βπ) β ran πΊ) |
206 | | oveq12 7371 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ = 0 β§ π¦ = 0 ) β (π₯ + π¦) = ( 0 + 0 )) |
207 | | sibfof.5 |
. . . . . . . . . . . . . . . 16
β’ (π β ( 0 + 0 ) =
(0gβπΎ)) |
208 | 206, 207 | sylan9eqr 2799 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π₯ = 0 β§ π¦ = 0 )) β (π₯ + π¦) = (0gβπΎ)) |
209 | 208 | ex 414 |
. . . . . . . . . . . . . 14
β’ (π β ((π₯ = 0 β§ π¦ = 0 ) β (π₯ + π¦) = (0gβπΎ))) |
210 | 209 | necon3ad 2957 |
. . . . . . . . . . . . 13
β’ (π β ((π₯ + π¦) β (0gβπΎ) β Β¬ (π₯ = 0 β§ π¦ = 0 ))) |
211 | | neorian 3040 |
. . . . . . . . . . . . 13
β’ ((π₯ β 0 β¨ π¦ β 0 ) β Β¬ (π₯ = 0 β§ π¦ = 0 )) |
212 | 210, 211 | syl6ibr 252 |
. . . . . . . . . . . 12
β’ (π β ((π₯ + π¦) β (0gβπΎ) β (π₯ β 0 β¨ π¦ β 0 ))) |
213 | 212 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π₯ + π¦) β (0gβπΎ) β (π₯ β 0 β¨ π¦ β 0 ))) |
214 | 213 | ralrimivva 3198 |
. . . . . . . . . 10
β’ (π β βπ₯ β π΅ βπ¦ β π΅ ((π₯ + π¦) β (0gβπΎ) β (π₯ β 0 β¨ π¦ β 0 ))) |
215 | 199, 214 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β βπ₯ β π΅ βπ¦ β π΅ ((π₯ + π¦) β (0gβπΎ) β (π₯ β 0 β¨ π¦ β 0 ))) |
216 | 67 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ)) β (β‘ + β {π§})) |
217 | 216 | sselda 3949 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β π β (β‘ + β {π§})) |
218 | | fniniseg 7015 |
. . . . . . . . . . . . 13
β’ ( + Fn (π΅ Γ π΅) β (π β (β‘ + β {π§}) β (π β (π΅ Γ π΅) β§ ( + βπ) = π§))) |
219 | 199, 61, 218 | 3syl 18 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β (π β (β‘ + β {π§}) β (π β (π΅ Γ π΅) β§ ( + βπ) = π§))) |
220 | 217, 219 | mpbid 231 |
. . . . . . . . . . 11
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β (π β (π΅ Γ π΅) β§ ( + βπ) = π§)) |
221 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β (π΅ Γ π΅) β§ ( + βπ) = π§) β ( + βπ) = π§) |
222 | | 1st2nd2 7965 |
. . . . . . . . . . . . . . 15
β’ (π β (π΅ Γ π΅) β π = β¨(1st βπ), (2nd βπ)β©) |
223 | 222 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π β (π΅ Γ π΅) β ( + βπ) = ( +
ββ¨(1st βπ), (2nd βπ)β©)) |
224 | | df-ov 7365 |
. . . . . . . . . . . . . 14
β’
((1st βπ) + (2nd
βπ)) = ( +
ββ¨(1st βπ), (2nd βπ)β©) |
225 | 223, 224 | eqtr4di 2795 |
. . . . . . . . . . . . 13
β’ (π β (π΅ Γ π΅) β ( + βπ) = ((1st βπ) + (2nd
βπ))) |
226 | 225 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β (π΅ Γ π΅) β§ ( + βπ) = π§) β ( + βπ) = ((1st βπ) + (2nd
βπ))) |
227 | 221, 226 | eqtr3d 2779 |
. . . . . . . . . . 11
β’ ((π β (π΅ Γ π΅) β§ ( + βπ) = π§) β π§ = ((1st βπ) + (2nd
βπ))) |
228 | 220, 227 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β π§ = ((1st βπ) + (2nd
βπ))) |
229 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) |
230 | 229 | eldifbd 3928 |
. . . . . . . . . . 11
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β Β¬ π§ β {(0gβπΎ)}) |
231 | | velsn 4607 |
. . . . . . . . . . . 12
β’ (π§ β
{(0gβπΎ)}
β π§ =
(0gβπΎ)) |
232 | 231 | necon3bbii 2992 |
. . . . . . . . . . 11
β’ (Β¬
π§ β
{(0gβπΎ)}
β π§ β
(0gβπΎ)) |
233 | 230, 232 | sylib 217 |
. . . . . . . . . 10
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β π§ β (0gβπΎ)) |
234 | 228, 233 | eqnetrrd 3013 |
. . . . . . . . 9
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β ((1st βπ) + (2nd
βπ)) β
(0gβπΎ)) |
235 | 175, 72 | sylanl2 680 |
. . . . . . . . . . 11
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β π β (π΅ Γ π΅)) |
236 | 235, 85 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β (1st βπ) β π΅) |
237 | 235, 98 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β (2nd βπ) β π΅) |
238 | | oveq1 7369 |
. . . . . . . . . . . . 13
β’ (π₯ = (1st βπ) β (π₯ + π¦) = ((1st βπ) + π¦)) |
239 | 238 | neeq1d 3004 |
. . . . . . . . . . . 12
β’ (π₯ = (1st βπ) β ((π₯ + π¦) β (0gβπΎ) β ((1st βπ) + π¦) β (0gβπΎ))) |
240 | | neeq1 3007 |
. . . . . . . . . . . . 13
β’ (π₯ = (1st βπ) β (π₯ β 0 β (1st
βπ) β 0
)) |
241 | 240 | orbi1d 916 |
. . . . . . . . . . . 12
β’ (π₯ = (1st βπ) β ((π₯ β 0 β¨ π¦ β 0 ) β ((1st
βπ) β 0 β¨ π¦ β 0 ))) |
242 | 239, 241 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π₯ = (1st βπ) β (((π₯ + π¦) β (0gβπΎ) β (π₯ β 0 β¨ π¦ β 0 )) β
(((1st βπ)
+ π¦) β
(0gβπΎ)
β ((1st βπ) β 0 β¨ π¦ β 0 )))) |
243 | | oveq2 7370 |
. . . . . . . . . . . . 13
β’ (π¦ = (2nd βπ) β ((1st
βπ) + π¦) = ((1st
βπ) +
(2nd βπ))) |
244 | 243 | neeq1d 3004 |
. . . . . . . . . . . 12
β’ (π¦ = (2nd βπ) β (((1st
βπ) + π¦) β
(0gβπΎ)
β ((1st βπ) + (2nd
βπ)) β
(0gβπΎ))) |
245 | | neeq1 3007 |
. . . . . . . . . . . . 13
β’ (π¦ = (2nd βπ) β (π¦ β 0 β (2nd
βπ) β 0
)) |
246 | 245 | orbi2d 915 |
. . . . . . . . . . . 12
β’ (π¦ = (2nd βπ) β (((1st
βπ) β 0 β¨ π¦ β 0 ) β ((1st
βπ) β 0 β¨
(2nd βπ)
β 0
))) |
247 | 244, 246 | imbi12d 345 |
. . . . . . . . . . 11
β’ (π¦ = (2nd βπ) β ((((1st
βπ) + π¦) β
(0gβπΎ)
β ((1st βπ) β 0 β¨ π¦ β 0 )) β
(((1st βπ)
+
(2nd βπ))
β (0gβπΎ) β ((1st βπ) β 0 β¨ (2nd
βπ) β 0
)))) |
248 | 242, 247 | rspc2v 3593 |
. . . . . . . . . 10
β’
(((1st βπ) β π΅ β§ (2nd βπ) β π΅) β (βπ₯ β π΅ βπ¦ β π΅ ((π₯ + π¦) β (0gβπΎ) β (π₯ β 0 β¨ π¦ β 0 )) β
(((1st βπ)
+
(2nd βπ))
β (0gβπΎ) β ((1st βπ) β 0 β¨ (2nd
βπ) β 0
)))) |
249 | 236, 237,
248 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β (βπ₯ β π΅ βπ¦ β π΅ ((π₯ + π¦) β (0gβπΎ) β (π₯ β 0 β¨ π¦ β 0 )) β
(((1st βπ)
+
(2nd βπ))
β (0gβπΎ) β ((1st βπ) β 0 β¨ (2nd
βπ) β 0
)))) |
250 | 215, 234,
249 | mp2d 49 |
. . . . . . . 8
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β ((1st βπ) β 0 β¨ (2nd
βπ) β 0
)) |
251 | 3, 4, 11, 12, 13, 14, 15, 16, 17, 19, 2, 74 | sibfinima 32979 |
. . . . . . . 8
β’ (((π β§ (1st
βπ) β ran πΉ β§ (2nd
βπ) β ran πΊ) β§ ((1st
βπ) β 0 β¨
(2nd βπ)
β 0 ))
β (πβ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)}))) β
(0[,)+β)) |
252 | 199, 203,
205, 250, 251 | syl31anc 1374 |
. . . . . . 7
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β (πβ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)}))) β
(0[,)+β)) |
253 | 198, 252 | esumpfinval 32714 |
. . . . . 6
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β
Ξ£*π β
((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))(πβ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)}))) = Ξ£π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))(πβ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})))) |
254 | 171, 195,
253 | 3eqtrd 2781 |
. . . . 5
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β (πβ(β‘(πΉ βf + πΊ) β {π§})) = Ξ£π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))(πβ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})))) |
255 | | rge0ssre 13380 |
. . . . . . 7
β’
(0[,)+β) β β |
256 | 255, 252 | sselid 3947 |
. . . . . 6
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β (πβ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)}))) β
β) |
257 | 198, 256 | fsumrecl 15626 |
. . . . 5
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β Ξ£π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))(πβ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)}))) β
β) |
258 | 254, 257 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β (πβ(β‘(πΉ βf + πΊ) β {π§})) β β) |
259 | 174 | adantr 482 |
. . . . . . 7
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β π β (measuresβdom π)) |
260 | 175, 108 | sylanl2 680 |
. . . . . . 7
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})) β dom π) |
261 | | measge0 32846 |
. . . . . . 7
β’ ((π β (measuresβdom
π) β§ ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})) β dom π) β 0 β€ (πβ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})))) |
262 | 259, 260,
261 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β§ π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))) β 0 β€ (πβ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})))) |
263 | 198, 256,
262 | fsumge0 15687 |
. . . . 5
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β 0 β€ Ξ£π β ((β‘ + β {π§}) β© (ran πΉ Γ ran πΊ))(πβ((β‘πΉ β {(1st βπ)}) β© (β‘πΊ β {(2nd βπ)})))) |
264 | 263, 254 | breqtrrd 5138 |
. . . 4
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β 0 β€ (πβ(β‘(πΉ βf + πΊ) β {π§}))) |
265 | | elrege0 13378 |
. . . 4
β’ ((πβ(β‘(πΉ βf + πΊ) β {π§})) β (0[,)+β) β ((πβ(β‘(πΉ βf + πΊ) β {π§})) β β β§ 0 β€ (πβ(β‘(πΉ βf + πΊ) β {π§})))) |
266 | 258, 264,
265 | sylanbrc 584 |
. . 3
β’ ((π β§ π§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})) β (πβ(β‘(πΉ βf + πΊ) β {π§})) β (0[,)+β)) |
267 | 266 | ralrimiva 3144 |
. 2
β’ (π β βπ§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})(πβ(β‘(πΉ βf + πΊ) β {π§})) β (0[,)+β)) |
268 | | eqid 2737 |
. . 3
β’
(sigaGenβ(TopOpenβπΎ)) = (sigaGenβ(TopOpenβπΎ)) |
269 | | eqid 2737 |
. . 3
β’
(0gβπΎ) = (0gβπΎ) |
270 | | eqid 2737 |
. . 3
β’ (
Β·π βπΎ) = ( Β·π
βπΎ) |
271 | | eqid 2737 |
. . 3
β’
(βHomβ(ScalarβπΎ)) = (βHomβ(ScalarβπΎ)) |
272 | 27, 28, 268, 269, 270, 271, 26, 16 | issibf 32973 |
. 2
β’ (π β ((πΉ βf + πΊ) β dom (πΎsitgπ) β ((πΉ βf + πΊ) β (dom πMblFnM(sigaGenβ(TopOpenβπΎ))) β§ ran (πΉ βf + πΊ) β Fin β§ βπ§ β (ran (πΉ βf + πΊ) β {(0gβπΎ)})(πβ(β‘(πΉ βf + πΊ) β {π§})) β (0[,)+β)))) |
273 | 169, 137,
267, 272 | mpbir3and 1343 |
1
β’ (π β (πΉ βf + πΊ) β dom (πΎsitgπ)) |