Step |
Hyp |
Ref |
Expression |
1 |
|
tsmsres.b |
|- B = ( Base ` G ) |
2 |
|
tsmsres.z |
|- .0. = ( 0g ` G ) |
3 |
|
tsmsres.1 |
|- ( ph -> G e. CMnd ) |
4 |
|
tsmsres.2 |
|- ( ph -> G e. TopSp ) |
5 |
|
tsmsres.a |
|- ( ph -> A e. V ) |
6 |
|
tsmsres.f |
|- ( ph -> F : A --> B ) |
7 |
|
tsmsres.s |
|- ( ph -> ( F supp .0. ) C_ W ) |
8 |
|
inss1 |
|- ( A i^i W ) C_ A |
9 |
8
|
sspwi |
|- ~P ( A i^i W ) C_ ~P A |
10 |
|
ssrin |
|- ( ~P ( A i^i W ) C_ ~P A -> ( ~P ( A i^i W ) i^i Fin ) C_ ( ~P A i^i Fin ) ) |
11 |
9 10
|
ax-mp |
|- ( ~P ( A i^i W ) i^i Fin ) C_ ( ~P A i^i Fin ) |
12 |
|
simpr |
|- ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) -> a e. ( ~P ( A i^i W ) i^i Fin ) ) |
13 |
11 12
|
sselid |
|- ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) -> a e. ( ~P A i^i Fin ) ) |
14 |
|
elfpw |
|- ( z e. ( ~P A i^i Fin ) <-> ( z C_ A /\ z e. Fin ) ) |
15 |
14
|
simplbi |
|- ( z e. ( ~P A i^i Fin ) -> z C_ A ) |
16 |
15
|
adantl |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> z C_ A ) |
17 |
16
|
ssrind |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( z i^i W ) C_ ( A i^i W ) ) |
18 |
|
elinel2 |
|- ( z e. ( ~P A i^i Fin ) -> z e. Fin ) |
19 |
18
|
adantl |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> z e. Fin ) |
20 |
|
inss1 |
|- ( z i^i W ) C_ z |
21 |
|
ssfi |
|- ( ( z e. Fin /\ ( z i^i W ) C_ z ) -> ( z i^i W ) e. Fin ) |
22 |
19 20 21
|
sylancl |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( z i^i W ) e. Fin ) |
23 |
|
elfpw |
|- ( ( z i^i W ) e. ( ~P ( A i^i W ) i^i Fin ) <-> ( ( z i^i W ) C_ ( A i^i W ) /\ ( z i^i W ) e. Fin ) ) |
24 |
17 22 23
|
sylanbrc |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( z i^i W ) e. ( ~P ( A i^i W ) i^i Fin ) ) |
25 |
|
sseq2 |
|- ( b = ( z i^i W ) -> ( a C_ b <-> a C_ ( z i^i W ) ) ) |
26 |
|
ssin |
|- ( ( a C_ z /\ a C_ W ) <-> a C_ ( z i^i W ) ) |
27 |
25 26
|
bitr4di |
|- ( b = ( z i^i W ) -> ( a C_ b <-> ( a C_ z /\ a C_ W ) ) ) |
28 |
|
reseq2 |
|- ( b = ( z i^i W ) -> ( ( F |` W ) |` b ) = ( ( F |` W ) |` ( z i^i W ) ) ) |
29 |
|
inss2 |
|- ( z i^i W ) C_ W |
30 |
|
resabs1 |
|- ( ( z i^i W ) C_ W -> ( ( F |` W ) |` ( z i^i W ) ) = ( F |` ( z i^i W ) ) ) |
31 |
29 30
|
ax-mp |
|- ( ( F |` W ) |` ( z i^i W ) ) = ( F |` ( z i^i W ) ) |
32 |
28 31
|
eqtrdi |
|- ( b = ( z i^i W ) -> ( ( F |` W ) |` b ) = ( F |` ( z i^i W ) ) ) |
33 |
32
|
oveq2d |
|- ( b = ( z i^i W ) -> ( G gsum ( ( F |` W ) |` b ) ) = ( G gsum ( F |` ( z i^i W ) ) ) ) |
34 |
33
|
eleq1d |
|- ( b = ( z i^i W ) -> ( ( G gsum ( ( F |` W ) |` b ) ) e. u <-> ( G gsum ( F |` ( z i^i W ) ) ) e. u ) ) |
35 |
27 34
|
imbi12d |
|- ( b = ( z i^i W ) -> ( ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) <-> ( ( a C_ z /\ a C_ W ) -> ( G gsum ( F |` ( z i^i W ) ) ) e. u ) ) ) |
36 |
35
|
rspcv |
|- ( ( z i^i W ) e. ( ~P ( A i^i W ) i^i Fin ) -> ( A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) -> ( ( a C_ z /\ a C_ W ) -> ( G gsum ( F |` ( z i^i W ) ) ) e. u ) ) ) |
37 |
24 36
|
syl |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) -> ( ( a C_ z /\ a C_ W ) -> ( G gsum ( F |` ( z i^i W ) ) ) e. u ) ) ) |
38 |
|
elfpw |
|- ( a e. ( ~P ( A i^i W ) i^i Fin ) <-> ( a C_ ( A i^i W ) /\ a e. Fin ) ) |
39 |
38
|
simplbi |
|- ( a e. ( ~P ( A i^i W ) i^i Fin ) -> a C_ ( A i^i W ) ) |
40 |
39
|
ad2antlr |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> a C_ ( A i^i W ) ) |
41 |
|
inss2 |
|- ( A i^i W ) C_ W |
42 |
40 41
|
sstrdi |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> a C_ W ) |
43 |
42
|
biantrud |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( a C_ z <-> ( a C_ z /\ a C_ W ) ) ) |
44 |
3
|
ad2antrr |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> G e. CMnd ) |
45 |
6
|
ad2antrr |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> F : A --> B ) |
46 |
45 16
|
fssresd |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( F |` z ) : z --> B ) |
47 |
6 5
|
fexd |
|- ( ph -> F e. _V ) |
48 |
47
|
ad2antrr |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> F e. _V ) |
49 |
2
|
fvexi |
|- .0. e. _V |
50 |
|
ressuppss |
|- ( ( F e. _V /\ .0. e. _V ) -> ( ( F |` z ) supp .0. ) C_ ( F supp .0. ) ) |
51 |
48 49 50
|
sylancl |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( ( F |` z ) supp .0. ) C_ ( F supp .0. ) ) |
52 |
7
|
ad2antrr |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( F supp .0. ) C_ W ) |
53 |
51 52
|
sstrd |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( ( F |` z ) supp .0. ) C_ W ) |
54 |
49
|
a1i |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> .0. e. _V ) |
55 |
46 19 54
|
fdmfifsupp |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( F |` z ) finSupp .0. ) |
56 |
1 2 44 19 46 53 55
|
gsumres |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( G gsum ( ( F |` z ) |` W ) ) = ( G gsum ( F |` z ) ) ) |
57 |
|
resres |
|- ( ( F |` z ) |` W ) = ( F |` ( z i^i W ) ) |
58 |
57
|
oveq2i |
|- ( G gsum ( ( F |` z ) |` W ) ) = ( G gsum ( F |` ( z i^i W ) ) ) |
59 |
56 58
|
eqtr3di |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` z ) ) = ( G gsum ( F |` ( z i^i W ) ) ) ) |
60 |
59
|
eleq1d |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( ( G gsum ( F |` z ) ) e. u <-> ( G gsum ( F |` ( z i^i W ) ) ) e. u ) ) |
61 |
43 60
|
imbi12d |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( ( a C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( ( a C_ z /\ a C_ W ) -> ( G gsum ( F |` ( z i^i W ) ) ) e. u ) ) ) |
62 |
37 61
|
sylibrd |
|- ( ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) -> ( a C_ z -> ( G gsum ( F |` z ) ) e. u ) ) ) |
63 |
62
|
ralrimdva |
|- ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) -> A. z e. ( ~P A i^i Fin ) ( a C_ z -> ( G gsum ( F |` z ) ) e. u ) ) ) |
64 |
|
sseq1 |
|- ( y = a -> ( y C_ z <-> a C_ z ) ) |
65 |
64
|
rspceaimv |
|- ( ( a e. ( ~P A i^i Fin ) /\ A. z e. ( ~P A i^i Fin ) ( a 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 ) ) |
66 |
13 63 65
|
syl6an |
|- ( ( ph /\ a e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) 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 ) ) ) |
67 |
66
|
rexlimdva |
|- ( ph -> ( E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) 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 ) ) ) |
68 |
|
elfpw |
|- ( y e. ( ~P A i^i Fin ) <-> ( y C_ A /\ y e. Fin ) ) |
69 |
68
|
simplbi |
|- ( y e. ( ~P A i^i Fin ) -> y C_ A ) |
70 |
69
|
adantl |
|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y C_ A ) |
71 |
70
|
ssrind |
|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( y i^i W ) C_ ( A i^i W ) ) |
72 |
|
elinel2 |
|- ( y e. ( ~P A i^i Fin ) -> y e. Fin ) |
73 |
72
|
adantl |
|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin ) |
74 |
|
inss1 |
|- ( y i^i W ) C_ y |
75 |
|
ssfi |
|- ( ( y e. Fin /\ ( y i^i W ) C_ y ) -> ( y i^i W ) e. Fin ) |
76 |
73 74 75
|
sylancl |
|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( y i^i W ) e. Fin ) |
77 |
|
elfpw |
|- ( ( y i^i W ) e. ( ~P ( A i^i W ) i^i Fin ) <-> ( ( y i^i W ) C_ ( A i^i W ) /\ ( y i^i W ) e. Fin ) ) |
78 |
71 76 77
|
sylanbrc |
|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( y i^i W ) e. ( ~P ( A i^i W ) i^i Fin ) ) |
79 |
69
|
ad2antlr |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> y C_ A ) |
80 |
|
elfpw |
|- ( b e. ( ~P ( A i^i W ) i^i Fin ) <-> ( b C_ ( A i^i W ) /\ b e. Fin ) ) |
81 |
80
|
simplbi |
|- ( b e. ( ~P ( A i^i W ) i^i Fin ) -> b C_ ( A i^i W ) ) |
82 |
81
|
adantl |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> b C_ ( A i^i W ) ) |
83 |
82 8
|
sstrdi |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> b C_ A ) |
84 |
79 83
|
unssd |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( y u. b ) C_ A ) |
85 |
|
elinel2 |
|- ( b e. ( ~P ( A i^i W ) i^i Fin ) -> b e. Fin ) |
86 |
|
unfi |
|- ( ( y e. Fin /\ b e. Fin ) -> ( y u. b ) e. Fin ) |
87 |
73 85 86
|
syl2an |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( y u. b ) e. Fin ) |
88 |
|
elfpw |
|- ( ( y u. b ) e. ( ~P A i^i Fin ) <-> ( ( y u. b ) C_ A /\ ( y u. b ) e. Fin ) ) |
89 |
84 87 88
|
sylanbrc |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( y u. b ) e. ( ~P A i^i Fin ) ) |
90 |
|
ssun1 |
|- y C_ ( y u. b ) |
91 |
|
id |
|- ( z = ( y u. b ) -> z = ( y u. b ) ) |
92 |
90 91
|
sseqtrrid |
|- ( z = ( y u. b ) -> y C_ z ) |
93 |
|
pm5.5 |
|- ( y C_ z -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` z ) ) e. u ) ) |
94 |
92 93
|
syl |
|- ( z = ( y u. b ) -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` z ) ) e. u ) ) |
95 |
|
reseq2 |
|- ( z = ( y u. b ) -> ( F |` z ) = ( F |` ( y u. b ) ) ) |
96 |
95
|
oveq2d |
|- ( z = ( y u. b ) -> ( G gsum ( F |` z ) ) = ( G gsum ( F |` ( y u. b ) ) ) ) |
97 |
96
|
eleq1d |
|- ( z = ( y u. b ) -> ( ( G gsum ( F |` z ) ) e. u <-> ( G gsum ( F |` ( y u. b ) ) ) e. u ) ) |
98 |
94 97
|
bitrd |
|- ( z = ( y u. b ) -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` ( y u. b ) ) ) e. u ) ) |
99 |
98
|
rspcv |
|- ( ( y u. b ) 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. b ) ) ) e. u ) ) |
100 |
89 99
|
syl |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) 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. b ) ) ) e. u ) ) |
101 |
3
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> G e. CMnd ) |
102 |
87
|
adantrr |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( y u. b ) e. Fin ) |
103 |
6
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> F : A --> B ) |
104 |
84
|
adantrr |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( y u. b ) C_ A ) |
105 |
103 104
|
fssresd |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( F |` ( y u. b ) ) : ( y u. b ) --> B ) |
106 |
47 49
|
jctir |
|- ( ph -> ( F e. _V /\ .0. e. _V ) ) |
107 |
106
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( F e. _V /\ .0. e. _V ) ) |
108 |
|
ressuppss |
|- ( ( F e. _V /\ .0. e. _V ) -> ( ( F |` ( y u. b ) ) supp .0. ) C_ ( F supp .0. ) ) |
109 |
107 108
|
syl |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( F |` ( y u. b ) ) supp .0. ) C_ ( F supp .0. ) ) |
110 |
7
|
ad2antrr |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( F supp .0. ) C_ W ) |
111 |
109 110
|
sstrd |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( F |` ( y u. b ) ) supp .0. ) C_ W ) |
112 |
49
|
a1i |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> .0. e. _V ) |
113 |
105 102 112
|
fdmfifsupp |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( F |` ( y u. b ) ) finSupp .0. ) |
114 |
1 2 101 102 105 111 113
|
gsumres |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( G gsum ( ( F |` ( y u. b ) ) |` W ) ) = ( G gsum ( F |` ( y u. b ) ) ) ) |
115 |
|
resres |
|- ( ( F |` ( y u. b ) ) |` W ) = ( F |` ( ( y u. b ) i^i W ) ) |
116 |
|
indir |
|- ( ( y u. b ) i^i W ) = ( ( y i^i W ) u. ( b i^i W ) ) |
117 |
82 41
|
sstrdi |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> b C_ W ) |
118 |
117
|
adantrr |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> b C_ W ) |
119 |
|
df-ss |
|- ( b C_ W <-> ( b i^i W ) = b ) |
120 |
118 119
|
sylib |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( b i^i W ) = b ) |
121 |
120
|
uneq2d |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( y i^i W ) u. ( b i^i W ) ) = ( ( y i^i W ) u. b ) ) |
122 |
|
simprr |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( y i^i W ) C_ b ) |
123 |
|
ssequn1 |
|- ( ( y i^i W ) C_ b <-> ( ( y i^i W ) u. b ) = b ) |
124 |
122 123
|
sylib |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( y i^i W ) u. b ) = b ) |
125 |
121 124
|
eqtrd |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( y i^i W ) u. ( b i^i W ) ) = b ) |
126 |
116 125
|
eqtrid |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( y u. b ) i^i W ) = b ) |
127 |
126
|
reseq2d |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( F |` ( ( y u. b ) i^i W ) ) = ( F |` b ) ) |
128 |
115 127
|
eqtrid |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( F |` ( y u. b ) ) |` W ) = ( F |` b ) ) |
129 |
118
|
resabs1d |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( F |` W ) |` b ) = ( F |` b ) ) |
130 |
128 129
|
eqtr4d |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( F |` ( y u. b ) ) |` W ) = ( ( F |` W ) |` b ) ) |
131 |
130
|
oveq2d |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( G gsum ( ( F |` ( y u. b ) ) |` W ) ) = ( G gsum ( ( F |` W ) |` b ) ) ) |
132 |
114 131
|
eqtr3d |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( G gsum ( F |` ( y u. b ) ) ) = ( G gsum ( ( F |` W ) |` b ) ) ) |
133 |
132
|
eleq1d |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( G gsum ( F |` ( y u. b ) ) ) e. u <-> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) |
134 |
133
|
biimpd |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ ( b e. ( ~P ( A i^i W ) i^i Fin ) /\ ( y i^i W ) C_ b ) ) -> ( ( G gsum ( F |` ( y u. b ) ) ) e. u -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) |
135 |
134
|
expr |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( ( y i^i W ) C_ b -> ( ( G gsum ( F |` ( y u. b ) ) ) e. u -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) ) |
136 |
135
|
com23 |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( ( G gsum ( F |` ( y u. b ) ) ) e. u -> ( ( y i^i W ) C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) ) |
137 |
100 136
|
syld |
|- ( ( ( ph /\ y e. ( ~P A i^i Fin ) ) /\ b e. ( ~P ( A i^i W ) i^i Fin ) ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> ( ( y i^i W ) C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) ) |
138 |
137
|
ralrimdva |
|- ( ( ph /\ 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. b e. ( ~P ( A i^i W ) i^i Fin ) ( ( y i^i W ) C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) ) |
139 |
|
sseq1 |
|- ( a = ( y i^i W ) -> ( a C_ b <-> ( y i^i W ) C_ b ) ) |
140 |
139
|
rspceaimv |
|- ( ( ( y i^i W ) e. ( ~P ( A i^i W ) i^i Fin ) /\ A. b e. ( ~P ( A i^i W ) i^i Fin ) ( ( y i^i W ) C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) |
141 |
78 138 140
|
syl6an |
|- ( ( ph /\ y e. ( ~P A i^i Fin ) ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) ) |
142 |
141
|
rexlimdva |
|- ( ph -> ( 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 ) -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) ) |
143 |
67 142
|
impbid |
|- ( ph -> ( E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) 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 ) ) ) |
144 |
143
|
imbi2d |
|- ( ph -> ( ( x e. u -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) <-> ( 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 ) ) ) ) |
145 |
144
|
ralbidv |
|- ( ph -> ( A. u e. ( TopOpen ` G ) ( x e. u -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) <-> A. u e. ( TopOpen ` G ) ( 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 ) ) ) ) |
146 |
145
|
anbi2d |
|- ( ph -> ( ( x e. B /\ A. u e. ( TopOpen ` G ) ( x e. u -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) ) <-> ( x e. B /\ A. u e. ( TopOpen ` G ) ( 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 ) ) ) ) ) |
147 |
|
eqid |
|- ( TopOpen ` G ) = ( TopOpen ` G ) |
148 |
|
eqid |
|- ( ~P ( A i^i W ) i^i Fin ) = ( ~P ( A i^i W ) i^i Fin ) |
149 |
|
inex1g |
|- ( A e. V -> ( A i^i W ) e. _V ) |
150 |
5 149
|
syl |
|- ( ph -> ( A i^i W ) e. _V ) |
151 |
|
fssres |
|- ( ( F : A --> B /\ ( A i^i W ) C_ A ) -> ( F |` ( A i^i W ) ) : ( A i^i W ) --> B ) |
152 |
6 8 151
|
sylancl |
|- ( ph -> ( F |` ( A i^i W ) ) : ( A i^i W ) --> B ) |
153 |
|
resres |
|- ( ( F |` A ) |` W ) = ( F |` ( A i^i W ) ) |
154 |
|
ffn |
|- ( F : A --> B -> F Fn A ) |
155 |
|
fnresdm |
|- ( F Fn A -> ( F |` A ) = F ) |
156 |
6 154 155
|
3syl |
|- ( ph -> ( F |` A ) = F ) |
157 |
156
|
reseq1d |
|- ( ph -> ( ( F |` A ) |` W ) = ( F |` W ) ) |
158 |
153 157
|
eqtr3id |
|- ( ph -> ( F |` ( A i^i W ) ) = ( F |` W ) ) |
159 |
158
|
feq1d |
|- ( ph -> ( ( F |` ( A i^i W ) ) : ( A i^i W ) --> B <-> ( F |` W ) : ( A i^i W ) --> B ) ) |
160 |
152 159
|
mpbid |
|- ( ph -> ( F |` W ) : ( A i^i W ) --> B ) |
161 |
1 147 148 3 4 150 160
|
eltsms |
|- ( ph -> ( x e. ( G tsums ( F |` W ) ) <-> ( x e. B /\ A. u e. ( TopOpen ` G ) ( x e. u -> E. a e. ( ~P ( A i^i W ) i^i Fin ) A. b e. ( ~P ( A i^i W ) i^i Fin ) ( a C_ b -> ( G gsum ( ( F |` W ) |` b ) ) e. u ) ) ) ) ) |
162 |
|
eqid |
|- ( ~P A i^i Fin ) = ( ~P A i^i Fin ) |
163 |
1 147 162 3 4 5 6
|
eltsms |
|- ( ph -> ( x e. ( G tsums F ) <-> ( x e. B /\ A. u e. ( TopOpen ` G ) ( 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 ) ) ) ) ) |
164 |
146 161 163
|
3bitr4d |
|- ( ph -> ( x e. ( G tsums ( F |` W ) ) <-> x e. ( G tsums F ) ) ) |
165 |
164
|
eqrdv |
|- ( ph -> ( G tsums ( F |` W ) ) = ( G tsums F ) ) |