Step |
Hyp |
Ref |
Expression |
1 |
|
tsmsmhm.b |
|- B = ( Base ` G ) |
2 |
|
tsmsmhm.j |
|- J = ( TopOpen ` G ) |
3 |
|
tsmsmhm.k |
|- K = ( TopOpen ` H ) |
4 |
|
tsmsmhm.1 |
|- ( ph -> G e. CMnd ) |
5 |
|
tsmsmhm.2 |
|- ( ph -> G e. TopSp ) |
6 |
|
tsmsmhm.3 |
|- ( ph -> H e. CMnd ) |
7 |
|
tsmsmhm.4 |
|- ( ph -> H e. TopSp ) |
8 |
|
tsmsmhm.5 |
|- ( ph -> C e. ( G MndHom H ) ) |
9 |
|
tsmsmhm.6 |
|- ( ph -> C e. ( J Cn K ) ) |
10 |
|
tsmsmhm.a |
|- ( ph -> A e. V ) |
11 |
|
tsmsmhm.f |
|- ( ph -> F : A --> B ) |
12 |
|
tsmsmhm.x |
|- ( ph -> X e. ( G tsums F ) ) |
13 |
1 2
|
istps |
|- ( G e. TopSp <-> J e. ( TopOn ` B ) ) |
14 |
5 13
|
sylib |
|- ( ph -> J e. ( TopOn ` B ) ) |
15 |
|
eqid |
|- ( ~P A i^i Fin ) = ( ~P A i^i Fin ) |
16 |
|
eqid |
|- ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) = ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) |
17 |
|
eqid |
|- ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) = ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) |
18 |
15 16 17 10
|
tsmsfbas |
|- ( ph -> ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) e. ( fBas ` ( ~P A i^i Fin ) ) ) |
19 |
|
fgcl |
|- ( ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) e. ( fBas ` ( ~P A i^i Fin ) ) -> ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) ) |
20 |
18 19
|
syl |
|- ( ph -> ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) ) |
21 |
1 15 4 10 11
|
tsmslem1 |
|- ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` z ) ) e. B ) |
22 |
21
|
fmpttd |
|- ( ph -> ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) : ( ~P A i^i Fin ) --> B ) |
23 |
1 2 15 17 5 10 11
|
tsmsval |
|- ( ph -> ( G tsums F ) = ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) ) |
24 |
12 23
|
eleqtrd |
|- ( ph -> X e. ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) ) |
25 |
1 4 5 10 11
|
tsmscl |
|- ( ph -> ( G tsums F ) C_ B ) |
26 |
25 12
|
sseldd |
|- ( ph -> X e. B ) |
27 |
|
toponuni |
|- ( J e. ( TopOn ` B ) -> B = U. J ) |
28 |
14 27
|
syl |
|- ( ph -> B = U. J ) |
29 |
26 28
|
eleqtrd |
|- ( ph -> X e. U. J ) |
30 |
|
eqid |
|- U. J = U. J |
31 |
30
|
cncnpi |
|- ( ( C e. ( J Cn K ) /\ X e. U. J ) -> C e. ( ( J CnP K ) ` X ) ) |
32 |
9 29 31
|
syl2anc |
|- ( ph -> C e. ( ( J CnP K ) ` X ) ) |
33 |
|
flfcnp |
|- ( ( ( J e. ( TopOn ` B ) /\ ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) /\ ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) : ( ~P A i^i Fin ) --> B ) /\ ( X e. ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) /\ C e. ( ( J CnP K ) ` X ) ) ) -> ( C ` X ) e. ( ( K fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( C o. ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) ) ) |
34 |
14 20 22 24 32 33
|
syl32anc |
|- ( ph -> ( C ` X ) e. ( ( K fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( C o. ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) ) ) |
35 |
|
eqid |
|- ( Base ` H ) = ( Base ` H ) |
36 |
35 3
|
istps |
|- ( H e. TopSp <-> K e. ( TopOn ` ( Base ` H ) ) ) |
37 |
7 36
|
sylib |
|- ( ph -> K e. ( TopOn ` ( Base ` H ) ) ) |
38 |
|
cnf2 |
|- ( ( J e. ( TopOn ` B ) /\ K e. ( TopOn ` ( Base ` H ) ) /\ C e. ( J Cn K ) ) -> C : B --> ( Base ` H ) ) |
39 |
14 37 9 38
|
syl3anc |
|- ( ph -> C : B --> ( Base ` H ) ) |
40 |
|
fco |
|- ( ( C : B --> ( Base ` H ) /\ F : A --> B ) -> ( C o. F ) : A --> ( Base ` H ) ) |
41 |
39 11 40
|
syl2anc |
|- ( ph -> ( C o. F ) : A --> ( Base ` H ) ) |
42 |
35 3 15 17 6 10 41
|
tsmsval |
|- ( ph -> ( H tsums ( C o. F ) ) = ( ( K fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( H gsum ( ( C o. F ) |` z ) ) ) ) ) |
43 |
39 21
|
cofmpt |
|- ( ph -> ( C o. ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) = ( z e. ( ~P A i^i Fin ) |-> ( C ` ( G gsum ( F |` z ) ) ) ) ) |
44 |
|
resco |
|- ( ( C o. F ) |` z ) = ( C o. ( F |` z ) ) |
45 |
44
|
oveq2i |
|- ( H gsum ( ( C o. F ) |` z ) ) = ( H gsum ( C o. ( F |` z ) ) ) |
46 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
47 |
4
|
adantr |
|- ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> G e. CMnd ) |
48 |
6
|
adantr |
|- ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> H e. CMnd ) |
49 |
|
cmnmnd |
|- ( H e. CMnd -> H e. Mnd ) |
50 |
48 49
|
syl |
|- ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> H e. Mnd ) |
51 |
|
elinel2 |
|- ( z e. ( ~P A i^i Fin ) -> z e. Fin ) |
52 |
51
|
adantl |
|- ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> z e. Fin ) |
53 |
8
|
adantr |
|- ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> C e. ( G MndHom H ) ) |
54 |
|
elfpw |
|- ( z e. ( ~P A i^i Fin ) <-> ( z C_ A /\ z e. Fin ) ) |
55 |
54
|
simplbi |
|- ( z e. ( ~P A i^i Fin ) -> z C_ A ) |
56 |
|
fssres |
|- ( ( F : A --> B /\ z C_ A ) -> ( F |` z ) : z --> B ) |
57 |
11 55 56
|
syl2an |
|- ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( F |` z ) : z --> B ) |
58 |
|
fvexd |
|- ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( 0g ` G ) e. _V ) |
59 |
57 52 58
|
fdmfifsupp |
|- ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( F |` z ) finSupp ( 0g ` G ) ) |
60 |
1 46 47 50 52 53 57 59
|
gsummhm |
|- ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( H gsum ( C o. ( F |` z ) ) ) = ( C ` ( G gsum ( F |` z ) ) ) ) |
61 |
45 60
|
syl5eq |
|- ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( H gsum ( ( C o. F ) |` z ) ) = ( C ` ( G gsum ( F |` z ) ) ) ) |
62 |
61
|
mpteq2dva |
|- ( ph -> ( z e. ( ~P A i^i Fin ) |-> ( H gsum ( ( C o. F ) |` z ) ) ) = ( z e. ( ~P A i^i Fin ) |-> ( C ` ( G gsum ( F |` z ) ) ) ) ) |
63 |
43 62
|
eqtr4d |
|- ( ph -> ( C o. ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) = ( z e. ( ~P A i^i Fin ) |-> ( H gsum ( ( C o. F ) |` z ) ) ) ) |
64 |
63
|
fveq2d |
|- ( ph -> ( ( K fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( C o. ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) ) = ( ( K fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( H gsum ( ( C o. F ) |` z ) ) ) ) ) |
65 |
42 64
|
eqtr4d |
|- ( ph -> ( H tsums ( C o. F ) ) = ( ( K fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( C o. ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) ) ) |
66 |
34 65
|
eleqtrrd |
|- ( ph -> ( C ` X ) e. ( H tsums ( C o. F ) ) ) |