Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sibfof Unicode version

Theorem sibfof 24607
Description: Applying function operations on simple functions results in simple functions with regard to the the destination space, provided the operation fulfills a simple condition. (Contributed by Thierry Arnoux, 12-Mar-2018.)
Hypotheses
Ref Expression
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  ( Wsitg 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  ( Wsitg M ) )
sibfof.3  |-  ( ph  ->  K  e.  TopSp )
sibfof.4  |-  ( ph  ->  J  e.  Fre )
sibfof.5  |-  ( ph  ->  (  .0.  .+  .0.  )  =  ( 0g `  K ) )
Assertion
Ref Expression
sibfof  |-  ( ph  ->  ( F  o F 
.+  G )  e. 
dom  ( Ksitg M
) )

Proof of Theorem sibfof
Dummy variables  x  y  z  b  p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sibfof.1 . . . . . . . . . 10  |-  ( ph  ->  .+  : ( B  X.  B ) --> C )
2 sibfof.0 . . . . . . . . . . . . 13  |-  ( ph  ->  W  e.  TopSp )
3 sitgval.b . . . . . . . . . . . . . 14  |-  B  =  ( Base `  W
)
4 sitgval.j . . . . . . . . . . . . . 14  |-  J  =  ( TopOpen `  W )
53, 4tpsuni 16958 . . . . . . . . . . . . 13  |-  ( W  e.  TopSp  ->  B  =  U. J )
62, 5syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  B  =  U. J
)
76, 6xpeq12d 4862 . . . . . . . . . . 11  |-  ( ph  ->  ( B  X.  B
)  =  ( U. J  X.  U. J ) )
87feq2d 5540 . . . . . . . . . 10  |-  ( ph  ->  (  .+  : ( B  X.  B ) --> C  <->  .+  : ( U. J  X.  U. J ) --> C ) )
91, 8mpbid 202 . . . . . . . . 9  |-  ( ph  ->  .+  : ( U. J  X.  U. J ) --> C )
109fovrnda 6176 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  U. J  /\  x  e.  U. J ) )  ->  ( z  .+  x )  e.  C
)
11 sitgval.s . . . . . . . . 9  |-  S  =  (sigaGen `  J )
12 sitgval.0 . . . . . . . . 9  |-  .0.  =  ( 0g `  W )
13 sitgval.x . . . . . . . . 9  |-  .x.  =  ( .s `  W )
14 sitgval.h . . . . . . . . 9  |-  H  =  (RRHom `  (Scalar `  W
) )
15 sitgval.1 . . . . . . . . 9  |-  ( ph  ->  W  e.  V )
16 sitgval.2 . . . . . . . . 9  |-  ( ph  ->  M  e.  U. ran measures )
17 sibfmbl.1 . . . . . . . . 9  |-  ( ph  ->  F  e.  dom  ( Wsitg M ) )
183, 4, 11, 12, 13, 14, 15, 16, 17sibff 24604 . . . . . . . 8  |-  ( ph  ->  F : U. dom  M --> U. J )
19 sibfof.2 . . . . . . . . 9  |-  ( ph  ->  G  e.  dom  ( Wsitg M ) )
203, 4, 11, 12, 13, 14, 15, 16, 19sibff 24604 . . . . . . . 8  |-  ( ph  ->  G : U. dom  M --> U. J )
21 dmexg 5089 . . . . . . . . 9  |-  ( M  e.  U. ran measures  ->  dom  M  e.  _V )
22 uniexg 4665 . . . . . . . . 9  |-  ( dom 
M  e.  _V  ->  U.
dom  M  e.  _V )
2316, 21, 223syl 19 . . . . . . . 8  |-  ( ph  ->  U. dom  M  e. 
_V )
24 inidm 3510 . . . . . . . 8  |-  ( U. dom  M  i^i  U. dom  M )  =  U. dom  M
2510, 18, 20, 23, 23, 24off 6279 . . . . . . 7  |-  ( ph  ->  ( F  o F 
.+  G ) : U. dom  M --> C )
26 sibfof.3 . . . . . . . . . 10  |-  ( ph  ->  K  e.  TopSp )
27 sibfof.c . . . . . . . . . . 11  |-  C  =  ( Base `  K
)
28 eqid 2404 . . . . . . . . . . 11  |-  ( TopOpen `  K )  =  (
TopOpen `  K )
2927, 28tpsuni 16958 . . . . . . . . . 10  |-  ( K  e.  TopSp  ->  C  =  U. ( TopOpen `  K )
)
3026, 29syl 16 . . . . . . . . 9  |-  ( ph  ->  C  =  U. ( TopOpen
`  K ) )
31 eqid 2404 . . . . . . . . . . 11  |-  (sigaGen `  ( TopOpen
`  K ) )  =  (sigaGen `  ( TopOpen
`  K ) )
3231unieqi 3985 . . . . . . . . . 10  |-  U. (sigaGen `  ( TopOpen `  K )
)  =  U. (sigaGen `  ( TopOpen `  K )
)
33 fvex 5701 . . . . . . . . . . 11  |-  ( TopOpen `  K )  e.  _V
34 unisg 24479 . . . . . . . . . . 11  |-  ( (
TopOpen `  K )  e. 
_V  ->  U. (sigaGen `  ( TopOpen
`  K ) )  =  U. ( TopOpen `  K ) )
3533, 34ax-mp 8 . . . . . . . . . 10  |-  U. (sigaGen `  ( TopOpen `  K )
)  =  U. ( TopOpen
`  K )
3632, 35eqtri 2424 . . . . . . . . 9  |-  U. (sigaGen `  ( TopOpen `  K )
)  =  U. ( TopOpen
`  K )
3730, 36syl6eqr 2454 . . . . . . . 8  |-  ( ph  ->  C  =  U. (sigaGen `  ( TopOpen `  K )
) )
38 feq3 5537 . . . . . . . 8  |-  ( C  =  U. (sigaGen `  ( TopOpen
`  K ) )  ->  ( ( F  o F  .+  G
) : U. dom  M --> C  <->  ( F  o F  .+  G ) : U. dom  M --> U. (sigaGen `  ( TopOpen `  K )
) ) )
3937, 38syl 16 . . . . . . 7  |-  ( ph  ->  ( ( F  o F  .+  G ) : U. dom  M --> C  <->  ( F  o F  .+  G ) : U. dom  M --> U. (sigaGen `  ( TopOpen `  K
) ) ) )
4025, 39mpbid 202 . . . . . 6  |-  ( ph  ->  ( F  o F 
.+  G ) : U. dom  M --> U. (sigaGen `  ( TopOpen `  K )
) )
4133a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( TopOpen `  K )  e.  _V )
4241sgsiga 24478 . . . . . . . . 9  |-  ( ph  ->  (sigaGen `  ( TopOpen `  K
) )  e.  U. ran sigAlgebra )
4331, 42syl5eqel 2488 . . . . . . . 8  |-  ( ph  ->  (sigaGen `  ( TopOpen `  K
) )  e.  U. ran sigAlgebra )
44 uniexg 4665 . . . . . . . 8  |-  ( (sigaGen `  ( TopOpen `  K )
)  e.  U. ran sigAlgebra  ->  U. (sigaGen `  ( TopOpen `  K
) )  e.  _V )
4543, 44syl 16 . . . . . . 7  |-  ( ph  ->  U. (sigaGen `  ( TopOpen
`  K ) )  e.  _V )
46 elmapg 6990 . . . . . . 7  |-  ( ( U. (sigaGen `  ( TopOpen
`  K ) )  e.  _V  /\  U. dom  M  e.  _V )  ->  ( ( F  o F  .+  G )  e.  ( U. (sigaGen `  ( TopOpen
`  K ) )  ^m  U. dom  M
)  <->  ( F  o F  .+  G ) : U. dom  M --> U. (sigaGen `  ( TopOpen `  K )
) ) )
4745, 23, 46syl2anc 643 . . . . . 6  |-  ( ph  ->  ( ( F  o F  .+  G )  e.  ( U. (sigaGen `  ( TopOpen
`  K ) )  ^m  U. dom  M
)  <->  ( F  o F  .+  G ) : U. dom  M --> U. (sigaGen `  ( TopOpen `  K )
) ) )
4840, 47mpbird 224 . . . . 5  |-  ( ph  ->  ( F  o F 
.+  G )  e.  ( U. (sigaGen `  ( TopOpen
`  K ) )  ^m  U. dom  M
) )
49 inundif 3666 . . . . . . . . 9  |-  ( ( b  i^i  ran  ( F  o F  .+  G
) )  u.  (
b  \  ran  ( F  o F  .+  G
) ) )  =  b
5049imaeq2i 5160 . . . . . . . 8  |-  ( `' ( F  o F 
.+  G ) "
( ( b  i^i 
ran  ( F  o F  .+  G ) )  u.  ( b  \  ran  ( F  o F 
.+  G ) ) ) )  =  ( `' ( F  o F  .+  G ) "
b )
51 ffun 5552 . . . . . . . . . 10  |-  ( ( F  o F  .+  G ) : U. dom  M --> C  ->  Fun  ( F  o F  .+  G ) )
52 unpreima 5815 . . . . . . . . . 10  |-  ( Fun  ( F  o F 
.+  G )  -> 
( `' ( F  o F  .+  G
) " ( ( b  i^i  ran  ( F  o F  .+  G
) )  u.  (
b  \  ran  ( F  o F  .+  G
) ) ) )  =  ( ( `' ( F  o F 
.+  G ) "
( b  i^i  ran  ( F  o F  .+  G ) ) )  u.  ( `' ( F  o F  .+  G ) " (
b  \  ran  ( F  o F  .+  G
) ) ) ) )
5325, 51, 523syl 19 . . . . . . . . 9  |-  ( ph  ->  ( `' ( F  o F  .+  G
) " ( ( b  i^i  ran  ( F  o F  .+  G
) )  u.  (
b  \  ran  ( F  o F  .+  G
) ) ) )  =  ( ( `' ( F  o F 
.+  G ) "
( b  i^i  ran  ( F  o F  .+  G ) ) )  u.  ( `' ( F  o F  .+  G ) " (
b  \  ran  ( F  o F  .+  G
) ) ) ) )
5453adantr 452 . . . . . . . 8  |-  ( (
ph  /\  b  e.  (sigaGen `  ( TopOpen `  K
) ) )  -> 
( `' ( F  o F  .+  G
) " ( ( b  i^i  ran  ( F  o F  .+  G
) )  u.  (
b  \  ran  ( F  o F  .+  G
) ) ) )  =  ( ( `' ( F  o F 
.+  G ) "
( b  i^i  ran  ( F  o F  .+  G ) ) )  u.  ( `' ( F  o F  .+  G ) " (
b  \  ran  ( F  o F  .+  G
) ) ) ) )
5550, 54syl5eqr 2450 . . . . . . 7  |-  ( (
ph  /\  b  e.  (sigaGen `  ( TopOpen `  K
) ) )  -> 
( `' ( F  o F  .+  G
) " b )  =  ( ( `' ( F  o F 
.+  G ) "
( b  i^i  ran  ( F  o F  .+  G ) ) )  u.  ( `' ( F  o F  .+  G ) " (
b  \  ran  ( F  o F  .+  G
) ) ) ) )
56 dmmeas 24508 . . . . . . . . . 10  |-  ( M  e.  U. ran measures  ->  dom  M  e.  U. ran sigAlgebra )
5716, 56syl 16 . . . . . . . . 9  |-  ( ph  ->  dom  M  e.  U. ran sigAlgebra )
5857adantr 452 . . . . . . . 8  |-  ( (
ph  /\  b  e.  (sigaGen `  ( TopOpen `  K
) ) )  ->  dom  M  e.  U. ran sigAlgebra )
59 imaiun 5951 . . . . . . . . . 10  |-  ( `' ( F  o F 
.+  G ) " U_ z  e.  (
b  i^i  ran  ( F  o F  .+  G
) ) { z } )  =  U_ z  e.  ( b  i^i  ran  ( F  o F  .+  G ) ) ( `' ( F  o F  .+  G
) " { z } )
60 iunid 4106 . . . . . . . . . . 11  |-  U_ z  e.  ( b  i^i  ran  ( F  o F  .+  G ) ) { z }  =  ( b  i^i  ran  ( F  o F  .+  G
) )
6160imaeq2i 5160 . . . . . . . . . 10  |-  ( `' ( F  o F 
.+  G ) " U_ z  e.  (
b  i^i  ran  ( F  o F  .+  G
) ) { z } )  =  ( `' ( F  o F  .+  G ) "
( b  i^i  ran  ( F  o F  .+  G ) ) )
6259, 61eqtr3i 2426 . . . . . . . . 9  |-  U_ z  e.  ( b  i^i  ran  ( F  o F  .+  G ) ) ( `' ( F  o F  .+  G ) " { z } )  =  ( `' ( F  o F  .+  G ) " (
b  i^i  ran  ( F  o F  .+  G
) ) )
63 inss2 3522 . . . . . . . . . . . 12  |-  ( b  i^i  ran  ( F  o F  .+  G ) )  C_  ran  ( F  o F  .+  G
)
64 feq3 5537 . . . . . . . . . . . . . . . . . . . 20  |-  ( B  =  U. J  -> 
( F : U. dom  M --> B  <->  F : U. dom  M --> U. J
) )
656, 64syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( F : U. dom  M --> B  <->  F : U. dom  M --> U. J
) )
6618, 65mpbird 224 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F : U. dom  M --> B )
67 feq3 5537 . . . . . . . . . . . . . . . . . . . 20  |-  ( B  =  U. J  -> 
( G : U. dom  M --> B  <->  G : U. dom  M --> U. J
) )
686, 67syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( G : U. dom  M --> B  <->  G : U. dom  M --> U. J
) )
6920, 68mpbird 224 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  G : U. dom  M --> B )
70 ffn 5550 . . . . . . . . . . . . . . . . . . 19  |-  (  .+  : ( B  X.  B ) --> C  ->  .+  Fn  ( B  X.  B ) )
711, 70syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  .+  Fn  ( B  X.  B ) )
7266, 69, 23, 71ofpreima 24034 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( `' ( F  o F  .+  G
) " { z } )  =  U_ p  e.  ( `'  .+  " { z } ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )
73 inundif 3666 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) )  u.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )  =  ( `' 
.+  " { z } )
74 iuneq1 4066 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) )  u.  ( ( `' 
.+  " { z } )  \  ( ran 
F  X.  ran  G
) ) )  =  ( `'  .+  " {
z } )  ->  U_ p  e.  (
( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) )  u.  ( ( `' 
.+  " { z } )  \  ( ran 
F  X.  ran  G
) ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  U_ p  e.  ( `'  .+  " {
z } ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )
7573, 74ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  U_ p  e.  ( ( ( `' 
.+  " { z } )  i^i  ( ran 
F  X.  ran  G
) )  u.  (
( `'  .+  " {
z } )  \ 
( ran  F  X.  ran  G ) ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  U_ p  e.  ( `'  .+  " {
z } ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )
76 iunxun 4132 . . . . . . . . . . . . . . . . . 18  |-  U_ p  e.  ( ( ( `' 
.+  " { z } )  i^i  ( ran 
F  X.  ran  G
) )  u.  (
( `'  .+  " {
z } )  \ 
( ran  F  X.  ran  G ) ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  ( U_ p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  u.  U_ p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )
7775, 76eqtr3i 2426 . . . . . . . . . . . . . . . . 17  |-  U_ p  e.  ( `'  .+  " {
z } ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  ( U_ p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  u.  U_ p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )
7872, 77syl6eq 2452 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( `' ( F  o F  .+  G
) " { z } )  =  (
U_ p  e.  ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  u.  U_ p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) ) )
79 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )  ->  p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )
8079eldifbd 3293 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )  ->  -.  p  e.  ( ran  F  X.  ran  G ) )
81 difssd 3435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) 
C_  ( `'  .+  " { z } ) )
82 cnvimass 5183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( `' 
.+  " { z } )  C_  dom  .+
83 fdm 5554 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  (  .+  : ( B  X.  B ) --> C  ->  dom  .+  =  ( B  X.  B ) )
841, 83syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  dom  .+  =  ( B  X.  B ) )
8582, 84syl5sseq 3356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( `'  .+  " {
z } )  C_  ( B  X.  B
) )
8681, 85sstrd 3318 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) 
C_  ( B  X.  B ) )
8786sselda 3308 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )  ->  p  e.  ( B  X.  B
) )
88 1st2nd2 6345 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( p  e.  ( B  X.  B )  ->  p  =  <. ( 1st `  p
) ,  ( 2nd `  p ) >. )
89 elxp6 6337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( p  e.  ( ran  F  X.  ran  G )  <->  ( p  =  <. ( 1st `  p
) ,  ( 2nd `  p ) >.  /\  (
( 1st `  p
)  e.  ran  F  /\  ( 2nd `  p
)  e.  ran  G
) ) )
9089biimpri 198 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( p  =  <. ( 1st `  p ) ,  ( 2nd `  p
) >.  /\  ( ( 1st `  p )  e. 
ran  F  /\  ( 2nd `  p )  e. 
ran  G ) )  ->  p  e.  ( ran  F  X.  ran  G ) )
9190ex 424 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( p  =  <. ( 1st `  p
) ,  ( 2nd `  p ) >.  ->  (
( ( 1st `  p
)  e.  ran  F  /\  ( 2nd `  p
)  e.  ran  G
)  ->  p  e.  ( ran  F  X.  ran  G ) ) )
9287, 88, 913syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )  ->  ( (
( 1st `  p
)  e.  ran  F  /\  ( 2nd `  p
)  e.  ran  G
)  ->  p  e.  ( ran  F  X.  ran  G ) ) )
9392con3d 127 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )  ->  ( -.  p  e.  ( ran  F  X.  ran  G )  ->  -.  ( ( 1st `  p )  e. 
ran  F  /\  ( 2nd `  p )  e. 
ran  G ) ) )
9480, 93mpd 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )  ->  -.  (
( 1st `  p
)  e.  ran  F  /\  ( 2nd `  p
)  e.  ran  G
) )
95 ianor 475 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  ( ( 1st `  p
)  e.  ran  F  /\  ( 2nd `  p
)  e.  ran  G
)  <->  ( -.  ( 1st `  p )  e. 
ran  F  \/  -.  ( 2nd `  p )  e.  ran  G ) )
9694, 95sylib 189 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )  ->  ( -.  ( 1st `  p )  e.  ran  F  \/  -.  ( 2nd `  p
)  e.  ran  G
) )
97 disjsn 3828 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ran  F  i^i  {
( 1st `  p
) } )  =  (/) 
<->  -.  ( 1st `  p
)  e.  ran  F
)
98 disjsn 3828 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ran  G  i^i  {
( 2nd `  p
) } )  =  (/) 
<->  -.  ( 2nd `  p
)  e.  ran  G
)
9997, 98orbi12i 508 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ran  F  i^i  { ( 1st `  p
) } )  =  (/)  \/  ( ran  G  i^i  { ( 2nd `  p
) } )  =  (/) )  <->  ( -.  ( 1st `  p )  e. 
ran  F  \/  -.  ( 2nd `  p )  e.  ran  G ) )
10096, 99sylibr 204 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )  ->  ( ( ran  F  i^i  { ( 1st `  p ) } )  =  (/)  \/  ( ran  G  i^i  { ( 2nd `  p
) } )  =  (/) ) )
101 ffn 5550 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( F : U. dom  M --> U. J  ->  F  Fn  U.
dom  M )
10218, 101syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  F  Fn  U. dom  M )
103 dffn3 5557 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F  Fn  U. dom  M  <->  F : U. dom  M --> ran  F )
104102, 103sylib 189 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  F : U. dom  M --> ran  F )
105104adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )  ->  F : U. dom  M --> ran  F
)
106 ffn 5550 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( G : U. dom  M --> U. J  ->  G  Fn  U.
dom  M )
10720, 106syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  G  Fn  U. dom  M )
108 dffn3 5557 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( G  Fn  U. dom  M  <->  G : U. dom  M --> ran  G )
109107, 108sylib 189 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  G : U. dom  M --> ran  G )
110109adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )  ->  G : U. dom  M --> ran  G
)
111 fimacnvdisj 5580 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( F : U. dom  M --> ran  F  /\  ( ran  F  i^i  { ( 1st `  p ) } )  =  (/) )  ->  ( `' F " { ( 1st `  p
) } )  =  (/) )
112 ineq1 3495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( `' F " { ( 1st `  p ) } )  =  (/)  ->  ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  ( (/)  i^i  ( `' G " { ( 2nd `  p ) } ) ) )
113 incom 3493 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (/)  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  ( ( `' G " { ( 2nd `  p ) } )  i^i  (/) )
114 in0 3613 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( `' G " { ( 2nd `  p ) } )  i^i  (/) )  =  (/)
115113, 114eqtri 2424 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (/)  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  (/)
116112, 115syl6eq 2452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( `' F " { ( 1st `  p ) } )  =  (/)  ->  ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  (/) )
117111, 116syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( F : U. dom  M --> ran  F  /\  ( ran  F  i^i  { ( 1st `  p ) } )  =  (/) )  ->  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) )  =  (/) )
118117ex 424 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( F : U. dom  M --> ran  F  ->  ( ( ran  F  i^i  { ( 1st `  p ) } )  =  (/)  ->  ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  (/) ) )
119 fimacnvdisj 5580 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( G : U. dom  M --> ran  G  /\  ( ran  G  i^i  { ( 2nd `  p ) } )  =  (/) )  ->  ( `' G " { ( 2nd `  p
) } )  =  (/) )
120 ineq2 3496 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( `' G " { ( 2nd `  p ) } )  =  (/)  ->  ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  ( ( `' F " { ( 1st `  p ) } )  i^i  (/) ) )
121 in0 3613 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( `' F " { ( 1st `  p ) } )  i^i  (/) )  =  (/)
122120, 121syl6eq 2452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( `' G " { ( 2nd `  p ) } )  =  (/)  ->  ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  (/) )
123119, 122syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( G : U. dom  M --> ran  G  /\  ( ran  G  i^i  { ( 2nd `  p ) } )  =  (/) )  ->  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) )  =  (/) )
124123ex 424 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( G : U. dom  M --> ran  G  ->  ( ( ran  G  i^i  { ( 2nd `  p ) } )  =  (/)  ->  ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  (/) ) )
125118, 124jaao 496 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : U. dom  M --> ran  F  /\  G : U. dom  M --> ran  G
)  ->  ( (
( ran  F  i^i  { ( 1st `  p
) } )  =  (/)  \/  ( ran  G  i^i  { ( 2nd `  p
) } )  =  (/) )  ->  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) )  =  (/) ) )
126105, 110, 125syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )  ->  ( (
( ran  F  i^i  { ( 1st `  p
) } )  =  (/)  \/  ( ran  G  i^i  { ( 2nd `  p
) } )  =  (/) )  ->  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) )  =  (/) ) )
127100, 126mpd 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) )  ->  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) )  =  (/) )
128127ralrimiva 2749 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  A. p  e.  ( ( `'  .+  " {
z } )  \ 
( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  (/) )
129 iuneq2 4069 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. p  e.  ( ( `'  .+  " { z } )  \  ( ran  F  X.  ran  G
) ) ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) )  =  (/)  ->  U_ p  e.  ( ( `'  .+  " {
z } )  \ 
( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  U_ p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) )
(/) )
130128, 129syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  U_ p  e.  ( ( `'  .+  " {
z } )  \ 
( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  U_ p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) )
(/) )
131 iun0 4107 . . . . . . . . . . . . . . . . . . 19  |-  U_ p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) )
(/)  =  (/)
132130, 131syl6eq 2452 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  U_ p  e.  ( ( `'  .+  " {
z } )  \ 
( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  =  (/) )
133132uneq2d 3461 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( U_ p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  u.  U_ p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )  =  ( U_ p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G
) ) ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) )  u.  (/) ) )
134 un0 3612 . . . . . . . . . . . . . . . . 17  |-  ( U_ p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G
) ) ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) )  u.  (/) )  =  U_ p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G
) ) ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) )
135133, 134syl6eq 2452 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( U_ p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  u.  U_ p  e.  ( ( `'  .+  " { z } ) 
\  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )  =  U_ p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )
13678, 135eqtrd 2436 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( `' ( F  o F  .+  G
) " { z } )  =  U_ p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G
) ) ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) ) )
137136adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  ran  ( F  o F 
.+  G ) )  ->  ( `' ( F  o F  .+  G ) " {
z } )  = 
U_ p  e.  ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )
13857adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  ran  ( F  o F 
.+  G ) )  ->  dom  M  e.  U.
ran sigAlgebra )
13957ad2antrr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  ran  ( F  o F  .+  G ) )  /\  p  e.  ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  dom  M  e.  U.
ran sigAlgebra )
140 simpll 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  ran  ( F  o F  .+  G ) )  /\  p  e.  ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ph )
141 inss1 3521 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G
) )  C_  ( `'  .+  " { z } )
14285adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  z  e.  ran  ( F  o F 
.+  G ) )  ->  ( `'  .+  " { z } ) 
C_  ( B  X.  B ) )
143141, 142syl5ss 3319 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  z  e.  ran  ( F  o F 
.+  G ) )  ->  ( ( `' 
.+  " { z } )  i^i  ( ran 
F  X.  ran  G
) )  C_  ( B  X.  B ) )
144143sselda 3308 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  ran  ( F  o F  .+  G ) )  /\  p  e.  ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  p  e.  ( B  X.  B ) )
14557adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  dom  M  e.  U. ran sigAlgebra )
146 fvex 5701 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( TopOpen `  W )  e.  _V
1474, 146eqeltri 2474 . . . . . . . . . . . . . . . . . . . . . . 23  |-  J  e. 
_V
148147a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  J  e.  _V )
149148sgsiga 24478 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  (sigaGen `  J )  e.  U. ran sigAlgebra )
15011, 149syl5eqel 2488 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  S  e.  U. ran sigAlgebra )
151150adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  S  e.  U. ran sigAlgebra )
1523, 4, 11, 12, 13, 14, 15, 16, 17sibfmbl 24603 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F  e.  ( dom 
MMblFnM S ) )
153152adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  F  e.  ( dom  MMblFnM S
) )
1544tpstop 16959 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( W  e.  TopSp  ->  J  e.  Top )
155 cldssbrsiga 24494 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( J  e.  Top  ->  ( Clsd `  J )  C_  (sigaGen `  J ) )
1562, 154, 1553syl 19 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( Clsd `  J
)  C_  (sigaGen `  J
) )
157156adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  ( Clsd `  J )  C_  (sigaGen `  J ) )
158 sibfof.4 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  J  e.  Fre )
159158adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  J  e.  Fre )
160 xp1st 6335 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  e.  ( B  X.  B )  ->  ( 1st `  p )  e.  B )
161160adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  ( 1st `  p )  e.  B )
1626adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  B  =  U. J )
163161, 162eleqtrd 2480 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  ( 1st `  p )  e. 
U. J )
164 eqid 2404 . . . . . . . . . . . . . . . . . . . . . . 23  |-  U. J  =  U. J
165164t1sncld 17344 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( J  e.  Fre  /\  ( 1st `  p )  e.  U. J )  ->  { ( 1st `  p ) }  e.  ( Clsd `  J )
)
166159, 163, 165syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  { ( 1st `  p ) }  e.  ( Clsd `  J ) )
167157, 166sseldd 3309 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  { ( 1st `  p ) }  e.  (sigaGen `  J
) )
168167, 11syl6eleqr 2495 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  { ( 1st `  p ) }  e.  S )
169145, 151, 153, 168mbfmcnvima 24560 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  ( `' F " { ( 1st `  p ) } )  e.  dom  M )
170140, 144, 169syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  ran  ( F  o F  .+  G ) )  /\  p  e.  ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( `' F " { ( 1st `  p
) } )  e. 
dom  M )
1713, 4, 11, 12, 13, 14, 15, 16, 19sibfmbl 24603 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  G  e.  ( dom 
MMblFnM S ) )
172171adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  G  e.  ( dom  MMblFnM S
) )
173 xp2nd 6336 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  e.  ( B  X.  B )  ->  ( 2nd `  p )  e.  B )
174173adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  ( 2nd `  p )  e.  B )
175174, 162eleqtrd 2480 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  ( 2nd `  p )  e. 
U. J )
176164t1sncld 17344 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( J  e.  Fre  /\  ( 2nd `  p )  e.  U. J )  ->  { ( 2nd `  p ) }  e.  ( Clsd `  J )
)
177159, 175, 176syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  { ( 2nd `  p ) }  e.  ( Clsd `  J ) )
178157, 177sseldd 3309 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  { ( 2nd `  p ) }  e.  (sigaGen `  J
) )
179178, 11syl6eleqr 2495 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  { ( 2nd `  p ) }  e.  S )
180145, 151, 172, 179mbfmcnvima 24560 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  p  e.  ( B  X.  B
) )  ->  ( `' G " { ( 2nd `  p ) } )  e.  dom  M )
181140, 144, 180syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  ran  ( F  o F  .+  G ) )  /\  p  e.  ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( `' G " { ( 2nd `  p
) } )  e. 
dom  M )
182 inelsiga 24471 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 )
183139, 170, 181, 182syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  ran  ( F  o F  .+  G ) )  /\  p  e.  ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) )  e. 
dom  M )
184183ralrimiva 2749 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  ran  ( F  o F 
.+  G ) )  ->  A. p  e.  ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  e.  dom  M )
185 inss2 3522 . . . . . . . . . . . . . . . . . 18  |-  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G
) )  C_  ( ran  F  X.  ran  G
)
1863, 4, 11, 12, 13, 14, 15, 16, 17sibfrn 24605 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ran  F  e.  Fin )
1873, 4, 11, 12, 13, 14, 15, 16, 19sibfrn 24605 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ran  G  e.  Fin )
188 xpfi 7337 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ran  F  e.  Fin  /\ 
ran  G  e.  Fin )  ->  ( ran  F  X.  ran  G )  e. 
Fin )
189186, 187, 188syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ran  F  X.  ran  G )  e.  Fin )
190 ssdomg 7112 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) ) )
191189, 190syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( `' 
.+  " { 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
) ) )
192185, 191mpi 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) )  ~<_  ( ran  F  X.  ran  G ) )
193 isfinite 7563 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ran  F  X.  ran  G )  e.  Fin  <->  ( ran  F  X.  ran  G ) 
~<  om )
194193biimpi 187 . . . . . . . . . . . . . . . . . 18  |-  ( ( ran  F  X.  ran  G )  e.  Fin  ->  ( ran  F  X.  ran  G )  ~<  om )
195 sdomdom 7094 . . . . . . . . . . . . . . . . . 18  |-  ( ( ran  F  X.  ran  G )  ~<  om  ->  ( ran  F  X.  ran  G )  ~<_  om )
196189, 194, 1953syl 19 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ran  F  X.  ran  G )  ~<_  om )
197 domtr 7119 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( `'  .+  " { 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 )
198192, 196, 197syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) )  ~<_  om )
199198adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  z  e.  ran  ( F  o F 
.+  G ) )  ->  ( ( `' 
.+  " { z } )  i^i  ( ran 
F  X.  ran  G
) )  ~<_  om )
200 nfcv 2540 . . . . . . . . . . . . . . . 16  |-  F/_ p
( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) )
201200sigaclcuni 24454 . . . . . . . . . . . . . . 15  |-  ( ( 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 )
202138, 184, 199, 201syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  z  e.  ran  ( F  o F 
.+  G ) )  ->  U_ p  e.  ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) )  e.  dom  M )
203137, 202eqeltrd 2478 . . . . . . . . . . . . 13  |-  ( (
ph  /\  z  e.  ran  ( F  o F 
.+  G ) )  ->  ( `' ( F  o F  .+  G ) " {
z } )  e. 
dom  M )
204203ralrimiva 2749 . . . . . . . . . . . 12  |-  ( ph  ->  A. z  e.  ran  ( F  o F  .+  G ) ( `' ( F  o F 
.+  G ) " { z } )  e.  dom  M )
205 ssralv 3367 . . . . . . . . . . . 12  |-  ( ( b  i^i  ran  ( F  o F  .+  G
) )  C_  ran  ( F  o F  .+  G )  ->  ( A. z  e.  ran  ( F  o F  .+  G ) ( `' ( F  o F 
.+  G ) " { z } )  e.  dom  M  ->  A. z  e.  (
b  i^i  ran  ( F  o F  .+  G
) ) ( `' ( F  o F 
.+  G ) " { z } )  e.  dom  M ) )
20663, 204, 205mpsyl 61 . . . . . . . . . . 11  |-  ( ph  ->  A. z  e.  ( b  i^i  ran  ( F  o F  .+  G
) ) ( `' ( F  o F 
.+  G ) " { z } )  e.  dom  M )
207206adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  (sigaGen `  ( TopOpen `  K
) ) )  ->  A. z  e.  (
b  i^i  ran  ( F  o F  .+  G
) ) ( `' ( F  o F 
.+  G ) " { z } )  e.  dom  M )
208 ffun 5552 . . . . . . . . . . . . . . . . 17  |-  (  .+  : ( B  X.  B ) --> C  ->  Fun  .+  )
2091, 208syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  Fun  .+  )
210 imafi 7357 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  .+  /\  ( ran  F  X.  ran  G
)  e.  Fin )  ->  (  .+  " ( ran  F  X.  ran  G
) )  e.  Fin )
211209, 189, 210syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ph  ->  (  .+  " ( ran  F  X.  ran  G
) )  e.  Fin )
21218, 20, 9, 23ofrn2 24006 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ran  ( F  o F  .+  G )  C_  (  .+  " ( ran 
F  X.  ran  G
) ) )
213 ssfi 7288 . . . . . . . . . . . . . . 15  |-  ( ( (  .+  " ( ran  F  X.  ran  G
) )  e.  Fin  /\ 
ran  ( F  o F  .+  G )  C_  (  .+  " ( ran 
F  X.  ran  G
) ) )  ->  ran  ( F  o F 
.+  G )  e. 
Fin )
214211, 212, 213syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ph  ->  ran  ( F  o F  .+  G )  e. 
Fin )
215 ssdomg 7112 . . . . . . . . . . . . . 14  |-  ( ran  ( F  o F 
.+  G )  e. 
Fin  ->  ( ( b  i^i  ran  ( F  o F  .+  G ) )  C_  ran  ( F  o F  .+  G
)  ->  ( b  i^i  ran  ( F  o F  .+  G ) )  ~<_  ran  ( F  o F  .+  G ) ) )
216214, 215syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( b  i^i 
ran  ( F  o F  .+  G ) ) 
C_  ran  ( F  o F  .+  G )  ->  ( b  i^i 
ran  ( F  o F  .+  G ) )  ~<_  ran  ( F  o F  .+  G ) ) )
21763, 216mpi 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( b  i^i  ran  ( F  o F  .+  G ) )  ~<_  ran  ( F  o F 
.+  G ) )
218 isfinite 7563 . . . . . . . . . . . . . 14  |-  ( ran  ( F  o F 
.+  G )  e. 
Fin 
<->  ran  ( F  o F  .+  G )  ~<  om )
219214, 218sylib 189 . . . . . . . . . . . . 13  |-  ( ph  ->  ran  ( F  o F  .+  G )  ~<  om )
220 sdomdom 7094 . . . . . . . . . . . . 13  |-  ( ran  ( F  o F 
.+  G )  ~<  om  ->  ran  ( F  o F  .+  G )  ~<_  om )
221219, 220syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ran  ( F  o F  .+  G )  ~<_  om )
222 domtr 7119 . . . . . . . . . . . 12  |-  ( ( ( b  i^i  ran  ( F  o F  .+  G ) )  ~<_  ran  ( F  o F 
.+  G )  /\  ran  ( F  o F 
.+  G )  ~<_  om )  ->  ( b  i^i  ran  ( F  o F  .+  G ) )  ~<_  om )
223217, 221, 222syl2anc 643 . . . . . . . . . . 11  |-  ( ph  ->  ( b  i^i  ran  ( F  o F  .+  G ) )  ~<_  om )
224223adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  (sigaGen `  ( TopOpen `  K
) ) )  -> 
( b  i^i  ran  ( F  o F  .+  G ) )  ~<_  om )
225 nfcv 2540 . . . . . . . . . . 11  |-  F/_ z
( b  i^i  ran  ( F  o F  .+  G ) )
226225sigaclcuni 24454 . . . . . . . . . 10  |-  ( ( dom  M  e.  U. ran sigAlgebra  /\  A. z  e.  ( b  i^i  ran  ( F  o F  .+  G
) ) ( `' ( F  o F 
.+  G ) " { z } )  e.  dom  M  /\  ( b  i^i  ran  ( F  o F  .+  G ) )  ~<_  om )  ->  U_ z  e.  ( b  i^i  ran  ( F  o F  .+  G ) ) ( `' ( F  o F  .+  G ) " { z } )  e.  dom  M )
22758, 207, 224, 226syl3anc 1184 . . . . . . . . 9  |-  ( (
ph  /\  b  e.  (sigaGen `  ( TopOpen `  K
) ) )  ->  U_ z  e.  (
b  i^i  ran  ( F  o F  .+  G
) ) ( `' ( F  o F 
.+  G ) " { z } )  e.  dom  M )
22862, 227syl5eqelr 2489 . . . . . . . 8  |-  ( (
ph  /\  b  e.  (sigaGen `  ( TopOpen `  K
) ) )  -> 
( `' ( F  o F  .+  G
) " ( b  i^i  ran  ( F  o F  .+  G ) ) )  e.  dom  M )
229 difpreima 5817 . . . . . . . . . . . 12  |-  ( Fun  ( F  o F 
.+  G )  -> 
( `' ( F  o F  .+  G
) " ( b 
\  ran  ( F  o F  .+  G ) ) )  =  ( ( `' ( F  o F  .+  G
) " b ) 
\  ( `' ( F  o F  .+  G ) " ran  ( F  o F  .+  G ) ) ) )
23025, 51, 2293syl 19 . . . . . . . . . . 11  |-  ( ph  ->  ( `' ( F  o F  .+  G
) " ( b 
\  ran  ( F  o F  .+  G ) ) )  =  ( ( `' ( F  o F  .+  G
) " b ) 
\  ( `' ( F  o F  .+  G ) " ran  ( F  o F  .+  G ) ) ) )
231 cnvimarndm 5184 . . . . . . . . . . . . 13  |-  ( `' ( F  o F 
.+  G ) " ran  ( F  o F 
.+  G ) )  =  dom  ( F  o F  .+  G
)
232231difeq2i 3422 . . . . . . . . . . . 12  |-  ( ( `' ( F  o F  .+  G ) "
b )  \  ( `' ( F  o F  .+  G ) " ran  ( F  o F 
.+  G ) ) )  =  ( ( `' ( F  o F  .+  G ) "
b )  \  dom  ( F  o F  .+  G ) )
233 cnvimass 5183 . . . . . . . . . . . . 13  |-  ( `' ( F  o F 
.+  G ) "
b )  C_  dom  ( F  o F  .+  G )
234 ssdif0 3646 . . . . . . . . . . . . 13  |-  ( ( `' ( F  o F  .+  G ) "
b )  C_  dom  ( F  o F  .+  G )  <->  ( ( `' ( F  o F  .+  G ) "
b )  \  dom  ( F  o F  .+  G ) )  =  (/) )
235233, 234mpbi 200 . . . . . . . . . . . 12  |-  ( ( `' ( F  o F  .+  G ) "
b )  \  dom  ( F  o F  .+  G ) )  =  (/)
236232, 235eqtri 2424 . . . . . . . . . . 11  |-  ( ( `' ( F  o F  .+  G ) "
b )  \  ( `' ( F  o F  .+  G ) " ran  ( F  o F 
.+  G ) ) )  =  (/)
237230, 236syl6eq 2452 . . . . . . . . . 10  |-  ( ph  ->  ( `' ( F  o F  .+  G
) " ( b 
\  ran  ( F  o F  .+  G ) ) )  =  (/) )
238 0elsiga 24450 . . . . . . . . . . 11  |-  ( dom 
M  e.  U. ran sigAlgebra  ->  (/)  e.  dom  M )
23957, 238syl 16 . . . . . . . . . 10  |-  ( ph  -> 
(/)  e.  dom  M )
240237, 239eqeltrd 2478 . . . . . . . . 9  |-  ( ph  ->  ( `' ( F  o F  .+  G
) " ( b 
\  ran  ( F  o F  .+  G ) ) )  e.  dom  M )
241240adantr 452 . . . . . . . 8  |-  ( (
ph  /\  b  e.  (sigaGen `  ( TopOpen `  K
) ) )  -> 
( `' ( F  o F  .+  G
) " ( b 
\  ran  ( F  o F  .+  G ) ) )  e.  dom  M )
242 unelsiga 24470 . . . . . . . 8  |-  ( ( dom  M  e.  U. ran sigAlgebra  /\  ( `' ( F  o F  .+  G
) " ( b  i^i  ran  ( F  o F  .+  G ) ) )  e.  dom  M  /\  ( `' ( F  o F  .+  G ) " (
b  \  ran  ( F  o F  .+  G
) ) )  e. 
dom  M )  -> 
( ( `' ( F  o F  .+  G ) " (
b  i^i  ran  ( F  o F  .+  G
) ) )  u.  ( `' ( F  o F  .+  G
) " ( b 
\  ran  ( F  o F  .+  G ) ) ) )  e. 
dom  M )
24358, 228, 241, 242syl3anc 1184 . . . . . . 7  |-  ( (
ph  /\  b  e.  (sigaGen `  ( TopOpen `  K
) ) )  -> 
( ( `' ( F  o F  .+  G ) " (
b  i^i  ran  ( F  o F  .+  G
) ) )  u.  ( `' ( F  o F  .+  G
) " ( b 
\  ran  ( F  o F  .+  G ) ) ) )  e. 
dom  M )
24455, 243eqeltrd 2478 . . . . . 6  |-  ( (
ph  /\  b  e.  (sigaGen `  ( TopOpen `  K
) ) )  -> 
( `' ( F  o F  .+  G
) " b )  e.  dom  M )
245244ralrimiva 2749 . . . . 5  |-  ( ph  ->  A. b  e.  (sigaGen `  ( TopOpen `  K )
) ( `' ( F  o F  .+  G ) " b
)  e.  dom  M
)
24648, 245jca 519 . . . 4  |-  ( ph  ->  ( ( F  o F  .+  G )  e.  ( U. (sigaGen `  ( TopOpen
`  K ) )  ^m  U. dom  M
)  /\  A. b  e.  (sigaGen `  ( TopOpen `  K
) ) ( `' ( F  o F 
.+  G ) "
b )  e.  dom  M ) )
24757, 43ismbfm 24555 . . . 4  |-  ( ph  ->  ( ( F  o F  .+  G )  e.  ( dom  MMblFnM (sigaGen `  ( TopOpen `  K )
) )  <->  ( ( F  o F  .+  G
)  e.  ( U. (sigaGen `  ( TopOpen `  K
) )  ^m  U. dom  M )  /\  A. b  e.  (sigaGen `  ( TopOpen
`  K ) ) ( `' ( F  o F  .+  G
) " b )  e.  dom  M ) ) )
248246, 247mpbird 224 . . 3  |-  ( ph  ->  ( F  o F 
.+  G )  e.  ( dom  MMblFnM (sigaGen `  ( TopOpen `  K )
) ) )
249136adantr 452 . . . . . . . 8  |-  ( (
ph  /\  z  e.  ( ran  ( F  o F  .+  G )  \  { ( 0g `  K ) } ) )  ->  ( `' ( F  o F  .+  G ) " {
z } )  = 
U_ p  e.  ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )
250249fveq2d 5691 . . . . . . 7  |-  ( (
ph  /\  z  e.  ( ran  ( F  o F  .+  G )  \  { ( 0g `  K ) } ) )  ->  ( M `  ( `' ( F  o F  .+  G
) " { z } ) )  =  ( M `  U_ p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) ) )
251 measbasedom 24509 . . . . . . . . . 10  |-  ( M  e.  U. ran measures  <->  M  e.  (measures `  dom  M ) )
25216, 251sylib 189 . . . . . . . . 9  |-  ( ph  ->  M  e.  (measures `  dom  M ) )
253252adantr 452 . . . . . . . 8  |-  ( (
ph  /\  z  e.  ( ran  ( F  o F  .+  G )  \  { ( 0g `  K ) } ) )  ->  M  e.  (measures `  dom  M ) )
254 difss 3434 . . . . . . . . . 10  |-  ( ran  ( F  o F 
.+  G )  \  { ( 0g `  K ) } ) 
C_  ran  ( F  o F  .+  G )
255254sseli 3304 . . . . . . . . 9  |-  ( z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } )  ->  z  e.  ran  ( F  o F 
.+  G ) )
256255, 184sylan2 461 . . . . . . . 8  |-  ( (
ph  /\  z  e.  ( ran  ( F  o F  .+  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 )
257198adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  ( ran  ( F  o F  .+  G )  \  { ( 0g `  K ) } ) )  ->  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G
) )  ~<_  om )
258 ffun 5552 . . . . . . . . . . . . . 14  |-  ( F : U. dom  M --> U. J  ->  Fun  F
)
25918, 258syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  Fun  F )
260 sndisj 4164 . . . . . . . . . . . . 13  |- Disj  x  e. 
ran  F { x }
261 disjpreima 23979 . . . . . . . . . . . . 13  |-  ( ( Fun  F  /\ Disj  x  e. 
ran  F { x } )  -> Disj  x  e. 
ran  F ( `' F " { x } ) )
262259, 260, 261sylancl 644 . . . . . . . . . . . 12  |-  ( ph  -> Disj  x  e.  ran  F ( `' F " { x } ) )
263 ffun 5552 . . . . . . . . . . . . . 14  |-  ( G : U. dom  M --> U. J  ->  Fun  G
)
26420, 263syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  Fun  G )
265 sndisj 4164 . . . . . . . . . . . . 13  |- Disj  y  e. 
ran  G { y }
266 disjpreima 23979 . . . . . . . . . . . . 13  |-  ( ( Fun  G  /\ Disj  y  e. 
ran  G { y } )  -> Disj  y  e. 
ran  G ( `' G " { y } ) )
267264, 265, 266sylancl 644 . . . . . . . . . . . 12  |-  ( ph  -> Disj  y  e.  ran  G ( `' G " { y } ) )
268 sneq 3785 . . . . . . . . . . . . . 14  |-  ( x  =  ( 1st `  p
)  ->  { x }  =  { ( 1st `  p ) } )
269268imaeq2d 5162 . . . . . . . . . . . . 13  |-  ( x  =  ( 1st `  p
)  ->  ( `' F " { x }
)  =  ( `' F " { ( 1st `  p ) } ) )
270 sneq 3785 . . . . . . . . . . . . . 14  |-  ( y  =  ( 2nd `  p
)  ->  { y }  =  { ( 2nd `  p ) } )
271270imaeq2d 5162 . . . . . . . . . . . . 13  |-  ( y  =  ( 2nd `  p
)  ->  ( `' G " { y } )  =  ( `' G " { ( 2nd `  p ) } ) )
272 simpl 444 . . . . . . . . . . . . 13  |-  ( (Disj  x  e.  ran  F ( `' F " { x } )  /\ Disj  y  e. 
ran  G ( `' G " { y } ) )  -> Disj  x  e.  ran  F ( `' F " { x } ) )
273 simpr 448 . . . . . . . . . . . . 13  |-  ( (Disj  x  e.  ran  F ( `' F " { x } )  /\ Disj  y  e. 
ran  G ( `' G " { y } ) )  -> Disj  y  e.  ran  G ( `' G " { y } ) )
274269, 271, 272, 273disjxpin 23981 . . . . . . . . . . . 12  |-  ( (Disj  x  e.  ran  F ( `' F " { x } )  /\ Disj  y  e. 
ran  G ( `' G " { y } ) )  -> Disj  p  e.  ( ran  F  X.  ran  G ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )
275262, 267, 274syl2anc 643 . . . . . . . . . . 11  |-  ( ph  -> Disj  p  e.  ( ran  F  X.  ran  G ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )
276 disjss1 4148 . . . . . . . . . . 11  |-  ( ( ( `'  .+  " {
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 ) } ) ) ) )
277185, 275, 276mpsyl 61 . . . . . . . . . 10  |-  ( ph  -> Disj  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G
) ) ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) ) )
278277adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  z  e.  ( ran  ( F  o F  .+  G )  \  { ( 0g `  K ) } ) )  -> Disj  p  e.  ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )
279257, 278jca 519 . . . . . . . 8  |-  ( (
ph  /\  z  e.  ( ran  ( F  o F  .+  G )  \  { ( 0g `  K ) } ) )  ->  ( (
( `'  .+  " {
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 ) } ) ) ) )
280 measvuni 24521 . . . . . . . 8  |-  ( ( 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
) } ) ) )  = Σ* p  e.  (
( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) ( M `  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) ) ) )
281253, 256, 279, 280syl3anc 1184 . . . . . . 7  |-  ( (
ph  /\  z  e.  ( ran  ( F  o F  .+  G )  \  { ( 0g `  K ) } ) )  ->  ( M `  U_ p  e.  ( ( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )  = Σ* p  e.  (
( `'  .+  " {
z } )  i^i  ( ran  F  X.  ran  G ) ) ( M `  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) ) ) )
282 ssfi 7288 . . . . . . . . . 10  |-  ( ( ( 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 )
283189, 185, 282sylancl 644 . . . . . . . . 9  |-  ( ph  ->  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) )  e.  Fin )
284283adantr 452 . . . . . . . 8  |-  ( (
ph  /\  z  e.  ( ran  ( F  o F  .+  G )  \  { ( 0g `  K ) } ) )  ->  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G
) )  e.  Fin )
285 iccssxr 10949 . . . . . . . . . . 11  |-  ( 0 [,]  +oo )  C_  RR*
286253adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  M  e.  (measures `  dom  M ) )
287255, 183sylanl2 633 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) )  e. 
dom  M )
288 measvxrge0 24512 . . . . . . . . . . . 12  |-  ( ( M  e.  (measures `  dom  M )  /\  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) )  e. 
dom  M )  -> 
( M `  (
( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )  e.  ( 0 [,]  +oo ) )
289286, 287, 288syl2anc 643 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  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 ) )
290285, 289sseldi 3306 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( M `  ( ( `' F " { ( 1st `  p
) } )  i^i  ( `' G " { ( 2nd `  p
) } ) ) )  e.  RR* )
291 measge0 24514 . . . . . . . . . . 11  |-  ( ( 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
) } ) ) ) )
292286, 287, 291syl2anc 643 . . . . . . . . . 10  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  0  <_  ( M `  ( ( `' F " { ( 1st `  p ) } )  i^i  ( `' G " { ( 2nd `  p ) } ) ) ) )
293 simpl 444 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( ph  /\  z  e.  ( ran  ( F  o F 
.+  G )  \  { ( 0g `  K ) } ) ) )
294 simpr 448 . . . . . . . . . . 11  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )
295255, 140sylanl2 633 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ph )
296185, 294sseldi 3306 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  p  e.  ( ran  F  X.  ran  G ) )
297 xp1st 6335 . . . . . . . . . . . . . . . . . 18  |-  ( p  e.  ( ran  F  X.  ran  G )  -> 
( 1st `  p
)  e.  ran  F
)
298296, 297syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( 1st `  p )  e.  ran  F )
299298orcd 382 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( ( 1st `  p )  e. 
ran  F  \/  ( 2nd `  p )  e. 
ran  G ) )
300298orcd 382 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( ( 1st `  p )  e. 
ran  F  \/  -.  ( 2nd `  p )  e.  {  .0.  }
) )
301299, 300jca 519 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( (
( 1st `  p
)  e.  ran  F  \/  ( 2nd `  p
)  e.  ran  G
)  /\  ( ( 1st `  p )  e. 
ran  F  \/  -.  ( 2nd `  p )  e.  {  .0.  }
) ) )
302 xp2nd 6336 . . . . . . . . . . . . . . . . . 18  |-  ( p  e.  ( ran  F  X.  ran  G )  -> 
( 2nd `  p
)  e.  ran  G
)
303296, 302syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( 2nd `  p )  e.  ran  G )
304303olcd 383 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( -.  ( 1st `  p )  e.  {  .0.  }  \/  ( 2nd `  p
)  e.  ran  G
) )
305 oveq12 6049 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  =  .0.  /\  y  =  .0.  )  ->  ( x  .+  y
)  =  (  .0.  .+  .0.  ) )
306305adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( x  =  .0.  /\  y  =  .0.  ) )  -> 
( x  .+  y
)  =  (  .0.  .+  .0.  ) )
307 sibfof.5 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  (  .0.  .+  .0.  )  =  ( 0g `  K ) )
308307adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( x  =  .0.  /\  y  =  .0.  ) )  -> 
(  .0.  .+  .0.  )  =  ( 0g `  K ) )
309306, 308eqtrd 2436 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( x  =  .0.  /\  y  =  .0.  ) )  -> 
( x  .+  y
)  =  ( 0g
`  K ) )
310309ex 424 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( x  =  .0.  /\  y  =  .0.  )  ->  (
x  .+  y )  =  ( 0g `  K ) ) )
311310necon3ad 2603 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( x  .+  y )  =/=  ( 0g `  K )  ->  -.  ( x  =  .0. 
/\  y  =  .0.  ) ) )
312 oran 483 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( x  =/=  .0.  \/  y  =/=  .0.  )  <->  -.  ( -.  x  =/=  .0.  /\ 
-.  y  =/=  .0.  ) )
313 nne 2571 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  x  =/=  .0.  <->  x  =  .0.  )
314 nne 2571 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( -.  y  =/=  .0.  <->  y  =  .0.  )
315313, 314anbi12i 679 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( -.  x  =/=  .0.  /\ 
-.  y  =/=  .0.  ) 
<->  ( x  =  .0. 
/\  y  =  .0.  ) )
316315notbii 288 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  ( -.  x  =/= 
.0.  /\  -.  y  =/=  .0.  )  <->  -.  (
x  =  .0.  /\  y  =  .0.  )
)
317312, 316bitri 241 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  =/=  .0.  \/  y  =/=  .0.  )  <->  -.  (
x  =  .0.  /\  y  =  .0.  )
)
318311, 317syl6ibr 219 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( x  .+  y )  =/=  ( 0g `  K )  -> 
( x  =/=  .0.  \/  y  =/=  .0.  ) ) )
319318adantr 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( x  e.  B  /\  y  e.  B ) )  -> 
( ( x  .+  y )  =/=  ( 0g `  K )  -> 
( x  =/=  .0.  \/  y  =/=  .0.  ) ) )
320319ralrimivva 2758 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. x  e.  B  A. y  e.  B  ( ( x  .+  y )  =/=  ( 0g `  K )  -> 
( x  =/=  .0.  \/  y  =/=  .0.  ) ) )
321295, 320syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  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.  ) ) )
322141a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  z  e.  ( ran  ( F  o F  .+  G )  \  { ( 0g `  K ) } ) )  ->  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G
) )  C_  ( `'  .+  " { z } ) )
323322sselda 3308 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  p  e.  ( `'  .+  " {
z } ) )
324295, 71syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  .+  Fn  ( B  X.  B ) )
325 fniniseg 5810 . . . . . . . . . . . . . . . . . . . . . 22  |-  (  .+  Fn  ( B  X.  B
)  ->  ( p  e.  ( `'  .+  " {
z } )  <->  ( p  e.  ( B  X.  B
)  /\  (  .+  `  p )  =  z ) ) )
326324, 325syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( p  e.  ( `'  .+  " {
z } )  <->  ( p  e.  ( B  X.  B
)  /\  (  .+  `  p )  =  z ) ) )
327323, 326mpbid 202 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( p  e.  ( B  X.  B
)  /\  (  .+  `  p )  =  z ) )
328 simpr 448 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( p  e.  ( B  X.  B )  /\  (  .+  `  p )  =  z )  -> 
(  .+  `  p )  =  z )
32988fveq2d 5691 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( p  e.  ( B  X.  B )  ->  (  .+  `  p )  =  (  .+  `  <. ( 1st `  p ) ,  ( 2nd `  p
) >. ) )
330 df-ov 6043 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1st `  p ) 
.+  ( 2nd `  p
) )  =  ( 
.+  `  <. ( 1st `  p ) ,  ( 2nd `  p )
>. )
331329, 330syl6eqr 2454 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  e.  ( B  X.  B )  ->  (  .+  `  p )  =  ( ( 1st `  p
)  .+  ( 2nd `  p ) ) )
332331adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( p  e.  ( B  X.  B )  /\  (  .+  `  p )  =  z )  -> 
(  .+  `  p )  =  ( ( 1st `  p )  .+  ( 2nd `  p ) ) )
333328, 332eqtr3d 2438 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( p  e.  ( B  X.  B )  /\  (  .+  `  p )  =  z )  -> 
z  =  ( ( 1st `  p ) 
.+  ( 2nd `  p
) ) )
334327, 333syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  z  =  ( ( 1st `  p
)  .+  ( 2nd `  p ) ) )
335 simplr 732 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  z  e.  ( ran  ( F  o F  .+  G )  \  { ( 0g `  K ) } ) )
336335eldifbd 3293 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  -.  z  e.  { ( 0g `  K ) } )
337 elsn 3789 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  { ( 0g
`  K ) }  <-> 
z  =  ( 0g
`  K ) )
338337necon3bbii 2598 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  z  e.  { ( 0g `  K ) }  <->  z  =/=  ( 0g `  K ) )
339336, 338sylib 189 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  z  =/=  ( 0g `  K ) )
340334, 339eqnetrrd 2587 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( ( 1st `  p )  .+  ( 2nd `  p ) )  =/=  ( 0g
`  K ) )
341255, 144sylanl2 633 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  p  e.  ( B  X.  B
) )
342341, 160syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( 1st `  p )  e.  B
)
343341, 173syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( 2nd `  p )  e.  B
)
344 oveq1 6047 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( 1st `  p
)  ->  ( x  .+  y )  =  ( ( 1st `  p
)  .+  y )
)
345344neeq1d 2580 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( 1st `  p
)  ->  ( (
x  .+  y )  =/=  ( 0g `  K
)  <->  ( ( 1st `  p )  .+  y
)  =/=  ( 0g
`  K ) ) )
346 neeq1 2575 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( 1st `  p
)  ->  ( x  =/=  .0.  <->  ( 1st `  p
)  =/=  .0.  )
)
347346orbi1d 684 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  ( 1st `  p
)  ->  ( (
x  =/=  .0.  \/  y  =/=  .0.  )  <->  ( ( 1st `  p )  =/= 
.0.  \/  y  =/=  .0.  ) ) )
348345, 347imbi12d 312 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  ( 1st `  p
)  ->  ( (
( x  .+  y
)  =/=  ( 0g
`  K )  -> 
( x  =/=  .0.  \/  y  =/=  .0.  ) )  <->  ( (
( 1st `  p
)  .+  y )  =/=  ( 0g `  K
)  ->  ( ( 1st `  p )  =/= 
.0.  \/  y  =/=  .0.  ) ) ) )
349 oveq2 6048 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( 2nd `  p
)  ->  ( ( 1st `  p )  .+  y )  =  ( ( 1st `  p
)  .+  ( 2nd `  p ) ) )
350349neeq1d 2580 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( 2nd `  p
)  ->  ( (
( 1st `  p
)  .+  y )  =/=  ( 0g `  K
)  <->  ( ( 1st `  p )  .+  ( 2nd `  p ) )  =/=  ( 0g `  K ) ) )
351 neeq1 2575 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( 2nd `  p
)  ->  ( y  =/=  .0.  <->  ( 2nd `  p
)  =/=  .0.  )
)
352351orbi2d 683 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( 2nd `  p
)  ->  ( (
( 1st `  p
)  =/=  .0.  \/  y  =/=  .0.  )  <->  ( ( 1st `  p )  =/= 
.0.  \/  ( 2nd `  p )  =/=  .0.  ) ) )
353350, 352imbi12d 312 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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.  ) ) ) )
354348, 353rspc2v 3018 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 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.  ) ) ) )
355342, 343, 354syl2anc 643 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  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.  ) ) ) )
356321, 340, 355mp2d 43 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( ( 1st `  p )  =/= 
.0.  \/  ( 2nd `  p )  =/=  .0.  ) )
357 fvex 5701 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1st `  p )  e.  _V
358357elsnc 3797 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1st `  p )  e.  {  .0.  }  <->  ( 1st `  p )  =  .0.  )
359358necon3bbii 2598 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( 1st `  p
)  e.  {  .0.  }  <-> 
( 1st `  p
)  =/=  .0.  )
360 fvex 5701 . . . . . . . . . . . . . . . . . . . 20  |-  ( 2nd `  p )  e.  _V
361360elsnc 3797 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2nd `  p )  e.  {  .0.  }  <->  ( 2nd `  p )  =  .0.  )
362361necon3bbii 2598 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( 2nd `  p
)  e.  {  .0.  }  <-> 
( 2nd `  p
)  =/=  .0.  )
363359, 362orbi12i 508 . . . . . . . . . . . . . . . . 17  |-  ( ( -.  ( 1st `  p
)  e.  {  .0.  }  \/  -.  ( 2nd `  p )  e.  {  .0.  } )  <->  ( ( 1st `  p )  =/= 
.0.  \/  ( 2nd `  p )  =/=  .0.  ) )
364356, 363sylibr 204 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( -.  ( 1st `  p )  e.  {  .0.  }  \/  -.  ( 2nd `  p
)  e.  {  .0.  } ) )
365304, 364jca 519 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( ( -.  ( 1st `  p
)  e.  {  .0.  }  \/  ( 2nd `  p
)  e.  ran  G
)  /\  ( -.  ( 1st `  p )  e.  {  .0.  }  \/  -.  ( 2nd `  p
)  e.  {  .0.  } ) ) )
366301, 365jca 519 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( (
( ( 1st `  p
)  e.  ran  F  \/  ( 2nd `  p
)  e.  ran  G
)  /\  ( ( 1st `  p )  e. 
ran  F  \/  -.  ( 2nd `  p )  e.  {  .0.  }
) )  /\  (
( -.  ( 1st `  p )  e.  {  .0.  }  \/  ( 2nd `  p )  e.  ran  G )  /\  ( -.  ( 1st `  p
)  e.  {  .0.  }  \/  -.  ( 2nd `  p )  e.  {  .0.  } ) ) ) )
367 orddi 840 . . . . . . . . . . . . . 14  |-  ( ( ( ( 1st `  p
)  e.  ran  F  /\  -.  ( 1st `  p
)  e.  {  .0.  } )  \/  ( ( 2nd `  p )  e.  ran  G  /\  -.  ( 2nd `  p
)  e.  {  .0.  } ) )  <->  ( (
( ( 1st `  p
)  e.  ran  F  \/  ( 2nd `  p
)  e.  ran  G
)  /\  ( ( 1st `  p )  e. 
ran  F  \/  -.  ( 2nd `  p )  e.  {  .0.  }
) )  /\  (
( -.  ( 1st `  p )  e.  {  .0.  }  \/  ( 2nd `  p )  e.  ran  G )  /\  ( -.  ( 1st `  p
)  e.  {  .0.  }  \/  -.  ( 2nd `  p )  e.  {  .0.  } ) ) ) )
368366, 367sylibr 204 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( (
( 1st `  p
)  e.  ran  F  /\  -.  ( 1st `  p
)  e.  {  .0.  } )  \/  ( ( 2nd `  p )  e.  ran  G  /\  -.  ( 2nd `  p
)  e.  {  .0.  } ) ) )
369 eldif 3290 . . . . . . . . . . . . . 14  |-  ( ( 1st `  p )  e.  ( ran  F  \  {  .0.  } )  <-> 
( ( 1st `  p
)  e.  ran  F  /\  -.  ( 1st `  p
)  e.  {  .0.  } ) )
370 eldif 3290 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  p )  e.  ( ran  G  \  {  .0.  } )  <-> 
( ( 2nd `  p
)  e.  ran  G  /\  -.  ( 2nd `  p
)  e.  {  .0.  } ) )
371369, 370orbi12i 508 . . . . . . . . . . . . 13  |-  ( ( ( 1st `  p
)  e.  ( ran 
F  \  {  .0.  } )  \/  ( 2nd `  p )  e.  ( ran  G  \  {  .0.  } ) )  <->  ( (
( 1st `  p
)  e.  ran  F  /\  -.  ( 1st `  p
)  e.  {  .0.  } )  \/  ( ( 2nd `  p )  e.  ran  G  /\  -.  ( 2nd `  p
)  e.  {  .0.  } ) ) )
372368, 371sylibr 204 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  z  e.  ( ran  ( F  o F  .+  G
)  \  { ( 0g `  K ) } ) )  /\  p  e.  ( ( `'  .+  " { z } )  i^i  ( ran  F  X.  ran  G ) ) )  ->  ( ( 1st `  p )  e.  ( ran  F  \  {  .0.  } )  \/  ( 2nd `  p
)  e.  ( ran 
G  \  {  .0.  } ) ) )
3733, 4, 11, 12, 13, 14, 15, 16, 17sibfima 24606 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( 1st `  p )  e.  ( ran  F  \  {  .0.  } ) )  -> 
( M `  ( `' F " { ( 1st `  p ) } ) )  e.  ( 0 [,)  +oo ) )
374 0re 9047 . . . . . . . . . . . . . . . . . 18  |-  0  e.  RR
375 pnfxr 10669 . . . . . . . . . . . . . . . . . 18  |-  +oo  e.  RR*
376 elico2 10930 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
( M `  ( `' F " { ( 1st `  p ) } ) )  e.  ( 0 [,)  +oo ) 
<->  ( ( M `  ( `' F " {