Theorem sibfof 28155

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

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 oF .+ 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	. . . . . . . 8 |- ( ph -> .+ : ( B X. B ) --> C )
2		sibfof.0	. . . . . . . . . . 11 |- ( ph -> W e. TopSp )
3		sitgval.b	. . . . . . . . . . . 12 |- B = ( Base ` W )
4		sitgval.j	. . . . . . . . . . . 12 |- J = ( TopOpen ` W )
5	3, 4	tpsuni 19312	. . . . . . . . . . 11 |- ( W e. TopSp -> B = U. J )
6	2, 5	syl 16	. . . . . . . . . 10 |- ( ph -> B = U. J )
7	6	sqxpeqd 5015	. . . . . . . . 9 |- ( ph -> ( B X. B ) = ( U. J X. U. J ) )
8	7	feq2d 5708	. . . . . . . 8 |- ( ph -> ( .+ : ( B X. B ) --> C <-> .+ : ( U. J X. U. J ) --> C ) )
9	1, 8	mpbid 210	. . . . . . 7 |- ( ph -> .+ : ( U. J X. U. J ) --> C )
10	9	fovrnda 6431	. . . . . 6 |- ( ( ph /\ ( z e. U. J /\ x e. U. J ) ) -> ( z .+ x ) e. C )
11		sitgval.s	. . . . . . 7 |- S = (sigaGen ` J )
12		sitgval.0	. . . . . . 7 |- .0. = ( 0g ` W )
13		sitgval.x	. . . . . . 7 |- .x. = ( .s ` W )
14		sitgval.h	. . . . . . 7 |- H = (RRHom ` (Scalar ` W ) )
15		sitgval.1	. . . . . . 7 |- ( ph -> W e. V )
16		sitgval.2	. . . . . . 7 |- ( ph -> M e. U. ran measures )
17		sibfmbl.1	. . . . . . 7 |- ( ph -> F e. dom ( Wsitg M ) )
18	3, 4, 11, 12, 13, 14, 15, 16, 17	sibff 28151	. . . . . 6 |- ( ph -> F : U. dom M --> U. J )
19		sibfof.2	. . . . . . 7 |- ( ph -> G e. dom ( Wsitg M ) )
20	3, 4, 11, 12, 13, 14, 15, 16, 19	sibff 28151	. . . . . 6 |- ( ph -> G : U. dom M --> U. J )
21		dmexg 6716	. . . . . . 7 |- ( M e. U. ran measures -> dom M e. _V )
22		uniexg 6582	. . . . . . 7 |- ( dom M e. _V -> U. dom M e. _V )
23	16, 21, 22	3syl 20	. . . . . 6 |- ( ph -> U. dom M e. _V )
24		inidm 3692	. . . . . 6 |- ( U. dom M i^i U. dom M ) = U. dom M
25	10, 18, 20, 23, 23, 24	off 6539	. . . . 5 |- ( ph -> ( F oF .+ G ) : U. dom M --> C )
26		sibfof.3	. . . . . . . 8 |- ( ph -> K e. TopSp )
27		sibfof.c	. . . . . . . . 9 |- C = ( Base ` K )
28		eqid 2443	. . . . . . . . 9 |- ( TopOpen ` K ) = ( TopOpen ` K )
29	27, 28	tpsuni 19312	. . . . . . . 8 |- ( K e. TopSp -> C = U. ( TopOpen ` K ) )
30	26, 29	syl 16	. . . . . . 7 |- ( ph -> C = U. ( TopOpen ` K ) )
31		fvex 5866	. . . . . . . 8 |- ( TopOpen ` K ) e. _V
32		unisg 28016	. . . . . . . 8 |- ( ( TopOpen ` K ) e. _V -> U. (sigaGen ` ( TopOpen ` K ) ) = U. ( TopOpen ` K ) )
33	31, 32	ax-mp 5	. . . . . . 7 |- U. (sigaGen ` ( TopOpen ` K ) ) = U. ( TopOpen ` K )
34	30, 33	syl6eqr 2502	. . . . . 6 |- ( ph -> C = U. (sigaGen ` ( TopOpen ` K ) ) )
35	34	feq3d 5709	. . . . 5 |- ( ph -> ( ( F oF .+ G ) : U. dom M --> C <-> ( F oF .+ G ) : U. dom M --> U. (sigaGen ` ( TopOpen ` K ) ) ) )
36	25, 35	mpbid 210	. . . 4 |- ( ph -> ( F oF .+ G ) : U. dom M --> U. (sigaGen ` ( TopOpen ` K ) ) )
37	31	a1i 11	. . . . . . 7 |- ( ph -> ( TopOpen ` K ) e. _V )
38	37	sgsiga 28015	. . . . . 6 |- ( ph -> (sigaGen ` ( TopOpen ` K ) ) e. U. ran sigAlgebra )
39		uniexg 6582	. . . . . 6 |- ( (sigaGen ` ( TopOpen ` K ) ) e. U. ran sigAlgebra -> U. (sigaGen ` ( TopOpen ` K ) ) e. _V )
40	38, 39	syl 16	. . . . 5 |- ( ph -> U. (sigaGen ` ( TopOpen ` K ) ) e. _V )
41		elmapg 7435	. . . . 5 |- ( ( U. (sigaGen ` ( TopOpen ` K ) ) e. _V /\ U. dom M e. _V ) -> ( ( F oF .+ G ) e. ( U. (sigaGen ` ( TopOpen ` K ) ) ^m U. dom M ) <-> ( F oF .+ G ) : U. dom M --> U. (sigaGen ` ( TopOpen ` K ) ) ) )
42	40, 23, 41	syl2anc 661	. . . 4 |- ( ph -> ( ( F oF .+ G ) e. ( U. (sigaGen ` ( TopOpen ` K ) ) ^m U. dom M ) <-> ( F oF .+ G ) : U. dom M --> U. (sigaGen ` ( TopOpen ` K ) ) ) )
43	36, 42	mpbird 232	. . 3 |- ( ph -> ( F oF .+ G ) e. ( U. (sigaGen ` ( TopOpen ` K ) ) ^m U. dom M ) )
44		inundif 3892	. . . . . . 7 |- ( ( b i^i ran ( F oF .+ G ) ) u. ( b \ ran ( F oF .+ G ) ) ) = b
45	44	imaeq2i 5325	. . . . . 6 |- ( `' ( F oF .+ G ) " ( ( b i^i ran ( F oF .+ G ) ) u. ( b \ ran ( F oF .+ G ) ) ) ) = ( `' ( F oF .+ G ) " b )
46		ffun 5723	. . . . . . . 8 |- ( ( F oF .+ G ) : U. dom M --> C -> Fun ( F oF .+ G ) )
47		unpreima 5998	. . . . . . . 8 |- ( Fun ( F oF .+ G ) -> ( `' ( F oF .+ G ) " ( ( b i^i ran ( F oF .+ G ) ) u. ( b \ ran ( F oF .+ G ) ) ) ) = ( ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) u. ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) ) )
48	25, 46, 47	3syl 20	. . . . . . 7 |- ( ph -> ( `' ( F oF .+ G ) " ( ( b i^i ran ( F oF .+ G ) ) u. ( b \ ran ( F oF .+ G ) ) ) ) = ( ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) u. ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) ) )
49	48	adantr 465	. . . . . 6 |- ( ( ph /\ b e. (sigaGen ` ( TopOpen ` K ) ) ) -> ( `' ( F oF .+ G ) " ( ( b i^i ran ( F oF .+ G ) ) u. ( b \ ran ( F oF .+ G ) ) ) ) = ( ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) u. ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) ) )
50	45, 49	syl5eqr 2498	. . . . 5 |- ( ( ph /\ b e. (sigaGen ` ( TopOpen ` K ) ) ) -> ( `' ( F oF .+ G ) " b ) = ( ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) u. ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) ) )
51		dmmeas 28045	. . . . . . . 8 |- ( M e. U. ran measures -> dom M e. U. ran sigAlgebra )
52	16, 51	syl 16	. . . . . . 7 |- ( ph -> dom M e. U. ran sigAlgebra )
53	52	adantr 465	. . . . . 6 |- ( ( ph /\ b e. (sigaGen ` ( TopOpen ` K ) ) ) -> dom M e. U. ran sigAlgebra )
54		imaiun 6142	. . . . . . . 8 |- ( `' ( F oF .+ G ) " U_ z e. ( b i^i ran ( F oF .+ G ) ) { z } ) = U_ z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } )
55		iunid 4370	. . . . . . . . 9 |- U_ z e. ( b i^i ran ( F oF .+ G ) ) { z } = ( b i^i ran ( F oF .+ G ) )
56	55	imaeq2i 5325	. . . . . . . 8 |- ( `' ( F oF .+ G ) " U_ z e. ( b i^i ran ( F oF .+ G ) ) { z } ) = ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) )
57	54, 56	eqtr3i 2474	. . . . . . 7 |- U_ z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) = ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) )
58		inss2 3704	. . . . . . . . . 10 |- ( b i^i ran ( F oF .+ G ) ) C_ ran ( F oF .+ G )
59	6	feq3d 5709	. . . . . . . . . . . . . . 15 |- ( ph -> ( F : U. dom M --> B <-> F : U. dom M --> U. J ) )
60	18, 59	mpbird 232	. . . . . . . . . . . . . 14 |- ( ph -> F : U. dom M --> B )
61	6	feq3d 5709	. . . . . . . . . . . . . . 15 |- ( ph -> ( G : U. dom M --> B <-> G : U. dom M --> U. J ) )
62	20, 61	mpbird 232	. . . . . . . . . . . . . 14 |- ( ph -> G : U. dom M --> B )
63		ffn 5721	. . . . . . . . . . . . . . 15 |- ( .+ : ( B X. B ) --> C -> .+ Fn ( B X. B ) )
64	1, 63	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> .+ Fn ( B X. B ) )
65	60, 62, 23, 64	ofpreima2 27380	. . . . . . . . . . . . 13 |- ( ph -> ( `' ( F oF .+ G ) " { z } ) = U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
66	65	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ z e. ran ( F oF .+ G ) ) -> ( `' ( F oF .+ G ) " { z } ) = U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
67	52	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ z e. ran ( F oF .+ G ) ) -> dom M e. U. ran sigAlgebra )
68	52	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ z e. ran ( F oF .+ G ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> dom M e. U. ran sigAlgebra )
69		simpll 753	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ z e. ran ( F oF .+ G ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ph )
70		inss1 3703	. . . . . . . . . . . . . . . . . 18 |- ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) C_ ( `' .+ " { z } )
71		cnvimass 5347	. . . . . . . . . . . . . . . . . . . 20 |- ( `' .+ " { z } ) C_ dom .+
72		fdm 5725	. . . . . . . . . . . . . . . . . . . . 21 |- ( .+ : ( B X. B ) --> C -> dom .+ = ( B X. B ) )
73	1, 72	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> dom .+ = ( B X. B ) )
74	71, 73	syl5sseq 3537	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( `' .+ " { z } ) C_ ( B X. B ) )
75	74	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. ran ( F oF .+ G ) ) -> ( `' .+ " { z } ) C_ ( B X. B ) )
76	70, 75	syl5ss 3500	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. ran ( F oF .+ G ) ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) C_ ( B X. B ) )
77	76	sselda 3489	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ z e. ran ( F oF .+ G ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> p e. ( B X. B ) )
78	52	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. ( B X. B ) ) -> dom M e. U. ran sigAlgebra )
79		sibfof.4	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> J e. Fre )
80	79	sgsiga 28015	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> (sigaGen ` J ) e. U. ran sigAlgebra )
81	11, 80	syl5eqel 2535	. . . . . . . . . . . . . . . . . 18 |- ( ph -> S e. U. ran sigAlgebra )
82	81	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. ( B X. B ) ) -> S e. U. ran sigAlgebra )
83	3, 4, 11, 12, 13, 14, 15, 16, 17	sibfmbl 28150	. . . . . . . . . . . . . . . . . 18 |- ( ph -> F e. ( dom MMblFnM S ) )
84	83	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. ( B X. B ) ) -> F e. ( dom MMblFnM S ) )
85	4	tpstop 19313	. . . . . . . . . . . . . . . . . . . . 21 |- ( W e. TopSp -> J e. Top )
86		cldssbrsiga 28031	. . . . . . . . . . . . . . . . . . . . 21 |- ( J e. Top -> ( Clsd ` J ) C_ (sigaGen ` J ) )
87	2, 85, 86	3syl 20	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( Clsd ` J ) C_ (sigaGen ` J ) )
88	87	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( B X. B ) ) -> ( Clsd ` J ) C_ (sigaGen ` J ) )
89	79	adantr 465	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ p e. ( B X. B ) ) -> J e. Fre )
90		xp1st 6815	. . . . . . . . . . . . . . . . . . . . . 22 |- ( p e. ( B X. B ) -> ( 1st ` p ) e. B )
91	90	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ p e. ( B X. B ) ) -> ( 1st ` p ) e. B )
92	6	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ p e. ( B X. B ) ) -> B = U. J )
93	91, 92	eleqtrd 2533	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ p e. ( B X. B ) ) -> ( 1st ` p ) e. U. J )
94		eqid 2443	. . . . . . . . . . . . . . . . . . . . 21 |- U. J = U. J
95	94	t1sncld 19700	. . . . . . . . . . . . . . . . . . . 20 |- ( ( J e. Fre /\ ( 1st ` p ) e. U. J ) -> { ( 1st ` p ) } e. ( Clsd ` J ) )
96	89, 93, 95	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( B X. B ) ) -> { ( 1st ` p ) } e. ( Clsd ` J ) )
97	88, 96	sseldd 3490	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. ( B X. B ) ) -> { ( 1st ` p ) } e. (sigaGen ` J ) )
98	97, 11	syl6eleqr 2542	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. ( B X. B ) ) -> { ( 1st ` p ) } e. S )
99	78, 82, 84, 98	mbfmcnvima 28101	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. ( B X. B ) ) -> ( `' F " { ( 1st ` p ) } ) e. dom M )
100	69, 77, 99	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ z e. ran ( F oF .+ G ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( `' F " { ( 1st ` p ) } ) e. dom M )
101	3, 4, 11, 12, 13, 14, 15, 16, 19	sibfmbl 28150	. . . . . . . . . . . . . . . . . 18 |- ( ph -> G e. ( dom MMblFnM S ) )
102	101	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. ( B X. B ) ) -> G e. ( dom MMblFnM S ) )
103		xp2nd 6816	. . . . . . . . . . . . . . . . . . . . . 22 |- ( p e. ( B X. B ) -> ( 2nd ` p ) e. B )
104	103	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ p e. ( B X. B ) ) -> ( 2nd ` p ) e. B )
105	104, 92	eleqtrd 2533	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ p e. ( B X. B ) ) -> ( 2nd ` p ) e. U. J )
106	94	t1sncld 19700	. . . . . . . . . . . . . . . . . . . 20 |- ( ( J e. Fre /\ ( 2nd ` p ) e. U. J ) -> { ( 2nd ` p ) } e. ( Clsd ` J ) )
107	89, 105, 106	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. ( B X. B ) ) -> { ( 2nd ` p ) } e. ( Clsd ` J ) )
108	88, 107	sseldd 3490	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. ( B X. B ) ) -> { ( 2nd ` p ) } e. (sigaGen ` J ) )
109	108, 11	syl6eleqr 2542	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. ( B X. B ) ) -> { ( 2nd ` p ) } e. S )
110	78, 82, 102, 109	mbfmcnvima 28101	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. ( B X. B ) ) -> ( `' G " { ( 2nd ` p ) } ) e. dom M )
111	69, 77, 110	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ z e. ran ( F oF .+ G ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( `' G " { ( 2nd ` p ) } ) e. dom M )
112		inelsiga 28008	. . . . . . . . . . . . . . 15 |- ( ( 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 )
113	68, 100, 111, 112	syl3anc 1229	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ z e. ran ( F oF .+ G ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M )
114	113	ralrimiva 2857	. . . . . . . . . . . . 13 |- ( ( ph /\ z e. ran ( F oF .+ G ) ) -> A. p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M )
115	3, 4, 11, 12, 13, 14, 15, 16, 17	sibfrn 28152	. . . . . . . . . . . . . . . . 17 |- ( ph -> ran F e. Fin )
116	3, 4, 11, 12, 13, 14, 15, 16, 19	sibfrn 28152	. . . . . . . . . . . . . . . . 17 |- ( ph -> ran G e. Fin )
117		xpfi 7793	. . . . . . . . . . . . . . . . 17 |- ( ( ran F e. Fin /\ ran G e. Fin ) -> ( ran F X. ran G ) e. Fin )
118	115, 116, 117	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ran F X. ran G ) e. Fin )
119		inss2 3704	. . . . . . . . . . . . . . . 16 |- ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) C_ ( ran F X. ran G )
120		ssdomg 7563	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) )
121	118, 119, 120	mpisyl 18	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ ( ran F X. ran G ) )
122		isfinite 8072	. . . . . . . . . . . . . . . . 17 |- ( ( ran F X. ran G ) e. Fin <-> ( ran F X. ran G ) ~< om )
123	122	biimpi 194	. . . . . . . . . . . . . . . 16 |- ( ( ran F X. ran G ) e. Fin -> ( ran F X. ran G ) ~< om )
124		sdomdom 7545	. . . . . . . . . . . . . . . 16 |- ( ( ran F X. ran G ) ~< om -> ( ran F X. ran G ) ~<_ om )
125	118, 123, 124	3syl 20	. . . . . . . . . . . . . . 15 |- ( ph -> ( ran F X. ran G ) ~<_ om )
126		domtr 7570	. . . . . . . . . . . . . . 15 |- ( ( ( ( `' .+ " { 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 )
127	121, 125, 126	syl2anc 661	. . . . . . . . . . . . . 14 |- ( ph -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ om )
128	127	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ z e. ran ( F oF .+ G ) ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ om )
129		nfcv 2605	. . . . . . . . . . . . . 14 |- F/_ p ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) )
130	129	sigaclcuni 27991	. . . . . . . . . . . . 13 |- ( ( 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 )
131	67, 114, 128, 130	syl3anc 1229	. . . . . . . . . . . 12 |- ( ( ph /\ z e. ran ( F oF .+ G ) ) -> U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M )
132	66, 131	eqeltrd 2531	. . . . . . . . . . 11 |- ( ( ph /\ z e. ran ( F oF .+ G ) ) -> ( `' ( F oF .+ G ) " { z } ) e. dom M )
133	132	ralrimiva 2857	. . . . . . . . . 10 |- ( ph -> A. z e. ran ( F oF .+ G ) ( `' ( F oF .+ G ) " { z } ) e. dom M )
134		ssralv 3549	. . . . . . . . . 10 |- ( ( b i^i ran ( F oF .+ G ) ) C_ ran ( F oF .+ G ) -> ( A. z e. ran ( F oF .+ G ) ( `' ( F oF .+ G ) " { z } ) e. dom M -> A. z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) e. dom M ) )
135	58, 133, 134	mpsyl 63	. . . . . . . . 9 |- ( ph -> A. z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) e. dom M )
136	135	adantr 465	. . . . . . . 8 |- ( ( ph /\ b e. (sigaGen ` ( TopOpen ` K ) ) ) -> A. z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) e. dom M )
137		ffun 5723	. . . . . . . . . . . . . 14 |- ( .+ : ( B X. B ) --> C -> Fun .+ )
138	1, 137	syl 16	. . . . . . . . . . . . 13 |- ( ph -> Fun .+ )
139		imafi 7815	. . . . . . . . . . . . 13 |- ( ( Fun .+ /\ ( ran F X. ran G ) e. Fin ) -> ( .+ " ( ran F X. ran G ) ) e. Fin )
140	138, 118, 139	syl2anc 661	. . . . . . . . . . . 12 |- ( ph -> ( .+ " ( ran F X. ran G ) ) e. Fin )
141	18, 20, 9, 23	ofrn2 27352	. . . . . . . . . . . 12 |- ( ph -> ran ( F oF .+ G ) C_ ( .+ " ( ran F X. ran G ) ) )
142		ssfi 7742	. . . . . . . . . . . 12 |- ( ( ( .+ " ( ran F X. ran G ) ) e. Fin /\ ran ( F oF .+ G ) C_ ( .+ " ( ran F X. ran G ) ) ) -> ran ( F oF .+ G ) e. Fin )
143	140, 141, 142	syl2anc 661	. . . . . . . . . . 11 |- ( ph -> ran ( F oF .+ G ) e. Fin )
144		ssdomg 7563	. . . . . . . . . . 11 |- ( ran ( F oF .+ G ) e. Fin -> ( ( b i^i ran ( F oF .+ G ) ) C_ ran ( F oF .+ G ) -> ( b i^i ran ( F oF .+ G ) ) ~<_ ran ( F oF .+ G ) ) )
145	143, 58, 144	mpisyl 18	. . . . . . . . . 10 |- ( ph -> ( b i^i ran ( F oF .+ G ) ) ~<_ ran ( F oF .+ G ) )
146		isfinite 8072	. . . . . . . . . . . 12 |- ( ran ( F oF .+ G ) e. Fin <-> ran ( F oF .+ G ) ~< om )
147	143, 146	sylib 196	. . . . . . . . . . 11 |- ( ph -> ran ( F oF .+ G ) ~< om )
148		sdomdom 7545	. . . . . . . . . . 11 |- ( ran ( F oF .+ G ) ~< om -> ran ( F oF .+ G ) ~<_ om )
149	147, 148	syl 16	. . . . . . . . . 10 |- ( ph -> ran ( F oF .+ G ) ~<_ om )
150		domtr 7570	. . . . . . . . . 10 |- ( ( ( b i^i ran ( F oF .+ G ) ) ~<_ ran ( F oF .+ G ) /\ ran ( F oF .+ G ) ~<_ om ) -> ( b i^i ran ( F oF .+ G ) ) ~<_ om )
151	145, 149, 150	syl2anc 661	. . . . . . . . 9 |- ( ph -> ( b i^i ran ( F oF .+ G ) ) ~<_ om )
152	151	adantr 465	. . . . . . . 8 |- ( ( ph /\ b e. (sigaGen ` ( TopOpen ` K ) ) ) -> ( b i^i ran ( F oF .+ G ) ) ~<_ om )
153		nfcv 2605	. . . . . . . . 9 |- F/_ z ( b i^i ran ( F oF .+ G ) )
154	153	sigaclcuni 27991	. . . . . . . 8 |- ( ( dom M e. U. ran sigAlgebra /\ A. z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) e. dom M /\ ( b i^i ran ( F oF .+ G ) ) ~<_ om ) -> U_ z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) e. dom M )
155	53, 136, 152, 154	syl3anc 1229	. . . . . . 7 |- ( ( ph /\ b e. (sigaGen ` ( TopOpen ` K ) ) ) -> U_ z e. ( b i^i ran ( F oF .+ G ) ) ( `' ( F oF .+ G ) " { z } ) e. dom M )
156	57, 155	syl5eqelr 2536	. . . . . 6 |- ( ( ph /\ b e. (sigaGen ` ( TopOpen ` K ) ) ) -> ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) e. dom M )
157		difpreima 6000	. . . . . . . . . 10 |- ( Fun ( F oF .+ G ) -> ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) = ( ( `' ( F oF .+ G ) " b ) \ ( `' ( F oF .+ G ) " ran ( F oF .+ G ) ) ) )
158	25, 46, 157	3syl 20	. . . . . . . . 9 |- ( ph -> ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) = ( ( `' ( F oF .+ G ) " b ) \ ( `' ( F oF .+ G ) " ran ( F oF .+ G ) ) ) )
159		cnvimarndm 5348	. . . . . . . . . . 11 |- ( `' ( F oF .+ G ) " ran ( F oF .+ G ) ) = dom ( F oF .+ G )
160	159	difeq2i 3604	. . . . . . . . . 10 |- ( ( `' ( F oF .+ G ) " b ) \ ( `' ( F oF .+ G ) " ran ( F oF .+ G ) ) ) = ( ( `' ( F oF .+ G ) " b ) \ dom ( F oF .+ G ) )
161		cnvimass 5347	. . . . . . . . . . 11 |- ( `' ( F oF .+ G ) " b ) C_ dom ( F oF .+ G )
162		ssdif0 3871	. . . . . . . . . . 11 |- ( ( `' ( F oF .+ G ) " b ) C_ dom ( F oF .+ G ) <-> ( ( `' ( F oF .+ G ) " b ) \ dom ( F oF .+ G ) ) = (/) )
163	161, 162	mpbi 208	. . . . . . . . . 10 |- ( ( `' ( F oF .+ G ) " b ) \ dom ( F oF .+ G ) ) = (/)
164	160, 163	eqtri 2472	. . . . . . . . 9 |- ( ( `' ( F oF .+ G ) " b ) \ ( `' ( F oF .+ G ) " ran ( F oF .+ G ) ) ) = (/)
165	158, 164	syl6eq 2500	. . . . . . . 8 |- ( ph -> ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) = (/) )
166		0elsiga 27987	. . . . . . . . 9 |- ( dom M e. U. ran sigAlgebra -> (/) e. dom M )
167	16, 51, 166	3syl 20	. . . . . . . 8 |- ( ph -> (/) e. dom M )
168	165, 167	eqeltrd 2531	. . . . . . 7 |- ( ph -> ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) e. dom M )
169	168	adantr 465	. . . . . 6 |- ( ( ph /\ b e. (sigaGen ` ( TopOpen ` K ) ) ) -> ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) e. dom M )
170		unelsiga 28007	. . . . . 6 |- ( ( dom M e. U. ran sigAlgebra /\ ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) e. dom M /\ ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) e. dom M ) -> ( ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) u. ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) ) e. dom M )
171	53, 156, 169, 170	syl3anc 1229	. . . . 5 |- ( ( ph /\ b e. (sigaGen ` ( TopOpen ` K ) ) ) -> ( ( `' ( F oF .+ G ) " ( b i^i ran ( F oF .+ G ) ) ) u. ( `' ( F oF .+ G ) " ( b \ ran ( F oF .+ G ) ) ) ) e. dom M )
172	50, 171	eqeltrd 2531	. . . 4 |- ( ( ph /\ b e. (sigaGen ` ( TopOpen ` K ) ) ) -> ( `' ( F oF .+ G ) " b ) e. dom M )
173	172	ralrimiva 2857	. . 3 |- ( ph -> A. b e. (sigaGen ` ( TopOpen ` K ) ) ( `' ( F oF .+ G ) " b ) e. dom M )
174	52, 38	ismbfm 28096	. . 3 |- ( ph -> ( ( F oF .+ G ) e. ( dom MMblFnM (sigaGen ` ( TopOpen ` K ) ) ) <-> ( ( F oF .+ G ) e. ( U. (sigaGen ` ( TopOpen ` K ) ) ^m U. dom M ) /\ A. b e. (sigaGen ` ( TopOpen ` K ) ) ( `' ( F oF .+ G ) " b ) e. dom M ) ) )
175	43, 173, 174	mpbir2and 922	. 2 |- ( ph -> ( F oF .+ G ) e. ( dom MMblFnM (sigaGen ` ( TopOpen ` K ) ) ) )
176	65	adantr 465	. . . . . . 7 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( `' ( F oF .+ G ) " { z } ) = U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
177	176	fveq2d 5860	. . . . . 6 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( M ` ( `' ( F oF .+ G ) " { z } ) ) = ( M ` U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
178		measbasedom 28046	. . . . . . . . 9 |- ( M e. U. ran measures <-> M e. (measures ` dom M ) )
179	16, 178	sylib 196	. . . . . . . 8 |- ( ph -> M e. (measures ` dom M ) )
180	179	adantr 465	. . . . . . 7 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> M e. (measures ` dom M ) )
181		eldifi 3611	. . . . . . . 8 |- ( z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) -> z e. ran ( F oF .+ G ) )
182	181, 114	sylan2 474	. . . . . . 7 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> A. p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M )
183	127	adantr 465	. . . . . . 7 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ~<_ om )
184		sneq 4024	. . . . . . . . . . 11 |- ( x = ( 1st ` p ) -> { x } = { ( 1st ` p ) } )
185	184	imaeq2d 5327	. . . . . . . . . 10 |- ( x = ( 1st ` p ) -> ( `' F " { x } ) = ( `' F " { ( 1st ` p ) } ) )
186		sneq 4024	. . . . . . . . . . 11 |- ( y = ( 2nd ` p ) -> { y } = { ( 2nd ` p ) } )
187	186	imaeq2d 5327	. . . . . . . . . 10 |- ( y = ( 2nd ` p ) -> ( `' G " { y } ) = ( `' G " { ( 2nd ` p ) } ) )
188		ffun 5723	. . . . . . . . . . . 12 |- ( F : U. dom M --> U. J -> Fun F )
189	18, 188	syl 16	. . . . . . . . . . 11 |- ( ph -> Fun F )
190		sndisj 4429	. . . . . . . . . . 11 |- Disj x e. ran F { x }
191		disjpreima 27317	. . . . . . . . . . 11 |- ( ( Fun F /\ Disj x e. ran F { x } ) -> Disj x e. ran F ( `' F " { x } ) )
192	189, 190, 191	sylancl 662	. . . . . . . . . 10 |- ( ph -> Disj x e. ran F ( `' F " { x } ) )
193		ffun 5723	. . . . . . . . . . . 12 |- ( G : U. dom M --> U. J -> Fun G )
194	20, 193	syl 16	. . . . . . . . . . 11 |- ( ph -> Fun G )
195		sndisj 4429	. . . . . . . . . . 11 |- Disj y e. ran G { y }
196		disjpreima 27317	. . . . . . . . . . 11 |- ( ( Fun G /\ Disj y e. ran G { y } ) -> Disj y e. ran G ( `' G " { y } ) )
197	194, 195, 196	sylancl 662	. . . . . . . . . 10 |- ( ph -> Disj y e. ran G ( `' G " { y } ) )
198	185, 187, 192, 197	disjxpin 27319	. . . . . . . . 9 |- ( ph -> Disj p e. ( ran F X. ran G ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
199		disjss1 4413	. . . . . . . . 9 |- ( ( ( `' .+ " { 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 ) } ) ) ) )
200	119, 198, 199	mpsyl 63	. . . . . . . 8 |- ( ph -> Disj p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
201	200	adantr 465	. . . . . . 7 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> Disj p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) )
202		measvuni 28058	. . . . . . 7 |- ( ( 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 ) } ) ) ) )
203	180, 182, 183, 201, 202	syl112anc 1233	. . . . . 6 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( M ` U_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) = Σ* p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
204		ssfi 7742	. . . . . . . . 9 |- ( ( ( 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 )
205	118, 119, 204	sylancl 662	. . . . . . . 8 |- ( ph -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) e. Fin )
206	205	adantr 465	. . . . . . 7 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) e. Fin )
207		simpll 753	. . . . . . . 8 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ph )
208		simpr 461	. . . . . . . . . 10 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) )
209	119, 208	sseldi 3487	. . . . . . . . 9 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> p e. ( ran F X. ran G ) )
210		xp1st 6815	. . . . . . . . 9 |- ( p e. ( ran F X. ran G ) -> ( 1st ` p ) e. ran F )
211	209, 210	syl 16	. . . . . . . 8 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( 1st ` p ) e. ran F )
212		xp2nd 6816	. . . . . . . . 9 |- ( p e. ( ran F X. ran G ) -> ( 2nd ` p ) e. ran G )
213	209, 212	syl 16	. . . . . . . 8 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( 2nd ` p ) e. ran G )
214		oveq12 6290	. . . . . . . . . . . . . . . 16 |- ( ( x = .0. /\ y = .0. ) -> ( x .+ y ) = ( .0. .+ .0. ) )
215		sibfof.5	. . . . . . . . . . . . . . . 16 |- ( ph -> ( .0. .+ .0. ) = ( 0g ` K ) )
216	214, 215	sylan9eqr 2506	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x = .0. /\ y = .0. ) ) -> ( x .+ y ) = ( 0g ` K ) )
217	216	ex 434	. . . . . . . . . . . . . 14 |- ( ph -> ( ( x = .0. /\ y = .0. ) -> ( x .+ y ) = ( 0g ` K ) ) )
218	217	necon3ad 2653	. . . . . . . . . . . . 13 |- ( ph -> ( ( x .+ y ) =/= ( 0g ` K ) -> -. ( x = .0. /\ y = .0. ) ) )
219		neorian 2770	. . . . . . . . . . . . 13 |- ( ( x =/= .0. \/ y =/= .0. ) <-> -. ( x = .0. /\ y = .0. ) )
220	218, 219	syl6ibr 227	. . . . . . . . . . . 12 |- ( ph -> ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) )
221	220	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) )
222	221	ralrimivva 2864	. . . . . . . . . 10 |- ( ph -> A. x e. B A. y e. B ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) )
223	207, 222	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> A. x e. B A. y e. B ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) )
224	70	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) C_ ( `' .+ " { z } ) )
225	224	sselda 3489	. . . . . . . . . . . 12 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> p e. ( `' .+ " { z } ) )
226		fniniseg 5993	. . . . . . . . . . . . 13 |- ( .+ Fn ( B X. B ) -> ( p e. ( `' .+ " { z } ) <-> ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) ) )
227	207, 64, 226	3syl 20	. . . . . . . . . . . 12 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( p e. ( `' .+ " { z } ) <-> ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) ) )
228	225, 227	mpbid 210	. . . . . . . . . . 11 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) )
229		simpr 461	. . . . . . . . . . . 12 |- ( ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) -> ( .+ ` p ) = z )
230		1st2nd2 6822	. . . . . . . . . . . . . . 15 |- ( p e. ( B X. B ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
231	230	fveq2d 5860	. . . . . . . . . . . . . 14 |- ( p e. ( B X. B ) -> ( .+ ` p ) = ( .+ ` <. ( 1st ` p ) , ( 2nd ` p ) >. ) )
232		df-ov 6284	. . . . . . . . . . . . . 14 |- ( ( 1st ` p ) .+ ( 2nd ` p ) ) = ( .+ ` <. ( 1st ` p ) , ( 2nd ` p ) >. )
233	231, 232	syl6eqr 2502	. . . . . . . . . . . . 13 |- ( p e. ( B X. B ) -> ( .+ ` p ) = ( ( 1st ` p ) .+ ( 2nd ` p ) ) )
234	233	adantr 465	. . . . . . . . . . . 12 |- ( ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) -> ( .+ ` p ) = ( ( 1st ` p ) .+ ( 2nd ` p ) ) )
235	229, 234	eqtr3d 2486	. . . . . . . . . . 11 |- ( ( p e. ( B X. B ) /\ ( .+ ` p ) = z ) -> z = ( ( 1st ` p ) .+ ( 2nd ` p ) ) )
236	228, 235	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> z = ( ( 1st ` p ) .+ ( 2nd ` p ) ) )
237		simplr 755	. . . . . . . . . . . 12 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) )
238	237	eldifbd 3474	. . . . . . . . . . 11 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> -. z e. { ( 0g ` K ) } )
239		elsn 4028	. . . . . . . . . . . 12 |- ( z e. { ( 0g ` K ) } <-> z = ( 0g ` K ) )
240	239	necon3bbii 2704	. . . . . . . . . . 11 |- ( -. z e. { ( 0g ` K ) } <-> z =/= ( 0g ` K ) )
241	238, 240	sylib 196	. . . . . . . . . 10 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> z =/= ( 0g ` K ) )
242	236, 241	eqnetrrd 2737	. . . . . . . . 9 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( ( 1st ` p ) .+ ( 2nd ` p ) ) =/= ( 0g ` K ) )
243	181, 77	sylanl2 651	. . . . . . . . . . 11 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> p e. ( B X. B ) )
244	243, 90	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( 1st ` p ) e. B )
245	243, 103	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( 2nd ` p ) e. B )
246		oveq1 6288	. . . . . . . . . . . . 13 |- ( x = ( 1st ` p ) -> ( x .+ y ) = ( ( 1st ` p ) .+ y ) )
247	246	neeq1d 2720	. . . . . . . . . . . 12 |- ( x = ( 1st ` p ) -> ( ( x .+ y ) =/= ( 0g ` K ) <-> ( ( 1st ` p ) .+ y ) =/= ( 0g ` K ) ) )
248		neeq1 2724	. . . . . . . . . . . . 13 |- ( x = ( 1st ` p ) -> ( x =/= .0. <-> ( 1st ` p ) =/= .0. ) )
249	248	orbi1d 702	. . . . . . . . . . . 12 |- ( x = ( 1st ` p ) -> ( ( x =/= .0. \/ y =/= .0. ) <-> ( ( 1st ` p ) =/= .0. \/ y =/= .0. ) ) )
250	247, 249	imbi12d 320	. . . . . . . . . . 11 |- ( x = ( 1st ` p ) -> ( ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) <-> ( ( ( 1st ` p ) .+ y ) =/= ( 0g ` K ) -> ( ( 1st ` p ) =/= .0. \/ y =/= .0. ) ) ) )
251		oveq2 6289	. . . . . . . . . . . . 13 |- ( y = ( 2nd ` p ) -> ( ( 1st ` p ) .+ y ) = ( ( 1st ` p ) .+ ( 2nd ` p ) ) )
252	251	neeq1d 2720	. . . . . . . . . . . 12 |- ( y = ( 2nd ` p ) -> ( ( ( 1st ` p ) .+ y ) =/= ( 0g ` K ) <-> ( ( 1st ` p ) .+ ( 2nd ` p ) ) =/= ( 0g ` K ) ) )
253		neeq1 2724	. . . . . . . . . . . . 13 |- ( y = ( 2nd ` p ) -> ( y =/= .0. <-> ( 2nd ` p ) =/= .0. ) )
254	253	orbi2d 701	. . . . . . . . . . . 12 |- ( y = ( 2nd ` p ) -> ( ( ( 1st ` p ) =/= .0. \/ y =/= .0. ) <-> ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) ) )
255	252, 254	imbi12d 320	. . . . . . . . . . 11 |- ( 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. ) ) ) )
256	250, 255	rspc2v 3205	. . . . . . . . . 10 |- ( ( ( 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. ) ) ) )
257	244, 245, 256	syl2anc 661	. . . . . . . . 9 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( A. x e. B A. y e. B ( ( x .+ y ) =/= ( 0g ` K ) -> ( x =/= .0. \/ y =/= .0. ) ) -> ( ( ( 1st ` p ) .+ ( 2nd ` p ) ) =/= ( 0g ` K ) -> ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) ) ) )
258	223, 242, 257	mp2d 45	. . . . . . . 8 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) )
259	3, 4, 11, 12, 13, 14, 15, 16, 17, 19, 2, 79	sibfinima 28154	. . . . . . . 8 |- ( ( ( ph /\ ( 1st ` p ) e. ran F /\ ( 2nd ` p ) e. ran G ) /\ ( ( 1st ` p ) =/= .0. \/ ( 2nd ` p ) =/= .0. ) ) -> ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) e. ( 0 [,) +oo ) )
260	207, 211, 213, 258, 259	syl31anc 1232	. . . . . . 7 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) e. ( 0 [,) +oo ) )
261	206, 260	esumpfinval 27954	. . . . . 6 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> Σ* p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) = sum_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
262	177, 203, 261	3eqtrd 2488	. . . . 5 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( M ` ( `' ( F oF .+ G ) " { z } ) ) = sum_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
263		rge0ssre 11637	. . . . . . 7 |- ( 0 [,) +oo ) C_ RR
264	263, 260	sseldi 3487	. . . . . 6 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) e. RR )
265	206, 264	fsumrecl 13535	. . . . 5 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> sum_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) e. RR )
266	262, 265	eqeltrd 2531	. . . 4 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( M ` ( `' ( F oF .+ G ) " { z } ) ) e. RR )
267	180	adantr 465	. . . . . . 7 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> M e. (measures ` dom M ) )
268	181, 113	sylanl2 651	. . . . . . 7 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) e. dom M )
269		measge0 28051	. . . . . . 7 |- ( ( 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 ) } ) ) ) )
270	267, 268, 269	syl2anc 661	. . . . . 6 |- ( ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) /\ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ) -> 0 <_ ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
271	206, 264, 270	fsumge0 13588	. . . . 5 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> 0 <_ sum_ p e. ( ( `' .+ " { z } ) i^i ( ran F X. ran G ) ) ( M ` ( ( `' F " { ( 1st ` p ) } ) i^i ( `' G " { ( 2nd ` p ) } ) ) ) )
272	271, 262	breqtrrd 4463	. . . 4 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> 0 <_ ( M ` ( `' ( F oF .+ G ) " { z } ) ) )
273		elrege0 11636	. . . 4 |- ( ( M ` ( `' ( F oF .+ G ) " { z } ) ) e. ( 0 [,) +oo ) <-> ( ( M ` ( `' ( F oF .+ G ) " { z } ) ) e. RR /\ 0 <_ ( M ` ( `' ( F oF .+ G ) " { z } ) ) ) )
274	266, 272, 273	sylanbrc 664	. . 3 |- ( ( ph /\ z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ) -> ( M ` ( `' ( F oF .+ G ) " { z } ) ) e. ( 0 [,) +oo ) )
275	274	ralrimiva 2857	. 2 |- ( ph -> A. z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ( M ` ( `' ( F oF .+ G ) " { z } ) ) e. ( 0 [,) +oo ) )
276		eqid 2443	. . 3 |- (sigaGen ` ( TopOpen ` K ) ) = (sigaGen ` ( TopOpen ` K ) )
277		eqid 2443	. . 3 |- ( 0g ` K ) = ( 0g ` K )
278		eqid 2443	. . 3 |- ( .s ` K ) = ( .s ` K )
279		eqid 2443	. . 3 |- (RRHom ` (Scalar ` K ) ) = (RRHom ` (Scalar ` K ) )
280	27, 28, 276, 277, 278, 279, 26, 16	issibf 28148	. 2 |- ( ph -> ( ( F oF .+ G ) e. dom ( Ksitg M ) <-> ( ( F oF .+ G ) e. ( dom MMblFnM (sigaGen ` ( TopOpen ` K ) ) ) /\ ran ( F oF .+ G ) e. Fin /\ A. z e. ( ran ( F oF .+ G ) \ { ( 0g ` K ) } ) ( M ` ( `' ( F oF .+ G ) " { z } ) ) e. ( 0 [,) +oo ) ) ) )
281	175, 143, 275, 280	mpbir3and 1180	1 |- ( ph -> ( F oF .+ G ) e. dom ( Ksitg M ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   = wceq 1383   e. wcel 1804   =/= wne 2638   A.wral 2793   _Vcvv 3095   \ cdif 3458   u. cun 3459   i^i cin 3460   C_ wss 3461   (/)c0 3770   {csn 4014   <.cop 4020   U.cuni 4234   U_ciun 4315  Disj wdisj 4407   class class class wbr 4437   X. cxp 4987   `'ccnv 4988   dom cdm 4989   ran crn 4990   "cima 4992   Fun wfun 5572   Fn wfn 5573   -->wf 5574   ` cfv 5578  (class class class)co 6281   oFcof 6523   omcom 6685   1stc1st 6783   2ndc2nd 6784   ^m cmap 7422   ~<_ cdom 7516   ~< csdm 7517   Fincfn 7518   RRcr 9494   0cc0 9495   +oocpnf 9628   <_ cle 9632   [,)cico 11540   sum_csu 13487   Basecbs 14509  Scalarcsca 14577   .scvsca 14578   TopOpenctopn 14696   0gc0g 14714   Topctop 19267   TopSpctps 19270   Clsdccld 19390   Frect1 19681  RRHomcrrh 27847  Σ^*cesum 27913  sigAlgebracsiga 27980  sigaGencsigagen 28011  measurescmeas 28039  MblFnMcmbfm 28094  sitgcsitg 28144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-inf2 8061  ax-ac2 8846  ax-cnex 9551  ax-resscn 9552  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-addrcl 9556  ax-mulcl 9557  ax-mulrcl 9558  ax-mulcom 9559  ax-addass 9560  ax-mulass 9561  ax-distr 9562  ax-i2m1 9563  ax-1ne0 9564  ax-1rid 9565  ax-rnegex 9566  ax-rrecex 9567  ax-cnre 9568  ax-pre-lttri 9569  ax-pre-lttrn 9570  ax-pre-ltadd 9571  ax-pre-mulgt0 9572  ax-pre-sup 9573  ax-addf 9574  ax-mulf 9575

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-fal 1389  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-reu 2800  df-rmo 2801  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-iin 4318  df-disj 4408  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-se 4829  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-isom 5587  df-riota 6242  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-of 6525  df-om 6686  df-1st 6785  df-2nd 6786  df-supp 6904  df-recs 7044  df-rdg 7078  df-1o 7132  df-2o 7133  df-oadd 7136  df-er 7313  df-map 7424  df-pm 7425  df-ixp 7472  df-en 7519  df-dom 7520  df-sdom 7521  df-fin 7522  df-fsupp 7832  df-fi 7873  df-sup 7903  df-oi 7938  df-card 8323  df-acn 8326  df-ac 8500  df-cda 8551  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637  df-sub 9812  df-neg 9813  df-div 10213  df-nn 10543  df-2 10600  df-3 10601  df-4 10602  df-5 10603  df-6 10604  df-7 10605  df-8 10606  df-9 10607  df-10 10608  df-n0 10802  df-z 10871  df-dec 10985  df-uz 11091  df-q 11192  df-rp 11230  df-xneg 11327  df-xadd 11328  df-xmul 11329  df-ioo 11542  df-ioc 11543  df-ico 11544  df-icc 11545  df-fz 11682  df-fzo 11804  df-fl 11908  df-mod 11976  df-seq 12087  df-exp 12146  df-fac 12333  df-bc 12360  df-hash 12385  df-shft 12879  df-cj 12911  df-re 12912  df-im 12913  df-sqrt 13047  df-abs 13048  df-limsup 13273  df-clim 13290  df-rlim 13291  df-sum 13488  df-ef 13681  df-sin 13683  df-cos 13684  df-pi 13686  df-struct 14511  df-ndx 14512  df-slot 14513  df-base 14514  df-sets 14515  df-ress 14516  df-plusg 14587  df-mulr 14588  df-starv 14589  df-sca 14590  df-vsca 14591  df-ip 14592  df-tset 14593  df-ple 14594  df-ds 14596  df-unif 14597  df-hom 14598  df-cco 14599  df-rest 14697  df-topn 14698  df-0g 14716  df-gsum 14717  df-topgen 14718  df-pt 14719  df-prds 14722  df-ordt 14775  df-xrs 14776  df-qtop 14781  df-imas 14782  df-xps 14784  df-mre 14860  df-mrc 14861  df-acs 14863  df-ps 15704  df-tsr 15705  df-plusf 15745  df-mgm 15746  df-sgrp 15785  df-mnd 15795  df-mhm 15840  df-submnd 15841  df-grp 15931  df-minusg 15932  df-sbg 15933  df-mulg 15934  df-subg 16072  df-cntz 16229  df-cmn 16674  df-abl 16675  df-mgp 17016  df-ur 17028  df-ring 17074  df-cring 17075  df-subrg 17301  df-abv 17340  df-lmod 17388  df-scaf 17389  df-sra 17692  df-rgmod 17693  df-psmet 18285  df-xmet 18286  df-met 18287  df-bl 18288  df-mopn 18289  df-fbas 18290  df-fg 18291  df-cnfld 18295  df-top 19272  df-bases 19274  df-topon 19275  df-topsp 19276  df-cld 19393  df-ntr 19394  df-cls 19395  df-nei 19472  df-lp 19510  df-perf 19511  df-cn 19601  df-cnp 19602  df-t1 19688  df-haus 19689  df-tx 19936  df-hmeo 20129  df-fil 20220  df-fm 20312  df-flim 20313  df-flf 20314  df-tmd 20444  df-tgp 20445  df-tsms 20498  df-trg 20535  df-xms 20696  df-ms 20697  df-tms 20698  df-nm 20976  df-ngp 20977  df-nrg 20979  df-nlm 20980  df-ii 21254  df-cncf 21255  df-limc 22143  df-dv 22144  df-log 22816  df-esum 27914  df-siga 27981  df-sigagen 28012  df-meas 28040  df-mbfm 28095  df-sitg 28145

This theorem is referenced by: (None)