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.

Step	Hyp	Ref	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 )
5	3, 4	tpsuni 16958	. . . . . . . . . . . . 13 |- ( W e. TopSp -> B = U. J )
6	2, 5	syl 16	. . . . . . . . . . . 12 |- ( ph -> B = U. J )
7	6, 6	xpeq12d 4862	. . . . . . . . . . 11 |- ( ph -> ( B X. B ) = ( U. J X. U. J ) )
8	7	feq2d 5540	. . . . . . . . . 10 |- ( ph -> ( .+ : ( B X. B ) --> C <-> .+ : ( U. J X. U. J ) --> C ) )
9	1, 8	mpbid 202	. . . . . . . . 9 |- ( ph -> .+ : ( U. J X. U. J ) --> C )
10	9	fovrnda 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 ) )
18	3, 4, 11, 12, 13, 14, 15, 16, 17	sibff 24604	. . . . . . . 8 |- ( ph -> F : U. dom M --> U. J )
19		sibfof.2	. . . . . . . . 9 |- ( ph -> G e. dom ( Wsitg M ) )
20	3, 4, 11, 12, 13, 14, 15, 16, 19	sibff 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 )
23	16, 21, 22	3syl 19	. . . . . . . 8 |- ( ph -> U. dom M e. _V )
24		inidm 3510	. . . . . . . 8 |- ( U. dom M i^i U. dom M ) = U. dom M
25	10, 18, 20, 23, 23, 24	off 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 )
29	27, 28	tpsuni 16958	. . . . . . . . . 10 |- ( K e. TopSp -> C = U. ( TopOpen ` K ) )
30	26, 29	syl 16	. . . . . . . . 9 |- ( ph -> C = U. ( TopOpen ` K ) )
31		eqid 2404	. . . . . . . . . . 11 |- (sigaGen ` ( TopOpen ` K ) ) = (sigaGen ` ( TopOpen ` K ) )
32	31	unieqi 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 ) )
35	33, 34	ax-mp 8	. . . . . . . . . 10 |- U. (sigaGen ` ( TopOpen ` K ) ) = U. ( TopOpen ` K )
36	32, 35	eqtri 2424	. . . . . . . . 9 |- U. (sigaGen ` ( TopOpen ` K ) ) = U. ( TopOpen ` K )
37	30, 36	syl6eqr 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 ) ) ) )
39	37, 38	syl 16	. . . . . . 7 |- ( ph -> ( ( F o F .+ G ) : U. dom M --> C <-> ( F o F .+ G ) : U. dom M --> U. (sigaGen ` ( TopOpen ` K ) ) ) )
40	25, 39	mpbid 202	. . . . . 6 |- ( ph -> ( F o F .+ G ) : U. dom M --> U. (sigaGen ` ( TopOpen ` K ) ) )
41	33	a1i 11	. . . . . . . . . 10 |- ( ph -> ( TopOpen ` K ) e. _V )
42	41	sgsiga 24478	. . . . . . . . 9 |- ( ph -> (sigaGen ` ( TopOpen ` K ) ) e. U. ran sigAlgebra )
43	31, 42	syl5eqel 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 )
45	43, 44	syl 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 ) ) ) )
47	45, 23, 46	syl2anc 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 ) ) ) )
48	40, 47	mpbird 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
50	49	imaeq2i 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 ) ) ) ) )
53	25, 51, 52	3syl 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 ) ) ) ) )
54	53	adantr 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 ) ) ) ) )
55	50, 54	syl5eqr 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 )
57	16, 56	syl 16	. . . . . . . . 9 |- ( ph -> dom M e. U. ran sigAlgebra )
58	57	adantr 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 ) )
61	60	imaeq2i 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 ) ) )
62	59, 61	eqtr3i 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 ) )
65	6, 64	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( F : U. dom M --> B <-> F : U. dom M --> U. J ) )
66	18, 65	mpbird 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 ) )
68	6, 67	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( G : U. dom M --> B <-> G : U. dom M --> U. J ) )
69	20, 68	mpbird 224	. . . . . . . . . . . . . . . . . 18 |- ( ph -> G : U. dom M --> B )
70		ffn 5550	. . . . . . . . . . . . . . . . . . 19 |- ( .+ : ( B X. B ) --> C -> .+ Fn ( B X. B ) )
71	1, 70	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> .+ Fn ( B X. B ) )
72	66, 69, 23, 71	ofpreima 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 ) } ) ) )
75	73, 74	ax-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 ) } ) ) )
77	75, 76	eqtr3i 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 ) } ) ) )
78	72, 77	syl6eq 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 ) ) )
80	79	eldifbd 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 ) )
84	1, 83	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ph -> dom .+ = ( B X. B ) )
85	82, 84	syl5sseq 3356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> ( `' .+ " { z } ) C_ ( B X. B ) )
86	81, 85	sstrd 3318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( ( `' .+ " { z } ) \ ( ran F X. ran G ) ) C_ ( B X. B ) )
87	86	sselda 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 ) ) )
90	89	biimpri 198	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( p = <. ( 1st ` p ) , ( 2nd ` p ) >. /\ ( ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) ) -> p e. ( ran F X. ran G ) )
91	90	ex 424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( p = <. ( 1st ` p ) , ( 2nd ` p ) >. -> ( ( ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) -> p e. ( ran F X. ran G ) ) )
92	87, 88, 91	3syl 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 ) ) )
93	92	con3d 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 ) ) )
94	80, 93	mpd 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 ) )
96	94, 95	sylib 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 )
99	97, 98	orbi12i 508	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ran F i^i { ( 1st ` p ) } ) = (/) \/ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) <-> ( -. ( 1st ` p ) e. ran F \/ -. ( 2nd ` p ) e. ran G ) )
100	96, 99	sylibr 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 )
102	18, 101	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> F Fn U. dom M )
103		dffn3 5557	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( F Fn U. dom M <-> F : U. dom M --> ran F )
104	102, 103	sylib 189	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> F : U. dom M --> ran F )
105	104	adantr 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 )
107	20, 106	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> G Fn U. dom M )
108		dffn3 5557	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( G Fn U. dom M <-> G : U. dom M --> ran G )
109	107, 108	sylib 189	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> G : U. dom M --> ran G )
110	109	adantr 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 (/) ) = (/)
115	113, 114	eqtri 2424	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( (/) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/)
116	112, 115	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( `' F " { ( 1st ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) )
117	111, 116	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( F : U. dom M --> ran F /\ ( ran F i^i { ( 1st ` p ) } ) = (/) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) )
118	117	ex 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 (/) ) = (/)
122	120, 121	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( `' G " { ( 2nd ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) )
123	119, 122	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( G : U. dom M --> ran G /\ ( ran G i^i { ( 2nd ` p ) } ) = (/) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) )
124	123	ex 424	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( G : U. dom M --> ran G -> ( ( ran G i^i { ( 2nd ` p ) } ) = (/) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) ) )
125	118, 124	jaao 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 ) } ) ) = (/) ) )
126	105, 110, 125	syl2anc 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 ) } ) ) = (/) ) )
127	100, 126	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ p e. ( ( `' .+ " { z } ) \ ( ran F X. ran G ) ) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) )
128	127	ralrimiva 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 ) ) (/) )
130	128, 129	syl 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 ) ) (/) = (/)
132	130, 131	syl6eq 2452	. . . . . . . . . . . . . . . . . 18 |- ( ph -> U_ p e. ( ( `' .+ " { z } ) \ ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) = (/) )
133	132	uneq2d 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 ) } ) )
135	133, 134	syl6eq 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 ) } ) ) )
136	78, 135	eqtrd 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 ) } ) ) )
137	136	adantr 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 ) } ) ) )
138	57	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ z e. ran ( F o F .+ G ) ) -> dom M e. U. ran sigAlgebra )
139	57	ad2antrr 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 } )
142	85	adantr 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ z e. ran ( F o F .+ G ) ) -> ( `' .+ " { z } ) C_ ( B X. B ) )
143	141, 142	syl5ss 3319	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ z e. ran ( F o F .+ G ) ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) C_ ( B X. B ) )
144	143	sselda 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 ) )
145	57	adantr 452	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( B X. B ) ) -> dom M e. U. ran sigAlgebra )
146		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( TopOpen ` W ) e. _V
147	4, 146	eqeltri 2474	. . . . . . . . . . . . . . . . . . . . . . 23 |- J e. _V
148	147	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> J e. _V )
149	148	sgsiga 24478	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> (sigaGen ` J ) e. U. ran sigAlgebra )
150	11, 149	syl5eqel 2488	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> S e. U. ran sigAlgebra )
151	150	adantr 452	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( B X. B ) ) -> S e. U. ran sigAlgebra )
152	3, 4, 11, 12, 13, 14, 15, 16, 17	sibfmbl 24603	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> F e. ( dom MMblFnM S ) )
153	152	adantr 452	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( B X. B ) ) -> F e. ( dom MMblFnM S ) )
154	4	tpstop 16959	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( W e. TopSp -> J e. Top )
155		cldssbrsiga 24494	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( J e. Top -> ( Clsd ` J ) C_ (sigaGen ` J ) )
156	2, 154, 155	3syl 19	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> ( Clsd ` J ) C_ (sigaGen ` J ) )
157	156	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ p e. ( B X. B ) ) -> ( Clsd ` J ) C_ (sigaGen ` J ) )
158		sibfof.4	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> J e. Fre )
159	158	adantr 452	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ p e. ( B X. B ) ) -> J e. Fre )
160		xp1st 6335	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( p e. ( B X. B ) -> ( 1st ` p ) e. B )
161	160	adantl 453	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ p e. ( B X. B ) ) -> ( 1st ` p ) e. B )
162	6	adantr 452	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ p e. ( B X. B ) ) -> B = U. J )
163	161, 162	eleqtrd 2480	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ p e. ( B X. B ) ) -> ( 1st ` p ) e. U. J )
164		eqid 2404	. . . . . . . . . . . . . . . . . . . . . . 23 |- U. J = U. J
165	164	t1sncld 17344	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( J e. Fre /\ ( 1st ` p ) e. U. J ) -> { ( 1st ` p ) } e. ( Clsd ` J ) )
166	159, 163, 165	syl2anc 643	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ p e. ( B X. B ) ) -> { ( 1st ` p ) } e. ( Clsd ` J ) )
167	157, 166	sseldd 3309	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ p e. ( B X. B ) ) -> { ( 1st ` p ) } e. (sigaGen ` J ) )
168	167, 11	syl6eleqr 2495	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( B X. B ) ) -> { ( 1st ` p ) } e. S )
169	145, 151, 153, 168	mbfmcnvima 24560	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. ( B X. B ) ) -> ( `' F " { ( 1st ` p ) } ) e. dom M )
170	140, 144, 169	syl2anc 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 )
171	3, 4, 11, 12, 13, 14, 15, 16, 19	sibfmbl 24603	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> G e. ( dom MMblFnM S ) )
172	171	adantr 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 )
174	173	adantl 453	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ p e. ( B X. B ) ) -> ( 2nd ` p ) e. B )
175	174, 162	eleqtrd 2480	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ p e. ( B X. B ) ) -> ( 2nd ` p ) e. U. J )
176	164	t1sncld 17344	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( J e. Fre /\ ( 2nd ` p ) e. U. J ) -> { ( 2nd ` p ) } e. ( Clsd ` J ) )
177	159, 175, 176	syl2anc 643	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ p e. ( B X. B ) ) -> { ( 2nd ` p ) } e. ( Clsd ` J ) )
178	157, 177	sseldd 3309	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ p e. ( B X. B ) ) -> { ( 2nd ` p ) } e. (sigaGen ` J ) )
179	178, 11	syl6eleqr 2495	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( B X. B ) ) -> { ( 2nd ` p ) } e. S )
180	145, 151, 172, 179	mbfmcnvima 24560	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. ( B X. B ) ) -> ( `' G " { ( 2nd ` p ) } ) e. dom M )
181	140, 144, 180	syl2anc 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 )
183	139, 170, 181, 182	syl3anc 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 )
184	183	ralrimiva 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 )
186	3, 4, 11, 12, 13, 14, 15, 16, 17	sibfrn 24605	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ran F e. Fin )
187	3, 4, 11, 12, 13, 14, 15, 16, 19	sibfrn 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 )
189	186, 187, 188	syl2anc 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 ) ) )
191	189, 190	syl 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 ) ) )
192	185, 191	mpi 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 )
194	193	biimpi 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 )
196	189, 194, 195	3syl 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 )
198	192, 196, 197	syl2anc 643	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ om )
199	198	adantr 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 ) )
201	200	sigaclcuni 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 )
202	138, 184, 199, 201	syl3anc 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 )
203	137, 202	eqeltrd 2478	. . . . . . . . . . . . 13 |- ( ( ph /\ z e. ran ( F o F .+ G ) ) -> ( `' ( F o F .+ G ) " { z } ) e. dom M )
204	203	ralrimiva 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 ) )
206	63, 204, 205	mpsyl 61	. . . . . . . . . . 11 |- ( ph -> A. z e. ( b i^i ran ( F o F .+ G ) ) ( `' ( F o F .+ G ) " { z } ) e. dom M )
207	206	adantr 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 .+ )
209	1, 208	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> Fun .+ )
210		imafi 7357	. . . . . . . . . . . . . . . 16 |- ( ( Fun .+ /\ ( ran F X. ran G ) e. Fin ) -> ( .+ " ( ran F X. ran G ) ) e. Fin )
211	209, 189, 210	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ph -> ( .+ " ( ran F X. ran G ) ) e. Fin )
212	18, 20, 9, 23	ofrn2 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 )
214	211, 212, 213	syl2anc 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 ) ) )
216	214, 215	syl 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 ) ) )
217	63, 216	mpi 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 )
219	214, 218	sylib 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 )
221	219, 220	syl 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 )
223	217, 221, 222	syl2anc 643	. . . . . . . . . . 11 |- ( ph -> ( b i^i ran ( F o F .+ G ) ) ~<_ om )
224	223	adantr 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 ) )
226	225	sigaclcuni 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 )
227	58, 207, 224, 226	syl3anc 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 )
228	62, 227	syl5eqelr 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 ) ) ) )
230	25, 51, 229	3syl 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 )
232	231	difeq2i 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 ) ) = (/) )
235	233, 234	mpbi 200	. . . . . . . . . . . 12 |- ( ( `' ( F o F .+ G ) " b ) \ dom ( F o F .+ G ) ) = (/)
236	232, 235	eqtri 2424	. . . . . . . . . . 11 |- ( ( `' ( F o F .+ G ) " b ) \ ( `' ( F o F .+ G ) " ran ( F o F .+ G ) ) ) = (/)
237	230, 236	syl6eq 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 )
239	57, 238	syl 16	. . . . . . . . . 10 |- ( ph -> (/) e. dom M )
240	237, 239	eqeltrd 2478	. . . . . . . . 9 |- ( ph -> ( `' ( F o F .+ G ) " ( b \ ran ( F o F .+ G ) ) ) e. dom M )
241	240	adantr 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 )
243	58, 228, 241, 242	syl3anc 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 )
244	55, 243	eqeltrd 2478	. . . . . 6 |- ( ( ph /\ b e. (sigaGen ` ( TopOpen ` K ) ) ) -> ( `' ( F o F .+ G ) " b ) e. dom M )
245	244	ralrimiva 2749	. . . . 5 |- ( ph -> A. b e. (sigaGen ` ( TopOpen ` K ) ) ( `' ( F o F .+ G ) " b ) e. dom M )
246	48, 245	jca 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 ) )
247	57, 43	ismbfm 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 ) ) )
248	246, 247	mpbird 224	. . 3 |- ( ph -> ( F o F .+ G ) e. ( dom MMblFnM (sigaGen ` ( TopOpen ` K ) ) ) )
249	136	adantr 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 ) } ) ) )
250	249	fveq2d 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 ) )
252	16, 251	sylib 189	. . . . . . . . 9 |- ( ph -> M e. (measures ` dom M ) )
253	252	adantr 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 )
255	254	sseli 3304	. . . . . . . . 9 |- ( z e. ( ran ( F o F .+ G ) \ { ( 0g ` K ) } ) -> z e. ran ( F o F .+ G ) )
256	255, 184	sylan2 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 )
257	198	adantr 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 )
259	18, 258	syl 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 } ) )
262	259, 260, 261	sylancl 644	. . . . . . . . . . . 12 |- ( ph -> Disj x e. ran F ( `' F " { x } ) )
263		ffun 5552	. . . . . . . . . . . . . 14 |- ( G : U. dom M --> U. J -> Fun G )
264	20, 263	syl 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 } ) )
267	264, 265, 266	sylancl 644	. . . . . . . . . . . 12 |- ( ph -> Disj y e. ran G ( `' G " { y } ) )
268		sneq 3785	. . . . . . . . . . . . . 14 |- ( x = ( 1st ` p ) -> { x } = { ( 1st ` p ) } )
269	268	imaeq2d 5162	. . . . . . . . . . . . 13 |- ( x = ( 1st ` p ) -> ( `' F " { x } ) = ( `' F " { ( 1st ` p ) } ) )
270		sneq 3785	. . . . . . . . . . . . . 14 |- ( y = ( 2nd ` p ) -> { y } = { ( 2nd ` p ) } )
271	270	imaeq2d 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 } ) )
274	269, 271, 272, 273	disjxpin 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 ) } ) ) )
275	262, 267, 274	syl2anc 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 ) } ) ) ) )
277	185, 275, 276	mpsyl 61	. . . . . . . . . 10 |- ( ph -> Disj p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
278	277	adantr 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 ) } ) ) )
279	257, 278	jca 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 ) } ) ) ) )
281	253, 256, 279, 280	syl3anc 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 )
283	189, 185, 282	sylancl 644	. . . . . . . . 9 |- ( ph -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) e. Fin )
284	283	adantr 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*
286	253	adantr 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 ) )
287	255, 183	sylanl2 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 ) )
289	286, 287, 288	syl2anc 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 ) )
290	285, 289	sseldi 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 ) } ) ) ) )
292	286, 287, 291	syl2anc 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 ) ) )
295	255, 140	sylanl2 633	. . . . . . . . . . . 12 |- ( ( ( ph /\ z e. ( ran ( F o F .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ph )
296	185, 294	sseldi 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 )
298	296, 297	syl 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 )
299	298	orcd 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 ) )
300	298	orcd 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. } ) )
301	299, 300	jca 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 )
303	296, 302	syl 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 )
304	303	olcd 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. ) )
306	305	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( x = .0. /\ y = .0. ) ) -> ( x .+ y ) = ( .0. .+ .0. ) )
307		sibfof.5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( .0. .+ .0. ) = ( 0g ` K ) )
308	307	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( x = .0. /\ y = .0. ) ) -> ( .0. .+ .0. ) = ( 0g ` K ) )
309	306, 308	eqtrd 2436	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( x = .0. /\ y = .0. ) ) -> ( x .+ y ) = ( 0g ` K ) )
310	309	ex 424	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> ( ( x = .0. /\ y = .0. ) -> ( x .+ y ) = ( 0g ` K ) ) )
311	310	necon3ad 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. )
315	313, 314	anbi12i 679	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( -. x =/= .0. /\ -. y =/= .0. ) <-> ( x = .0. /\ y = .0. ) )
316	315	notbii 288	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -. ( -. x =/= .0. /\ -. y =/= .0. ) <-> -. ( x = .0. /\ y = .0. ) )
317	312, 316	bitri 241	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x =/= .0. \/ y =/= .0. ) <-> -. ( x = .0. /\ y = .0. ) )
318	311, 317	syl6ibr 219	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) )
319	318	adantr 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) )
320	319	ralrimivva 2758	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> A. x e. B A. y e. B ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) )
321	295, 320	syl 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. ) ) )
322	141	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ z e. ( ran ( F o F .+ G ) \ { ( 0g ` K ) } ) ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) C_ ( `' .+ " { z } ) )
323	322	sselda 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 } ) )
324	295, 71	syl 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 ) ) )
326	324, 325	syl 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 ) ) )
327	323, 326	mpbid 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 )
329	88	fveq2d 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 ) >. )
331	329, 330	syl6eqr 2454	. . . . . . . . . . . . . . . . . . . . . 22 |- ( p e. ( B X. B ) -> ( .+ ` p ) = ( ( 1st ` p ) .+ ( 2nd ` p ) ) )
332	331	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) -> ( .+ ` p ) = ( ( 1st ` p ) .+ ( 2nd ` p ) ) )
333	328, 332	eqtr3d 2438	. . . . . . . . . . . . . . . . . . . 20 |- ( ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) -> z = ( ( 1st ` p ) .+ ( 2nd ` p ) ) )
334	327, 333	syl 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 ) } ) )
336	335	eldifbd 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 ) )
338	337	necon3bbii 2598	. . . . . . . . . . . . . . . . . . . 20 |- ( -. z e. { ( 0g ` K ) } <-> z =/= ( 0g ` K ) )
339	336, 338	sylib 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 ) )
340	334, 339	eqnetrrd 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 ) )
341	255, 144	sylanl2 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 ) )
342	341, 160	syl 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 )
343	341, 173	syl 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 ) )
345	344	neeq1d 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. ) )
347	346	orbi1d 684	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = ( 1st ` p ) -> ( ( x =/= .0. \/ y =/= .0. ) <-> ( ( 1st ` p ) =/= .0. \/ y =/= .0. ) ) )
348	345, 347	imbi12d 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 ) ) )
350	349	neeq1d 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. ) )
352	351	orbi2d 683	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( 2nd ` p ) -> ( ( ( 1st ` p ) =/= .0. \/ y =/= .0. ) <-> ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) ) )
353	350, 352	imbi12d 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. ) ) ) )
354	348, 353	rspc2v 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. ) ) ) )
355	342, 343, 354	syl2anc 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. ) ) ) )
356	321, 340, 355	mp2d 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
358	357	elsnc 3797	. . . . . . . . . . . . . . . . . . 19 |- ( ( 1st ` p ) e. { .0. } <-> ( 1st ` p ) = .0. )
359	358	necon3bbii 2598	. . . . . . . . . . . . . . . . . 18 |- ( -. ( 1st ` p ) e. { .0. } <-> ( 1st ` p ) =/= .0. )
360		fvex 5701	. . . . . . . . . . . . . . . . . . . 20 |- ( 2nd ` p ) e. _V
361	360	elsnc 3797	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2nd ` p ) e. { .0. } <-> ( 2nd ` p ) = .0. )
362	361	necon3bbii 2598	. . . . . . . . . . . . . . . . . 18 |- ( -. ( 2nd ` p ) e. { .0. } <-> ( 2nd ` p ) =/= .0. )
363	359, 362	orbi12i 508	. . . . . . . . . . . . . . . . 17 |- ( ( -. ( 1st ` p ) e. { .0. } \/ -. ( 2nd ` p ) e. { .0. } ) <-> ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) )
364	356, 363	sylibr 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. } ) )
365	304, 364	jca 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. } ) ) )
366	301, 365	jca 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. } ) ) ) )
368	366, 367	sylibr 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. } ) )
371	369, 370	orbi12i 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. } ) ) )
372	368, 371	sylibr 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. } ) ) )
373	3, 4, 11, 12, 13, 14, 15, 16, 17	sibfima 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 " {