eltsms

Description: The property of being a sum of the sequence F in the topological commutative monoid G . (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	eltsms.b	\|- B = ( Base ` G )
	eltsms.j	\|- J = ( TopOpen ` G )
	eltsms.s	\|- S = ( ~P A i^i Fin )
	eltsms.1	\|- ( ph -> G e. CMnd )
	eltsms.2	\|- ( ph -> G e. TopSp )
	eltsms.a	\|- ( ph -> A e. V )
	eltsms.f	\|- ( ph -> F : A --> B )
Assertion	eltsms	\|- ( ph -> ( C e. ( G tsums F ) <-> ( C e. B /\ A. u e. J ( C e. u -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F \|` y ) ) e. u ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eltsms.b	\|- B = ( Base ` G )
2		eltsms.j	\|- J = ( TopOpen ` G )
3		eltsms.s	\|- S = ( ~P A i^i Fin )
4		eltsms.1	\|- ( ph -> G e. CMnd )
5		eltsms.2	\|- ( ph -> G e. TopSp )
6		eltsms.a	\|- ( ph -> A e. V )
7		eltsms.f	\|- ( ph -> F : A --> B )
8		eqid	\|- ran ( z e. S \|-> { y e. S \| z C_ y } ) = ran ( z e. S \|-> { y e. S \| z C_ y } )
9	1 2 3 8 4 6 7	tsmsval	\|- ( ph -> ( G tsums F ) = ( ( J fLimf ( S filGen ran ( z e. S \|-> { y e. S \| z C_ y } ) ) ) ` ( y e. S \|-> ( G gsum ( F \|` y ) ) ) ) )
10	9	eleq2d	\|- ( ph -> ( C e. ( G tsums F ) <-> C e. ( ( J fLimf ( S filGen ran ( z e. S \|-> { y e. S \| z C_ y } ) ) ) ` ( y e. S \|-> ( G gsum ( F \|` y ) ) ) ) ) )
11	1 2	istps	\|- ( G e. TopSp <-> J e. ( TopOn ` B ) )
12	5 11	sylib	\|- ( ph -> J e. ( TopOn ` B ) )
13		eqid	\|- ( z e. S \|-> { y e. S \| z C_ y } ) = ( z e. S \|-> { y e. S \| z C_ y } )
14	3 13 8 6	tsmsfbas	\|- ( ph -> ran ( z e. S \|-> { y e. S \| z C_ y } ) e. ( fBas ` S ) )
15	1 3 4 6 7	tsmslem1	\|- ( ( ph /\ y e. S ) -> ( G gsum ( F \|` y ) ) e. B )
16	15	fmpttd	\|- ( ph -> ( y e. S \|-> ( G gsum ( F \|` y ) ) ) : S --> B )
17		eqid	\|- ( S filGen ran ( z e. S \|-> { y e. S \| z C_ y } ) ) = ( S filGen ran ( z e. S \|-> { y e. S \| z C_ y } ) )
18	17	flffbas	\|- ( ( J e. ( TopOn ` B ) /\ ran ( z e. S \|-> { y e. S \| z C_ y } ) e. ( fBas ` S ) /\ ( y e. S \|-> ( G gsum ( F \|` y ) ) ) : S --> B ) -> ( C e. ( ( J fLimf ( S filGen ran ( z e. S \|-> { y e. S \| z C_ y } ) ) ) ` ( y e. S \|-> ( G gsum ( F \|` y ) ) ) ) <-> ( C e. B /\ A. u e. J ( C e. u -> E. w e. ran ( z e. S \|-> { y e. S \| z C_ y } ) ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " w ) C_ u ) ) ) )
19	12 14 16 18	syl3anc	\|- ( ph -> ( C e. ( ( J fLimf ( S filGen ran ( z e. S \|-> { y e. S \| z C_ y } ) ) ) ` ( y e. S \|-> ( G gsum ( F \|` y ) ) ) ) <-> ( C e. B /\ A. u e. J ( C e. u -> E. w e. ran ( z e. S \|-> { y e. S \| z C_ y } ) ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " w ) C_ u ) ) ) )
20		pwexg	\|- ( A e. V -> ~P A e. _V )
21		inex1g	\|- ( ~P A e. _V -> ( ~P A i^i Fin ) e. _V )
22	6 20 21	3syl	\|- ( ph -> ( ~P A i^i Fin ) e. _V )
23	3 22	eqeltrid	\|- ( ph -> S e. _V )
24	23	adantr	\|- ( ( ph /\ u e. J ) -> S e. _V )
25		rabexg	\|- ( S e. _V -> { y e. S \| z C_ y } e. _V )
26	24 25	syl	\|- ( ( ph /\ u e. J ) -> { y e. S \| z C_ y } e. _V )
27	26	ralrimivw	\|- ( ( ph /\ u e. J ) -> A. z e. S { y e. S \| z C_ y } e. _V )
28		imaeq2	\|- ( w = { y e. S \| z C_ y } -> ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " w ) = ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " { y e. S \| z C_ y } ) )
29	28	sseq1d	\|- ( w = { y e. S \| z C_ y } -> ( ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " w ) C_ u <-> ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " { y e. S \| z C_ y } ) C_ u ) )
30	13 29	rexrnmptw	\|- ( A. z e. S { y e. S \| z C_ y } e. _V -> ( E. w e. ran ( z e. S \|-> { y e. S \| z C_ y } ) ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " w ) C_ u <-> E. z e. S ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " { y e. S \| z C_ y } ) C_ u ) )
31	27 30	syl	\|- ( ( ph /\ u e. J ) -> ( E. w e. ran ( z e. S \|-> { y e. S \| z C_ y } ) ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " w ) C_ u <-> E. z e. S ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " { y e. S \| z C_ y } ) C_ u ) )
32		funmpt	\|- Fun ( y e. S \|-> ( G gsum ( F \|` y ) ) )
33		ssrab2	\|- { y e. S \| z C_ y } C_ S
34		ovex	\|- ( G gsum ( F \|` y ) ) e. _V
35		eqid	\|- ( y e. S \|-> ( G gsum ( F \|` y ) ) ) = ( y e. S \|-> ( G gsum ( F \|` y ) ) )
36	34 35	dmmpti	\|- dom ( y e. S \|-> ( G gsum ( F \|` y ) ) ) = S
37	33 36	sseqtrri	\|- { y e. S \| z C_ y } C_ dom ( y e. S \|-> ( G gsum ( F \|` y ) ) )
38		funimass3	\|- ( ( Fun ( y e. S \|-> ( G gsum ( F \|` y ) ) ) /\ { y e. S \| z C_ y } C_ dom ( y e. S \|-> ( G gsum ( F \|` y ) ) ) ) -> ( ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " { y e. S \| z C_ y } ) C_ u <-> { y e. S \| z C_ y } C_ ( `' ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " u ) ) )
39	32 37 38	mp2an	\|- ( ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " { y e. S \| z C_ y } ) C_ u <-> { y e. S \| z C_ y } C_ ( `' ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " u ) )
40	35	mptpreima	\|- ( `' ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " u ) = { y e. S \| ( G gsum ( F \|` y ) ) e. u }
41	40	sseq2i	\|- ( { y e. S \| z C_ y } C_ ( `' ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " u ) <-> { y e. S \| z C_ y } C_ { y e. S \| ( G gsum ( F \|` y ) ) e. u } )
42		ss2rab	\|- ( { y e. S \| z C_ y } C_ { y e. S \| ( G gsum ( F \|` y ) ) e. u } <-> A. y e. S ( z C_ y -> ( G gsum ( F \|` y ) ) e. u ) )
43	39 41 42	3bitri	\|- ( ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " { y e. S \| z C_ y } ) C_ u <-> A. y e. S ( z C_ y -> ( G gsum ( F \|` y ) ) e. u ) )
44	43	rexbii	\|- ( E. z e. S ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " { y e. S \| z C_ y } ) C_ u <-> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F \|` y ) ) e. u ) )
45	31 44	bitrdi	\|- ( ( ph /\ u e. J ) -> ( E. w e. ran ( z e. S \|-> { y e. S \| z C_ y } ) ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " w ) C_ u <-> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F \|` y ) ) e. u ) ) )
46	45	imbi2d	\|- ( ( ph /\ u e. J ) -> ( ( C e. u -> E. w e. ran ( z e. S \|-> { y e. S \| z C_ y } ) ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " w ) C_ u ) <-> ( C e. u -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F \|` y ) ) e. u ) ) ) )
47	46	ralbidva	\|- ( ph -> ( A. u e. J ( C e. u -> E. w e. ran ( z e. S \|-> { y e. S \| z C_ y } ) ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " w ) C_ u ) <-> A. u e. J ( C e. u -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F \|` y ) ) e. u ) ) ) )
48	47	anbi2d	\|- ( ph -> ( ( C e. B /\ A. u e. J ( C e. u -> E. w e. ran ( z e. S \|-> { y e. S \| z C_ y } ) ( ( y e. S \|-> ( G gsum ( F \|` y ) ) ) " w ) C_ u ) ) <-> ( C e. B /\ A. u e. J ( C e. u -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F \|` y ) ) e. u ) ) ) ) )
49	10 19 48	3bitrd	\|- ( ph -> ( C e. ( G tsums F ) <-> ( C e. B /\ A. u e. J ( C e. u -> E. z e. S A. y e. S ( z C_ y -> ( G gsum ( F \|` y ) ) e. u ) ) ) ) )

Metamath Proof Explorer

Theorem eltsms

Proof