Metamath Proof Explorer

Theorem sibfof

Description: Applying function operations on simple functions results in simple functions with regard to the destination space, provided the operation fulfills a simple condition. (Contributed by Thierry Arnoux, 12-Mar-2018)

Ref Expression
Hypotheses sitgval.b 
|- B = ( Base ` W )
sitgval.j 
|- J = ( TopOpen ` W )
sitgval.s 
|- S = ( sigaGen ` J )
sitgval.0 
|- .0. = ( 0g ` W )
sitgval.x 
|- .x. = ( .s ` W )
sitgval.h 
|- H = ( RRHom ` ( Scalar ` W ) )
sitgval.1 
|- ( ph -> W e. V )
sitgval.2 
|- ( ph -> M e. U. ran measures )
sibfmbl.1 
|- ( ph -> F e. dom ( W sitg M ) )
sibfof.c 
|- C = ( Base ` K )
sibfof.0 
|- ( ph -> W e. TopSp )
sibfof.1 
|- ( ph -> .+ : ( B X. B ) --> C )
sibfof.2 
|- ( ph -> G e. dom ( W sitg M ) )
sibfof.3 
|- ( ph -> K e. TopSp )
sibfof.4 
|- ( ph -> J e. Fre )
sibfof.5 
|- ( ph -> ( .0. .+ .0. ) = ( 0g ` K ) )
Assertion sibfof 
|- ( ph -> ( F oF .+ G ) e. dom ( K sitg M ) )

Proof

Step Hyp Ref Expression
1 sitgval.b 
 |-  B = ( Base ` W )
2 sitgval.j 
 |-  J = ( TopOpen ` W )
3 sitgval.s 
 |-  S = ( sigaGen ` J )
4 sitgval.0 
 |-  .0. = ( 0g ` W )
5 sitgval.x 
 |-  .x. = ( .s ` W )
6 sitgval.h 
 |-  H = ( RRHom ` ( Scalar ` W ) )
7 sitgval.1 
 |-  ( ph -> W e. V )
8 sitgval.2 
 |-  ( ph -> M e. U. ran measures )
9 sibfmbl.1 
 |-  ( ph -> F e. dom ( W sitg M ) )
10 sibfof.c 
 |-  C = ( Base ` K )
11 sibfof.0 
 |-  ( ph -> W e. TopSp )
12 sibfof.1 
 |-  ( ph -> .+ : ( B X. B ) --> C )
13 sibfof.2 
 |-  ( ph -> G e. dom ( W sitg M ) )
14 sibfof.3 
 |-  ( ph -> K e. TopSp )
15 sibfof.4 
 |-  ( ph -> J e. Fre )
16 sibfof.5 
 |-  ( ph -> ( .0. .+ .0. ) = ( 0g ` K ) )
17 1 2 tpsuni 
 |-  ( W e. TopSp -> B = U. J )
18 11 17 syl 
 |-  ( ph -> B = U. J )
19 18 sqxpeqd 
 |-  ( ph -> ( B X. B ) = ( U. J X. U. J ) )
20 19 feq2d 
 |-  ( ph -> ( .+ : ( B X. B ) --> C <-> .+ : ( U. J X. U. J ) --> C ) )
21 12 20 mpbid 
 |-  ( ph -> .+ : ( U. J X. U. J ) --> C )
22 21 fovcdmda 
 |-  ( ( ph /\ ( z e. U. J /\ x e. U. J ) ) -> ( z .+ x ) e. C )
23 1 2 3 4 5 6 7 8 9 sibff 
 |-  ( ph -> F : U. dom M --> U. J )
24 1 2 3 4 5 6 7 8 13 sibff 
 |-  ( ph -> G : U. dom M --> U. J )
25 dmexg 
 |-  ( M e. U. ran measures -> dom M e. _V )
26 uniexg 
 |-  ( dom M e. _V -> U. dom M e. _V )
27 8 25 26 3syl 
 |-  ( ph -> U. dom M e. _V )
28 inidm 
 |-  ( U. dom M i^i U. dom M ) = U. dom M
29 22 23 24 27 27 28 off 
 |-  ( ph -> ( F oF .+ G ) : U. dom M --> C )
30 eqid 
 |-  ( TopOpen ` K ) = ( TopOpen ` K )
31 10 30 tpsuni 
 |-  ( K e. TopSp -> C = U. ( TopOpen ` K ) )
32 14 31 syl 
 |-  ( ph -> C = U. ( TopOpen ` K ) )
