Step |
Hyp |
Ref |
Expression |
1 |
|
tsmsid.b |
|- B = ( Base ` G ) |
2 |
|
tsmsid.z |
|- .0. = ( 0g ` G ) |
3 |
|
tsmsid.1 |
|- ( ph -> G e. CMnd ) |
4 |
|
tsmsid.2 |
|- ( ph -> G e. TopSp ) |
5 |
|
tsmsid.a |
|- ( ph -> A e. V ) |
6 |
|
tsmsid.f |
|- ( ph -> F : A --> B ) |
7 |
|
tsmsid.w |
|- ( ph -> F finSupp .0. ) |
8 |
|
tsmsgsum.j |
|- J = ( TopOpen ` G ) |
9 |
1 8
|
istps |
|- ( G e. TopSp <-> J e. ( TopOn ` B ) ) |
10 |
4 9
|
sylib |
|- ( ph -> J e. ( TopOn ` B ) ) |
11 |
|
toponuni |
|- ( J e. ( TopOn ` B ) -> B = U. J ) |
12 |
10 11
|
syl |
|- ( ph -> B = U. J ) |
13 |
12
|
eleq2d |
|- ( ph -> ( x e. B <-> x e. U. J ) ) |
14 |
|
elfpw |
|- ( y e. ( ~P A i^i Fin ) <-> ( y C_ A /\ y e. Fin ) ) |
15 |
14
|
simplbi |
|- ( y e. ( ~P A i^i Fin ) -> y C_ A ) |
16 |
15
|
adantl |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> y C_ A ) |
17 |
|
suppssdm |
|- ( F supp .0. ) C_ dom F |
18 |
17 6
|
fssdm |
|- ( ph -> ( F supp .0. ) C_ A ) |
19 |
18
|
ad2antrr |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( F supp .0. ) C_ A ) |
20 |
16 19
|
unssd |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( y u. ( F supp .0. ) ) C_ A ) |
21 |
|
elinel2 |
|- ( y e. ( ~P A i^i Fin ) -> y e. Fin ) |
22 |
21
|
adantl |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin ) |
23 |
7
|
ad2antrr |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> F finSupp .0. ) |
24 |
23
|
fsuppimpd |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( F supp .0. ) e. Fin ) |
25 |
|
unfi |
|- ( ( y e. Fin /\ ( F supp .0. ) e. Fin ) -> ( y u. ( F supp .0. ) ) e. Fin ) |
26 |
22 24 25
|
syl2anc |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( y u. ( F supp .0. ) ) e. Fin ) |
27 |
|
elfpw |
|- ( ( y u. ( F supp .0. ) ) e. ( ~P A i^i Fin ) <-> ( ( y u. ( F supp .0. ) ) C_ A /\ ( y u. ( F supp .0. ) ) e. Fin ) ) |
28 |
20 26 27
|
sylanbrc |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( y u. ( F supp .0. ) ) e. ( ~P A i^i Fin ) ) |
29 |
|
ssun1 |
|- y C_ ( y u. ( F supp .0. ) ) |
30 |
|
id |
|- ( z = ( y u. ( F supp .0. ) ) -> z = ( y u. ( F supp .0. ) ) ) |
31 |
29 30
|
sseqtrrid |
|- ( z = ( y u. ( F supp .0. ) ) -> y C_ z ) |
32 |
|
pm5.5 |
|- ( y C_ z -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` z ) ) e. u ) ) |
33 |
31 32
|
syl |
|- ( z = ( y u. ( F supp .0. ) ) -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` z ) ) e. u ) ) |
34 |
|
reseq2 |
|- ( z = ( y u. ( F supp .0. ) ) -> ( F |` z ) = ( F |` ( y u. ( F supp .0. ) ) ) ) |
35 |
34
|
oveq2d |
|- ( z = ( y u. ( F supp .0. ) ) -> ( G gsum ( F |` z ) ) = ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) ) |
36 |
35
|
eleq1d |
|- ( z = ( y u. ( F supp .0. ) ) -> ( ( G gsum ( F |` z ) ) e. u <-> ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) e. u ) ) |
37 |
33 36
|
bitrd |
|- ( z = ( y u. ( F supp .0. ) ) -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) e. u ) ) |
38 |
37
|
rspcv |
|- ( ( y u. ( F supp .0. ) ) e. ( ~P A i^i Fin ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) e. u ) ) |
39 |
28 38
|
syl |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) e. u ) ) |
40 |
3
|
ad2antrr |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> G e. CMnd ) |
41 |
5
|
ad2antrr |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> A e. V ) |
42 |
6
|
ad2antrr |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> F : A --> B ) |
43 |
|
ssun2 |
|- ( F supp .0. ) C_ ( y u. ( F supp .0. ) ) |
44 |
43
|
a1i |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( F supp .0. ) C_ ( y u. ( F supp .0. ) ) ) |
45 |
1 2 40 41 42 44 23
|
gsumres |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) = ( G gsum F ) ) |
46 |
45
|
eleq1d |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) e. u <-> ( G gsum F ) e. u ) ) |
47 |
39 46
|
sylibd |
|- ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> ( G gsum F ) e. u ) ) |
48 |
47
|
rexlimdva |
|- ( ( ph /\ u e. J ) -> ( E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> ( G gsum F ) e. u ) ) |
49 |
7
|
fsuppimpd |
|- ( ph -> ( F supp .0. ) e. Fin ) |
50 |
|
elfpw |
|- ( ( F supp .0. ) e. ( ~P A i^i Fin ) <-> ( ( F supp .0. ) C_ A /\ ( F supp .0. ) e. Fin ) ) |
51 |
18 49 50
|
sylanbrc |
|- ( ph -> ( F supp .0. ) e. ( ~P A i^i Fin ) ) |
52 |
3
|
ad2antrr |
|- ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> G e. CMnd ) |
53 |
5
|
ad2antrr |
|- ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> A e. V ) |
54 |
6
|
ad2antrr |
|- ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> F : A --> B ) |
55 |
|
simprr |
|- ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> ( F supp .0. ) C_ z ) |
56 |
7
|
ad2antrr |
|- ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> F finSupp .0. ) |
57 |
1 2 52 53 54 55 56
|
gsumres |
|- ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> ( G gsum ( F |` z ) ) = ( G gsum F ) ) |
58 |
|
simplrr |
|- ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> ( G gsum F ) e. u ) |
59 |
57 58
|
eqeltrd |
|- ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> ( G gsum ( F |` z ) ) e. u ) |
60 |
59
|
expr |
|- ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( ( F supp .0. ) C_ z -> ( G gsum ( F |` z ) ) e. u ) ) |
61 |
60
|
ralrimiva |
|- ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) -> A. z e. ( ~P A i^i Fin ) ( ( F supp .0. ) C_ z -> ( G gsum ( F |` z ) ) e. u ) ) |
62 |
|
sseq1 |
|- ( y = ( F supp .0. ) -> ( y C_ z <-> ( F supp .0. ) C_ z ) ) |
63 |
62
|
rspceaimv |
|- ( ( ( F supp .0. ) e. ( ~P A i^i Fin ) /\ A. z e. ( ~P A i^i Fin ) ( ( F supp .0. ) C_ z -> ( G gsum ( F |` z ) ) e. u ) ) -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) |
64 |
51 61 63
|
syl2an2r |
|- ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) |
65 |
64
|
expr |
|- ( ( ph /\ u e. J ) -> ( ( G gsum F ) e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) ) |
66 |
48 65
|
impbid |
|- ( ( ph /\ u e. J ) -> ( E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum F ) e. u ) ) |
67 |
|
disjsn |
|- ( ( u i^i { ( G gsum F ) } ) = (/) <-> -. ( G gsum F ) e. u ) |
68 |
67
|
necon2abii |
|- ( ( G gsum F ) e. u <-> ( u i^i { ( G gsum F ) } ) =/= (/) ) |
69 |
66 68
|
bitrdi |
|- ( ( ph /\ u e. J ) -> ( E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( u i^i { ( G gsum F ) } ) =/= (/) ) ) |
70 |
69
|
imbi2d |
|- ( ( ph /\ u e. J ) -> ( ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) <-> ( x e. u -> ( u i^i { ( G gsum F ) } ) =/= (/) ) ) ) |
71 |
70
|
ralbidva |
|- ( ph -> ( A. u e. J ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) <-> A. u e. J ( x e. u -> ( u i^i { ( G gsum F ) } ) =/= (/) ) ) ) |
72 |
13 71
|
anbi12d |
|- ( ph -> ( ( x e. B /\ A. u e. J ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) ) <-> ( x e. U. J /\ A. u e. J ( x e. u -> ( u i^i { ( G gsum F ) } ) =/= (/) ) ) ) ) |
73 |
|
eqid |
|- ( ~P A i^i Fin ) = ( ~P A i^i Fin ) |
74 |
1 8 73 3 4 5 6
|
eltsms |
|- ( ph -> ( x e. ( G tsums F ) <-> ( x e. B /\ A. u e. J ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) ) ) ) |
75 |
|
topontop |
|- ( J e. ( TopOn ` B ) -> J e. Top ) |
76 |
10 75
|
syl |
|- ( ph -> J e. Top ) |
77 |
1 2 3 5 6 7
|
gsumcl |
|- ( ph -> ( G gsum F ) e. B ) |
78 |
77
|
snssd |
|- ( ph -> { ( G gsum F ) } C_ B ) |
79 |
78 12
|
sseqtrd |
|- ( ph -> { ( G gsum F ) } C_ U. J ) |
80 |
|
eqid |
|- U. J = U. J |
81 |
80
|
elcls2 |
|- ( ( J e. Top /\ { ( G gsum F ) } C_ U. J ) -> ( x e. ( ( cls ` J ) ` { ( G gsum F ) } ) <-> ( x e. U. J /\ A. u e. J ( x e. u -> ( u i^i { ( G gsum F ) } ) =/= (/) ) ) ) ) |
82 |
76 79 81
|
syl2anc |
|- ( ph -> ( x e. ( ( cls ` J ) ` { ( G gsum F ) } ) <-> ( x e. U. J /\ A. u e. J ( x e. u -> ( u i^i { ( G gsum F ) } ) =/= (/) ) ) ) ) |
83 |
72 74 82
|
3bitr4d |
|- ( ph -> ( x e. ( G tsums F ) <-> x e. ( ( cls ` J ) ` { ( G gsum F ) } ) ) ) |
84 |
83
|
eqrdv |
|- ( ph -> ( G tsums F ) = ( ( cls ` J ) ` { ( G gsum F ) } ) ) |