33 fvex 
 |-  ( TopOpen ` K ) e. _V
34 unisg 
 |-  ( ( TopOpen ` K ) e. _V -> U. ( sigaGen ` ( TopOpen ` K ) ) = U. ( TopOpen ` K ) )
35 33 34 ax-mp 
 |-  U. ( sigaGen ` ( TopOpen ` K ) ) = U. ( TopOpen ` K )
36 32 35 eqtr4di 
 |-  ( ph -> C = U. ( sigaGen ` ( TopOpen ` K ) ) )
37 36 feq3d 
 |-  ( ph -> ( ( F oF .+ G ) : U. dom M --> C <-> ( F oF .+ G ) : U. dom M --> U. ( sigaGen ` ( TopOpen ` K ) ) ) )
38 29 37 mpbid 
 |-  ( ph -> ( F oF .+ G ) : U. dom M --> U. ( sigaGen ` ( TopOpen ` K ) ) )
39 33 a1i 
 |-  ( ph -> ( TopOpen ` K ) e. _V )
40 39 sgsiga 
 |-  ( ph -> ( sigaGen ` ( TopOpen ` K ) ) e. U. ran sigAlgebra )
41 40 uniexd 
 |-  ( ph -> U. ( sigaGen ` ( TopOpen ` K ) ) e. _V )
42 41 27 elmapd 
 |-  ( ph -> ( ( F oF .+ G ) e. ( U. ( sigaGen ` ( TopOpen ` K ) ) ^m U. dom M ) <-> ( F oF .+ G ) : U. dom M --> U. ( sigaGen ` ( TopOpen ` K ) ) ) )
43 38 42 mpbird 
 |-  ( ph -> ( F oF .+ G ) e. ( U. ( sigaGen ` ( TopOpen ` K ) ) ^m U. dom M ) )
44 inundif 
 |-  ( ( b i^i ran ( F oF .+ G ) ) u. ( b \ ran ( F oF .+ G ) ) ) = b
45 44 imaeq2i 
 |-  ( `' ( F oF .+ G ) " ( ( b i^i ran ( F oF .+ G ) ) u. ( b \ ran ( F oF .+ G ) ) ) ) = ( `' ( F oF .+ G ) " b )
46 ffun 
 |-  ( ( F oF .+ G ) : U. dom M --> C -> Fun ( F oF .+ G ) )
47 unpreima 
 |-  ( Fun ( F oF .+ G ) -> ( `' ( F oF .+ G ) " ( ( b i^i ran ( F oF .+ G ) ) u. ( b \ ran ( F oF .+ G ) ) ) ) = ( ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) u. ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) ) )
48 29 46 47 3syl 
 |-  ( ph -> ( `' ( F oF .+ G ) " ( ( b i^i ran ( F oF .+ G ) ) u. ( b \ ran ( F oF .+ G ) ) ) ) = ( ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) u. ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) ) )
49 48 adantr 
 |-  ( ( ph /\ b e. ( sigaGen ` ( TopOpen ` K ) ) ) -> ( `' ( F oF .+ G ) " ( ( b i^i ran ( F oF .+ G ) ) u. ( b \ ran ( F oF .+ G ) ) ) ) = ( ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) u. ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) ) )
50 45 49 eqtr3id 
 |-  ( ( ph /\ b e. ( sigaGen ` ( TopOpen ` K ) ) ) -> ( `' ( F oF .+ G ) " b ) = ( ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) u. ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) ) )
51 dmmeas 
 |-  ( M e. U. ran measures -> dom M e. U. ran sigAlgebra )
52 8 51 syl 
 |-  ( ph -> dom M e. U. ran sigAlgebra )
53 52 adantr 
 |-  ( ( ph /\ b e. ( sigaGen ` ( TopOpen ` K ) ) ) -> dom M e. U. ran sigAlgebra )
54 imaiun 
 |-  ( `' ( F oF .+ G ) " U_ z e. ( b i^i ran ( F oF .+ G ) ) { z } ) = U_ z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } )
55 iunid 
 |-  U_ z e. ( b i^i ran ( F oF .+ G ) ) { z } = ( b i^i ran ( F oF .+ G ) )
56 55 imaeq2i 
 |-  ( `' ( F oF .+ G ) " U_ z e. ( b i^i ran ( F oF .+ G ) ) { z } ) = ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) )
57 54 56 eqtr3i 
 |-  U_ z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) = ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) )
58 inss2 
 |-  ( b i^i ran ( F oF .+ G ) ) C_ ran ( F oF .+ G )
59 18 feq3d 
 |-  ( ph -> ( F : U. dom M --> B <-> F : U. dom M --> U. J ) )
60 23 59 mpbird 
 |-  ( ph -> F : U. dom M --> B )
61 18 feq3d 
 |-  ( ph -> ( G : U. dom M --> B <-> G : U. dom M --> U. J ) )
62 24 61 mpbird 
 |-  ( ph -> G : U. dom M --> B )
63 12 ffnd 
 |-  ( ph -> .+ Fn ( B X. B ) )
64 60 62 27 63 ofpreima2 
 |-  ( ph -> ( `' ( F oF .+ G ) " { z } ) = U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
65 64 adantr 
 |-  ( ( ph /\ z e. ran ( F oF .+ G ) ) -> ( `' ( F oF .+ G ) " { z } ) = U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
66 52 adantr 
 |-  ( ( ph /\ z e. ran ( F oF .+ G ) ) -> dom M e. U. ran sigAlgebra )
67 52 ad2antrr 
 |-  ( ( ( ph /\ z e. ran ( F oF .+ G ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> dom M e. U. ran sigAlgebra )
68 simpll 
 |-  ( ( ( ph /\ z e. ran ( F oF .+ G ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ph )
69 inss1 
 |-  ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) C_ ( `' .+ " { z } )
70 cnvimass 
 |-  ( `' .+ " { z } ) C_ dom .+
71 70 12 fssdm 
 |-  ( ph -> ( `' .+ " { z } ) C_ ( B X. B ) )
72 71 adantr 
 |-  ( ( ph /\ z e. ran ( F oF .+ G ) ) -> ( `' .+ " { z } ) C_ ( B X. B ) )
73 69 72 sstrid 
 |-  ( ( ph /\ z e. ran ( F oF .+ G ) ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) C_ ( B X. B ) )
74 73 sselda 
 |-  ( ( ( ph /\ z e. ran ( F oF .+ G ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> p e. ( B X. B ) )
75 52 adantr 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> dom M e. U. ran sigAlgebra )
76 15 sgsiga 
 |-  ( ph -> ( sigaGen ` J ) e. U. ran sigAlgebra )
77 3 76 eqeltrid 
 |-  ( ph -> S e. U. ran sigAlgebra )
78 77 adantr 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> S e. U. ran sigAlgebra )
79 1 2 3 4 5 6 7 8 9 sibfmbl 
 |-  ( ph -> F e. ( dom M MblFnM S ) )
80 79 adantr 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> F e. ( dom M MblFnM S ) )
81 2 tpstop 
 |-  ( W e. TopSp -> J e. Top )
82 cldssbrsiga 
 |-  ( J e. Top -> ( Clsd ` J ) C_ ( sigaGen ` J ) )
83 11 81 82 3syl 
 |-  ( ph -> ( Clsd ` J ) C_ ( sigaGen ` J ) )
84 83 adantr 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> ( Clsd ` J ) C_ ( sigaGen ` J ) )
85 15 adantr 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> J e. Fre )
86 xp1st 
 |-  ( p e. ( B X. B ) -> ( 1st ` p ) e. B )
87 86 adantl 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> ( 1st ` p ) e. B )
88 18 adantr 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> B = U. J )
89 87 88 eleqtrd 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> ( 1st ` p ) e. U. J )
90 eqid 
 |-  U. J = U. J
91 90 t1sncld 
 |-  ( ( J e. Fre /\ ( 1st ` p ) e. U. J ) -> { ( 1st ` p ) } e. ( Clsd ` J ) )
92 85 89 91 syl2anc 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> { ( 1st ` p ) } e. ( Clsd ` J ) )
93 84 92 sseldd 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> { ( 1st ` p ) } e. ( sigaGen ` J ) )
94 93 3 eleqtrrdi 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> { ( 1st ` p ) } e. S )
95 75 78 80 94 mbfmcnvima 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> ( `' F " { ( 1st ` p ) } ) e. dom M )
96 68 74 95 syl2anc 
 |-  ( ( ( ph /\ z e. ran ( F oF .+ G ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( `' F " { ( 1st ` p ) } ) e. dom M )
97 1 2 3 4 5 6 7 8 13 sibfmbl 
 |-  ( ph -> G e. ( dom M MblFnM S ) )
98 97 adantr 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> G e. ( dom M MblFnM S ) )
99 xp2nd 
 |-  ( p e. ( B X. B ) -> ( 2nd ` p ) e. B )
100 99 adantl 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> ( 2nd ` p ) e. B )
101 100 88 eleqtrd 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> ( 2nd ` p ) e. U. J )
102 90 t1sncld 
 |-  ( ( J e. Fre /\ ( 2nd ` p ) e. U. J ) -> { ( 2nd ` p ) } e. ( Clsd ` J ) )
103 85 101 102 syl2anc 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> { ( 2nd ` p ) } e. ( Clsd ` J ) )
104 84 103 sseldd 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> { ( 2nd ` p ) } e. ( sigaGen ` J ) )
105 104 3 eleqtrrdi 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> { ( 2nd ` p ) } e. S )
106 75 78 98 105 mbfmcnvima 
 |-  ( ( ph /\ p e. ( B X. B ) ) -> ( `' G " { ( 2nd ` p ) } ) e. dom M )
107 68 74 106 syl2anc 
 |-  ( ( ( ph /\ z e. ran ( F oF .+ G ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( `' G " { ( 2nd ` p ) } ) e. dom M )
108 inelsiga 
 |-  ( ( dom M e. U. ran sigAlgebra /\ ( `' F " { ( 1st ` p ) } ) e. dom M /\ ( `' G " { ( 2nd ` p ) } ) e. dom M ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M )
109 67 96 107 108 syl3anc 
 |-  ( ( ( ph /\ z e. ran ( F oF .+ G ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M )
110 109 ralrimiva 
 |-  ( ( ph /\ z e. ran ( F oF .+ G ) ) -> A. p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M )
111 1 2 3 4 5 6 7 8 9 sibfrn 
 |-  ( ph -> ran F e. Fin )
112 1 2 3 4 5 6 7 8 13 sibfrn 
 |-  ( ph -> ran G e. Fin )
113 xpfi 
 |-  ( ( ran F e. Fin /\ ran G e. Fin ) -> ( ran F X. ran G ) e. Fin )
114 111 112 113 syl2anc 
 |-  ( ph -> ( ran F X. ran G ) e. Fin )
115 inss2 
 |-  ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) C_ ( ran F X. ran G )
116 ssdomg 
 |-  ( ( ran F X. ran G ) e. Fin -> ( ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) C_ ( ran F X. ran G ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ ( ran F X. ran G ) ) )
117 114 115 116 mpisyl 
 |-  ( ph -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ ( ran F X. ran G ) )
118 isfinite 
 |-  ( ( ran F X. ran G ) e. Fin <-> ( ran F X. ran G ) ~< _om )
119 118 biimpi 
 |-  ( ( ran F X. ran G ) e. Fin -> ( ran F X. ran G ) ~< _om )
120 sdomdom 
 |-  ( ( ran F X. ran G ) ~< _om -> ( ran F X. ran G ) ~<_ _om )
121 114 119 120 3syl 
 |-  ( ph -> ( ran F X. ran G ) ~<_ _om )
122 domtr 
 |-  ( ( ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ ( ran F X. ran G ) /\ ( ran F X. ran G ) ~<_ _om ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ _om )
123 117 121 122 syl2anc 
 |-  ( ph -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ _om )
124 123 adantr 
 |-  ( ( ph /\ z e. ran ( F oF .+ G ) ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ _om )
125 nfcv 
 |-  F/_ p ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) )
126 125 sigaclcuni 
 |-  ( ( dom M e. U. ran sigAlgebra /\ A. p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M /\ ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ _om ) -> U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M )
127 66 110 124 126 syl3anc 
 |-  ( ( ph /\ z e. ran ( F oF .+ G ) ) -> U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M )
128 65 127 eqeltrd 
 |-  ( ( ph /\ z e. ran ( F oF .+ G ) ) -> ( `' ( F oF .+ G ) " { z } ) e. dom M )
129 128 ralrimiva 
 |-  ( ph -> A. z e. ran ( F oF .+ G ) ( `' ( F oF .+ G ) " { z } ) e. dom M )
130 ssralv 
 |-  ( ( b i^i ran ( F oF .+ G ) ) C_ ran ( F oF .+ G ) -> ( A. z e. ran ( F oF .+ G ) ( `' ( F oF .+ G ) " { z } ) e. dom M -> A. z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) e. dom M ) )
131 58 129 130 mpsyl 
 |-  ( ph -> A. z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) e. dom M )
132 131 adantr 
 |-  ( ( ph /\ b e. ( sigaGen ` ( TopOpen ` K ) ) ) -> A. z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) e. dom M )
133 12 ffund 
 |-  ( ph -> Fun .+ )
134 imafi 
 |-  ( ( Fun .+ /\ ( ran F X. ran G ) e. Fin ) -> ( .+ " ( ran F X. ran G ) ) e. Fin )
135 133 114 134 syl2anc 
 |-  ( ph -> ( .+ " ( ran F X. ran G ) ) e. Fin )
136 23 24 21 27 ofrn2 
 |-  ( ph -> ran ( F oF .+ G ) C_ ( .+ " ( ran F X. ran G ) ) )
137 ssfi 
 |-  ( ( ( .+ " ( ran F X. ran G ) ) e. Fin /\ ran ( F oF .+ G ) C_ ( .+ " ( ran F X. ran G ) ) ) -> ran ( F oF .+ G ) e. Fin )
138 135 136 137 syl2anc 
 |-  ( ph -> ran ( F oF .+ G ) e. Fin )
139 ssdomg 
 |-  ( ran ( F oF .+ G ) e. Fin -> ( ( b i^i ran ( F oF .+ G ) ) C_ ran ( F oF .+ G ) -> ( b i^i ran ( F oF .+ G ) ) ~<_ ran ( F oF .+ G ) ) )
140 138 58 139 mpisyl 
 |-  ( ph -> ( b i^i ran ( F oF .+ G ) ) ~<_ ran ( F oF .+ G ) )
141 isfinite 
 |-  ( ran ( F oF .+ G ) e. Fin <-> ran ( F oF .+ G ) ~< _om )
142 138 141 sylib 
 |-  ( ph -> ran ( F oF .+ G ) ~< _om )
143 sdomdom 
 |-  ( ran ( F oF .+ G ) ~< _om -> ran ( F oF .+ G ) ~<_ _om )
144 142 143 syl 
 |-  ( ph -> ran ( F oF .+ G ) ~<_ _om )
145 domtr 
 |-  ( ( ( b i^i ran ( F oF .+ G ) ) ~<_ ran ( F oF .+ G ) /\ ran ( F oF .+ G ) ~<_ _om ) -> ( b i^i ran ( F oF .+ G ) ) ~<_ _om )
146 140 144 145 syl2anc 
 |-  ( ph -> ( b i^i ran ( F oF .+ G ) ) ~<_ _om )
147 146 adantr 
 |-  ( ( ph /\ b e. ( sigaGen ` ( TopOpen ` K ) ) ) -> ( b i^i ran ( F oF .+ G ) ) ~<_ _om )
148 nfcv 
 |-  F/_ z ( b i^i ran ( F oF .+ G ) )
149 148 sigaclcuni 
 |-  ( ( dom M e. U. ran sigAlgebra /\ A. z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) e. dom M /\ ( b i^i ran ( F oF .+ G ) ) ~<_ _om ) -> U_ z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) e. dom M )
150 53 132 147 149 syl3anc 
 |-  ( ( ph /\ b e. ( sigaGen ` ( TopOpen ` K ) ) ) -> U_ z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) e. dom M )
151 57 150 eqeltrrid 
 |-  ( ( ph /\ b e. ( sigaGen ` ( TopOpen ` K ) ) ) -> ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) e. dom M )
152 difpreima 
 |-  ( Fun ( F oF .+ G ) -> ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) = ( ( `' ( F oF .+ G ) " b ) \ ( `' ( F oF .+ G ) " ran ( F oF .+ G ) ) ) )
153 29 46 152 3syl 
 |-  ( ph -> ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) = ( ( `' ( F oF .+ G ) " b ) \ ( `' ( F oF .+ G ) " ran ( F oF .+ G ) ) ) )
154 cnvimarndm 
 |-  ( `' ( F oF .+ G ) " ran ( F oF .+ G ) ) = dom ( F oF .+ G )
155 154 difeq2i 
 |-  ( ( `' ( F oF .+ G ) " b ) \ ( `' ( F oF .+ G ) " ran ( F oF .+ G ) ) ) = ( ( `' ( F oF .+ G ) " b ) \ dom ( F oF .+ G ) )
156 cnvimass 
 |-  ( `' ( F oF .+ G ) " b ) C_ dom ( F oF .+ G )
157 ssdif0 
 |-  ( ( `' ( F oF .+ G ) " b ) C_ dom ( F oF .+ G ) <-> ( ( `' ( F oF .+ G ) " b ) \ dom ( F oF .+ G ) ) = (/) )
158 156 157 mpbi 
 |-  ( ( `' ( F oF .+ G ) " b ) \ dom ( F oF .+ G ) ) = (/)
159 155 158 eqtri 
 |-  ( ( `' ( F oF .+ G ) " b ) \ ( `' ( F oF .+ G ) " ran ( F oF .+ G ) ) ) = (/)
160 153 159 eqtrdi 
 |-  ( ph -> ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) = (/) )
161 0elsiga 
 |-  ( dom M e. U. ran sigAlgebra -> (/) e. dom M )
162 8 51 161 3syl 
 |-  ( ph -> (/) e. dom M )
163 160 162 eqeltrd 
 |-  ( ph -> ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) e. dom M )
164 163 adantr 
 |-  ( ( ph /\ b e. ( sigaGen ` ( TopOpen ` K ) ) ) -> ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) e. dom M )
165 unelsiga 
 |-  ( ( dom M e. U. ran sigAlgebra /\ ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) e. dom M /\ ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) e. dom M ) -> ( ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) u. ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) ) e. dom M )
166 53 151 164 165 syl3anc 
 |-  ( ( ph /\ b e. ( sigaGen ` ( TopOpen ` K ) ) ) -> ( ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) u. ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) ) e. dom M )
167 50 166 eqeltrd 
 |-  ( ( ph /\ b e. ( sigaGen ` ( TopOpen ` K ) ) ) -> ( `' ( F oF .+ G ) " b ) e. dom M )
168 167 ralrimiva 
 |-  ( ph -> A. b e. ( sigaGen ` ( TopOpen ` K ) ) ( `' ( F oF .+ G ) " b ) e. dom M )
169 52 40 ismbfm 
 |-  ( ph -> ( ( F oF .+ G ) e. ( dom M MblFnM ( sigaGen ` ( TopOpen ` K ) ) ) <-> ( ( F oF .+ G ) e. ( U. ( sigaGen ` ( TopOpen ` K ) ) ^m U. dom M ) /\ A. b e. ( sigaGen ` ( TopOpen ` K ) ) ( `' ( F oF .+ G ) " b ) e. dom M ) ) )
170 43 168 169 mpbir2and 
 |-  ( ph -> ( F oF .+ G ) e. ( dom M MblFnM ( sigaGen ` ( TopOpen ` K ) ) ) )
171 64 adantr 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( `' ( F oF .+ G ) " { z } ) = U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
172 171 fveq2d 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( M ` ( `' ( F oF .+ G ) " { z } ) ) = ( M ` U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
173 measbasedom 
 |-  ( M e. U. ran measures <-> M e. ( measures ` dom M ) )
174 8 173 sylib 
 |-  ( ph -> M e. ( measures ` dom M ) )
175 174 adantr 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> M e. ( measures ` dom M ) )
176 eldifi 
 |-  ( z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) -> z e. ran ( F oF .+ G ) )
177 176 110 sylan2 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> A. p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M )
178 123 adantr 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ _om )
179 sneq 
 |-  ( x = ( 1st ` p ) -> { x } = { ( 1st ` p ) } )
180 179 imaeq2d 
 |-  ( x = ( 1st ` p ) -> ( `' F " { x } ) = ( `' F " { ( 1st ` p ) } ) )
181 sneq 
 |-  ( y = ( 2nd ` p ) -> { y } = { ( 2nd ` p ) } )
182 181 imaeq2d 
 |-  ( y = ( 2nd ` p ) -> ( `' G " { y } ) = ( `' G " { ( 2nd ` p ) } ) )
183 23 ffund 
 |-  ( ph -> Fun F )
184 sndisj 
 |-  Disj_ x e. ran F { x }
185 disjpreima 
 |-  ( ( Fun F /\ Disj_ x e. ran F { x } ) -> Disj_ x e. ran F ( `' F " { x } ) )
186 183 184 185 sylancl 
 |-  ( ph -> Disj_ x e. ran F ( `' F " { x } ) )
187 24 ffund 
 |-  ( ph -> Fun G )
188 sndisj 
 |-  Disj_ y e. ran G { y }
189 disjpreima 
 |-  ( ( Fun G /\ Disj_ y e. ran G { y } ) -> Disj_ y e. ran G ( `' G " { y } ) )
190 187 188 189 sylancl 
 |-  ( ph -> Disj_ y e. ran G ( `' G " { y } ) )
191 180 182 186 190 disjxpin 
 |-  ( ph -> Disj_ p e. ( ran F X. ran G ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
192 disjss1 
 |-  ( ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) C_ ( ran F X. ran G ) -> ( Disj_ p e. ( ran F X. ran G ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) -> Disj_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
193 115 191 192 mpsyl 
 |-  ( ph -> Disj_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
194 193 adantr 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> Disj_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
195 measvuni 
 |-  ( ( M e. ( measures ` dom M ) /\ A. p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M /\ ( ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ _om /\ Disj_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) ) -> ( M ` U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) = sum* p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
196 175 177 178 194 195 syl112anc 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( M ` U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) = sum* p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
197 ssfi 
 |-  ( ( ( ran F X. ran G ) e. Fin /\ ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) C_ ( ran F X. ran G ) ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) e. Fin )
198 114 115 197 sylancl 
 |-  ( ph -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) e. Fin )
199 198 adantr 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) e. Fin )
200 simpll 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ph )
201 simpr 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) )
202 115 201 sselid 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> p e. ( ran F X. ran G ) )
203 xp1st 
 |-  ( p e. ( ran F X. ran G ) -> ( 1st ` p ) e. ran F )
204 202 203 syl 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( 1st ` p ) e. ran F )
205 xp2nd 
 |-  ( p e. ( ran F X. ran G ) -> ( 2nd ` p ) e. ran G )
206 202 205 syl 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( 2nd ` p ) e. ran G )
207 oveq12 
 |-  ( ( x = .0. /\ y = .0. ) -> ( x .+ y ) = ( .0. .+ .0. ) )
208 207 16 sylan9eqr 
 |-  ( ( ph /\ ( x = .0. /\ y = .0. ) ) -> ( x .+ y ) = ( 0g ` K ) )
209 208 ex 
 |-  ( ph -> ( ( x = .0. /\ y = .0. ) -> ( x .+ y ) = ( 0g ` K ) ) )
210 209 necon3ad 
 |-  ( ph -> ( ( x .+ y ) =/= ( 0g ` K ) -> -. ( x = .0. /\ y = .0. ) ) )
211 neorian 
 |-  ( ( x =/= .0. \/ y =/= .0. ) <-> -. ( x = .0. /\ y = .0. ) )
212 210 211 imbitrrdi 
 |-  ( ph -> ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) )
213 212 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) )
214 213 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) )
215 200 214 syl 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> A. x e. B A. y e. B ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) )
216 69 a1i 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) C_ ( `' .+ " { z } ) )
217 216 sselda 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> p e. ( `' .+ " { z } ) )
218 fniniseg 
 |-  ( .+ Fn ( B X. B ) -> ( p e. ( `' .+ " { z } ) <-> ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) ) )
219 200 63 218 3syl 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( p e. ( `' .+ " { z } ) <-> ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) ) )
220 217 219 mpbid 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) )
221 simpr 
 |-  ( ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) -> ( .+ ` p ) = z )
222 1st2nd2 
 |-  ( p e. ( B X. B ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
223 222 fveq2d 
 |-  ( p e. ( B X. B ) -> ( .+ ` p ) = ( .+ ` <. ( 1st ` p ) , ( 2nd ` p ) >. ) )
224 df-ov 
 |-  ( ( 1st ` p ) .+ ( 2nd ` p ) ) = ( .+ ` <. ( 1st ` p ) , ( 2nd ` p ) >. )
225 223 224 eqtr4di 
 |-  ( p e. ( B X. B ) -> ( .+ ` p ) = ( ( 1st ` p ) .+ ( 2nd ` p ) ) )
226 225 adantr 
 |-  ( ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) -> ( .+ ` p ) = ( ( 1st ` p ) .+ ( 2nd ` p ) ) )
227 221 226 eqtr3d 
 |-  ( ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) -> z = ( ( 1st ` p ) .+ ( 2nd ` p ) ) )
228 220 227 syl 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> z = ( ( 1st ` p ) .+ ( 2nd ` p ) ) )
229 simplr 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) )
230 229 eldifbd 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> -. z e. { ( 0g ` K ) } )
231 velsn 
 |-  ( z e. { ( 0g ` K ) } <-> z = ( 0g ` K ) )
232 231 necon3bbii 
 |-  ( -. z e. { ( 0g ` K ) } <-> z =/= ( 0g ` K ) )
233 230 232 sylib 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> z =/= ( 0g ` K ) )
234 228 233 eqnetrrd 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( ( 1st ` p ) .+ ( 2nd ` p ) ) =/= ( 0g ` K ) )
235 176 74 sylanl2 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> p e. ( B X. B ) )
236 235 86 syl 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( 1st ` p ) e. B )
237 235 99 syl 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( 2nd ` p ) e. B )
238 oveq1 
 |-  ( x = ( 1st ` p ) -> ( x .+ y ) = ( ( 1st ` p ) .+ y ) )
239 238 neeq1d 
 |-  ( x = ( 1st ` p ) -> ( ( x .+ y ) =/= ( 0g ` K ) <-> ( ( 1st ` p ) .+ y ) =/= ( 0g ` K ) ) )
240 neeq1 
 |-  ( x = ( 1st ` p ) -> ( x =/= .0. <-> ( 1st ` p ) =/= .0. ) )
241 240 orbi1d 
 |-  ( x = ( 1st ` p ) -> ( ( x =/= .0. \/ y =/= .0. ) <-> ( ( 1st ` p ) =/= .0. \/ y =/= .0. ) ) )
242 239 241 imbi12d 
 |-  ( x = ( 1st ` p ) -> ( ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) <-> ( ( ( 1st ` p ) .+ y ) =/= ( 0g ` K ) -> ( ( 1st ` p ) =/= .0. \/ y =/= .0. ) ) ) )
243 oveq2 
 |-  ( y = ( 2nd ` p ) -> ( ( 1st ` p ) .+ y ) = ( ( 1st ` p ) .+ ( 2nd ` p ) ) )
244 243 neeq1d 
 |-  ( y = ( 2nd ` p ) -> ( ( ( 1st ` p ) .+ y ) =/= ( 0g ` K ) <-> ( ( 1st ` p ) .+ ( 2nd ` p ) ) =/= ( 0g ` K ) ) )
245 neeq1 
 |-  ( y = ( 2nd ` p ) -> ( y =/= .0. <-> ( 2nd ` p ) =/= .0. ) )
246 245 orbi2d 
 |-  ( y = ( 2nd ` p ) -> ( ( ( 1st ` p ) =/= .0. \/ y =/= .0. ) <-> ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) ) )
247 244 246 imbi12d 
 |-  ( y = ( 2nd ` p ) -> ( ( ( ( 1st ` p ) .+ y ) =/= ( 0g ` K ) -> ( ( 1st ` p ) =/= .0. \/ y =/= .0. ) ) <-> ( ( ( 1st ` p ) .+ ( 2nd ` p ) ) =/= ( 0g ` K ) -> ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) ) ) )
248 242 247 rspc2v 
 |-  ( ( ( 1st ` p ) e. B /\ ( 2nd ` p ) e. B ) -> ( A. x e. B A. y e. B ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) -> ( ( ( 1st ` p ) .+ ( 2nd ` p ) ) =/= ( 0g ` K ) -> ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) ) ) )
249 236 237 248 syl2anc 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( A. x e. B A. y e. B ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) -> ( ( ( 1st ` p ) .+ ( 2nd ` p ) ) =/= ( 0g ` K ) -> ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) ) ) )
250 215 234 249 mp2d 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) )
251 1 2 3 4 5 6 7 8 9 13 11 15 sibfinima 
 |-  ( ( ( ph /\ ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) /\ ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) ) -> ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) e. ( 0 [,) +oo ) )
252 200 204 206 250 251 syl31anc 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) e. ( 0 [,) +oo ) )
253 199 252 esumpfinval 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> sum* p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) = sum_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
254 172 196 253 3eqtrd 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( M ` ( `' ( F oF .+ G ) " { z } ) ) = sum_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
255 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
256 255 252 sselid 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) e. RR )
257 199 256 fsumrecl 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> sum_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) e. RR )
258 254 257 eqeltrd 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( M ` ( `' ( F oF .+ G ) " { z } ) ) e. RR )
259 175 adantr 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> M e. ( measures ` dom M ) )
260 176 109 sylanl2 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M )
261 measge0 
 |-  ( ( M e. ( measures ` dom M ) /\ ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M ) -> 0 <_ ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
262 259 260 261 syl2anc 
 |-  ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> 0 <_ ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
263 199 256 262 fsumge0 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> 0 <_ sum_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
264 263 254 breqtrrd 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> 0 <_ ( M ` ( `' ( F oF .+ G ) " { z } ) ) )
265 elrege0 
 |-  ( ( M ` ( `' ( F oF .+ G ) " { z } ) ) e. ( 0 [,) +oo ) <-> ( ( M ` ( `' ( F oF .+ G ) " { z } ) ) e. RR /\ 0 <_ ( M ` ( `' ( F oF .+ G ) " { z } ) ) ) )
266 258 264 265 sylanbrc 
 |-  ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( M ` ( `' ( F oF .+ G ) " { z } ) ) e. ( 0 [,) +oo ) )
267 266 ralrimiva 
 |-  ( ph -> A. z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ( M ` ( `' ( F oF .+ G ) " { z } ) ) e. ( 0 [,) +oo ) )
268 eqid 
 |-  ( sigaGen ` ( TopOpen ` K ) ) = ( sigaGen ` ( TopOpen ` K ) )
269 eqid 
 |-  ( 0g ` K ) = ( 0g ` K )
270 eqid 
 |-  ( .s ` K ) = ( .s ` K )
271 eqid 
 |-  ( RRHom ` ( Scalar ` K ) ) = ( RRHom ` ( Scalar ` K ) )
272 10 30 268 269 270 271 14 8 issibf 
 |-  ( ph -> ( ( F oF .+ G ) e. dom ( K sitg M ) <-> ( ( F oF .+ G ) e. ( dom M MblFnM ( sigaGen ` ( TopOpen ` K ) ) ) /\ ran ( F oF .+ G ) e. Fin /\ A. z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ( M ` ( `' ( F oF .+ G ) " { z } ) ) e. ( 0 [,) +oo ) ) ) )
273 170 138 267 272 mpbir3and 
 |-  ( ph -> ( F oF .+ G ) e. dom ( K sitg M ) )