Step |
Hyp |
Ref |
Expression |
1 |
|
tsmsxp.b |
|- B = ( Base ` G ) |
2 |
|
tsmsxp.g |
|- ( ph -> G e. CMnd ) |
3 |
|
tsmsxp.2 |
|- ( ph -> G e. TopGrp ) |
4 |
|
tsmsxp.a |
|- ( ph -> A e. V ) |
5 |
|
tsmsxp.c |
|- ( ph -> C e. W ) |
6 |
|
tsmsxp.f |
|- ( ph -> F : ( A X. C ) --> B ) |
7 |
|
tsmsxp.h |
|- ( ph -> H : A --> B ) |
8 |
|
tsmsxp.1 |
|- ( ( ph /\ j e. A ) -> ( H ` j ) e. ( G tsums ( k e. C |-> ( j F k ) ) ) ) |
9 |
|
tsmsxp.j |
|- J = ( TopOpen ` G ) |
10 |
|
tsmsxp.z |
|- .0. = ( 0g ` G ) |
11 |
|
tsmsxp.p |
|- .+ = ( +g ` G ) |
12 |
|
tsmsxp.m |
|- .- = ( -g ` G ) |
13 |
|
tsmsxp.l |
|- ( ph -> L e. J ) |
14 |
|
tsmsxp.3 |
|- ( ph -> .0. e. L ) |
15 |
|
tsmsxp.k |
|- ( ph -> K e. ( ~P A i^i Fin ) ) |
16 |
|
tsmsxp.4 |
|- ( ph -> A. c e. S A. d e. T ( c .+ d ) e. U ) |
17 |
|
tsmsxp.n |
|- ( ph -> N e. ( ~P C i^i Fin ) ) |
18 |
|
tsmsxp.s |
|- ( ph -> D C_ ( K X. N ) ) |
19 |
|
tsmsxp.x |
|- ( ph -> A. x e. K ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. N ) ) ) ) e. L ) |
20 |
|
tsmsxp.5 |
|- ( ph -> ( G gsum ( F |` ( K X. N ) ) ) e. S ) |
21 |
|
tsmsxp.6 |
|- ( ph -> A. g e. ( L ^m K ) ( G gsum g ) e. T ) |
22 |
|
tgpgrp |
|- ( G e. TopGrp -> G e. Grp ) |
23 |
3 22
|
syl |
|- ( ph -> G e. Grp ) |
24 |
|
isabl |
|- ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) ) |
25 |
23 2 24
|
sylanbrc |
|- ( ph -> G e. Abel ) |
26 |
15
|
elin2d |
|- ( ph -> K e. Fin ) |
27 |
17
|
elin2d |
|- ( ph -> N e. Fin ) |
28 |
|
xpfi |
|- ( ( K e. Fin /\ N e. Fin ) -> ( K X. N ) e. Fin ) |
29 |
26 27 28
|
syl2anc |
|- ( ph -> ( K X. N ) e. Fin ) |
30 |
|
elfpw |
|- ( K e. ( ~P A i^i Fin ) <-> ( K C_ A /\ K e. Fin ) ) |
31 |
30
|
simplbi |
|- ( K e. ( ~P A i^i Fin ) -> K C_ A ) |
32 |
15 31
|
syl |
|- ( ph -> K C_ A ) |
33 |
|
elfpw |
|- ( N e. ( ~P C i^i Fin ) <-> ( N C_ C /\ N e. Fin ) ) |
34 |
33
|
simplbi |
|- ( N e. ( ~P C i^i Fin ) -> N C_ C ) |
35 |
17 34
|
syl |
|- ( ph -> N C_ C ) |
36 |
|
xpss12 |
|- ( ( K C_ A /\ N C_ C ) -> ( K X. N ) C_ ( A X. C ) ) |
37 |
32 35 36
|
syl2anc |
|- ( ph -> ( K X. N ) C_ ( A X. C ) ) |
38 |
6 37
|
fssresd |
|- ( ph -> ( F |` ( K X. N ) ) : ( K X. N ) --> B ) |
39 |
38 29 14
|
fdmfifsupp |
|- ( ph -> ( F |` ( K X. N ) ) finSupp .0. ) |
40 |
1 10 2 29 38 39
|
gsumcl |
|- ( ph -> ( G gsum ( F |` ( K X. N ) ) ) e. B ) |
41 |
7 32
|
fssresd |
|- ( ph -> ( H |` K ) : K --> B ) |
42 |
41 26 14
|
fdmfifsupp |
|- ( ph -> ( H |` K ) finSupp .0. ) |
43 |
1 10 2 15 41 42
|
gsumcl |
|- ( ph -> ( G gsum ( H |` K ) ) e. B ) |
44 |
1 11 12
|
ablpncan3 |
|- ( ( G e. Abel /\ ( ( G gsum ( F |` ( K X. N ) ) ) e. B /\ ( G gsum ( H |` K ) ) e. B ) ) -> ( ( G gsum ( F |` ( K X. N ) ) ) .+ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) = ( G gsum ( H |` K ) ) ) |
45 |
25 40 43 44
|
syl12anc |
|- ( ph -> ( ( G gsum ( F |` ( K X. N ) ) ) .+ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) = ( G gsum ( H |` K ) ) ) |
46 |
2
|
adantr |
|- ( ( ph /\ y e. K ) -> G e. CMnd ) |
47 |
|
snfi |
|- { y } e. Fin |
48 |
27
|
adantr |
|- ( ( ph /\ y e. K ) -> N e. Fin ) |
49 |
|
xpfi |
|- ( ( { y } e. Fin /\ N e. Fin ) -> ( { y } X. N ) e. Fin ) |
50 |
47 48 49
|
sylancr |
|- ( ( ph /\ y e. K ) -> ( { y } X. N ) e. Fin ) |
51 |
6
|
adantr |
|- ( ( ph /\ y e. K ) -> F : ( A X. C ) --> B ) |
52 |
32
|
sselda |
|- ( ( ph /\ y e. K ) -> y e. A ) |
53 |
52
|
snssd |
|- ( ( ph /\ y e. K ) -> { y } C_ A ) |
54 |
35
|
adantr |
|- ( ( ph /\ y e. K ) -> N C_ C ) |
55 |
|
xpss12 |
|- ( ( { y } C_ A /\ N C_ C ) -> ( { y } X. N ) C_ ( A X. C ) ) |
56 |
53 54 55
|
syl2anc |
|- ( ( ph /\ y e. K ) -> ( { y } X. N ) C_ ( A X. C ) ) |
57 |
51 56
|
fssresd |
|- ( ( ph /\ y e. K ) -> ( F |` ( { y } X. N ) ) : ( { y } X. N ) --> B ) |
58 |
10
|
fvexi |
|- .0. e. _V |
59 |
58
|
a1i |
|- ( ( ph /\ y e. K ) -> .0. e. _V ) |
60 |
57 50 59
|
fdmfifsupp |
|- ( ( ph /\ y e. K ) -> ( F |` ( { y } X. N ) ) finSupp .0. ) |
61 |
1 10 46 50 57 60
|
gsumcl |
|- ( ( ph /\ y e. K ) -> ( G gsum ( F |` ( { y } X. N ) ) ) e. B ) |
62 |
61
|
fmpttd |
|- ( ph -> ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) : K --> B ) |
63 |
|
eqid |
|- ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) = ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) |
64 |
|
ovexd |
|- ( ( ph /\ y e. K ) -> ( G gsum ( F |` ( { y } X. N ) ) ) e. _V ) |
65 |
63 26 64 14
|
fsuppmptdm |
|- ( ph -> ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) finSupp .0. ) |
66 |
1 10 12 25 15 41 62 42 65
|
gsumsub |
|- ( ph -> ( G gsum ( ( H |` K ) oF .- ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) = ( ( G gsum ( H |` K ) ) .- ( G gsum ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) ) |
67 |
|
fvexd |
|- ( ( ph /\ y e. K ) -> ( H ` y ) e. _V ) |
68 |
7 32
|
feqresmpt |
|- ( ph -> ( H |` K ) = ( y e. K |-> ( H ` y ) ) ) |
69 |
|
eqidd |
|- ( ph -> ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) = ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) |
70 |
15 67 64 68 69
|
offval2 |
|- ( ph -> ( ( H |` K ) oF .- ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) = ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) |
71 |
70
|
oveq2d |
|- ( ph -> ( G gsum ( ( H |` K ) oF .- ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) = ( G gsum ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) ) |
72 |
|
cmnmnd |
|- ( G e. CMnd -> G e. Mnd ) |
73 |
46 72
|
syl |
|- ( ( ph /\ y e. K ) -> G e. Mnd ) |
74 |
|
simpr |
|- ( ( ph /\ y e. K ) -> y e. K ) |
75 |
51
|
adantr |
|- ( ( ( ph /\ y e. K ) /\ z e. N ) -> F : ( A X. C ) --> B ) |
76 |
52
|
adantr |
|- ( ( ( ph /\ y e. K ) /\ z e. N ) -> y e. A ) |
77 |
54
|
sselda |
|- ( ( ( ph /\ y e. K ) /\ z e. N ) -> z e. C ) |
78 |
75 76 77
|
fovrnd |
|- ( ( ( ph /\ y e. K ) /\ z e. N ) -> ( y F z ) e. B ) |
79 |
78
|
fmpttd |
|- ( ( ph /\ y e. K ) -> ( z e. N |-> ( y F z ) ) : N --> B ) |
80 |
|
eqid |
|- ( z e. N |-> ( y F z ) ) = ( z e. N |-> ( y F z ) ) |
81 |
|
ovexd |
|- ( ( ( ph /\ y e. K ) /\ z e. N ) -> ( y F z ) e. _V ) |
82 |
80 48 81 59
|
fsuppmptdm |
|- ( ( ph /\ y e. K ) -> ( z e. N |-> ( y F z ) ) finSupp .0. ) |
83 |
1 10 46 48 79 82
|
gsumcl |
|- ( ( ph /\ y e. K ) -> ( G gsum ( z e. N |-> ( y F z ) ) ) e. B ) |
84 |
|
velsn |
|- ( w e. { y } <-> w = y ) |
85 |
|
ovres |
|- ( ( w e. { y } /\ z e. N ) -> ( w ( F |` ( { y } X. N ) ) z ) = ( w F z ) ) |
86 |
84 85
|
sylanbr |
|- ( ( w = y /\ z e. N ) -> ( w ( F |` ( { y } X. N ) ) z ) = ( w F z ) ) |
87 |
|
oveq1 |
|- ( w = y -> ( w F z ) = ( y F z ) ) |
88 |
87
|
adantr |
|- ( ( w = y /\ z e. N ) -> ( w F z ) = ( y F z ) ) |
89 |
86 88
|
eqtrd |
|- ( ( w = y /\ z e. N ) -> ( w ( F |` ( { y } X. N ) ) z ) = ( y F z ) ) |
90 |
89
|
mpteq2dva |
|- ( w = y -> ( z e. N |-> ( w ( F |` ( { y } X. N ) ) z ) ) = ( z e. N |-> ( y F z ) ) ) |
91 |
90
|
oveq2d |
|- ( w = y -> ( G gsum ( z e. N |-> ( w ( F |` ( { y } X. N ) ) z ) ) ) = ( G gsum ( z e. N |-> ( y F z ) ) ) ) |
92 |
1 91
|
gsumsn |
|- ( ( G e. Mnd /\ y e. K /\ ( G gsum ( z e. N |-> ( y F z ) ) ) e. B ) -> ( G gsum ( w e. { y } |-> ( G gsum ( z e. N |-> ( w ( F |` ( { y } X. N ) ) z ) ) ) ) ) = ( G gsum ( z e. N |-> ( y F z ) ) ) ) |
93 |
73 74 83 92
|
syl3anc |
|- ( ( ph /\ y e. K ) -> ( G gsum ( w e. { y } |-> ( G gsum ( z e. N |-> ( w ( F |` ( { y } X. N ) ) z ) ) ) ) ) = ( G gsum ( z e. N |-> ( y F z ) ) ) ) |
94 |
47
|
a1i |
|- ( ( ph /\ y e. K ) -> { y } e. Fin ) |
95 |
1 10 46 94 48 57 60
|
gsumxp |
|- ( ( ph /\ y e. K ) -> ( G gsum ( F |` ( { y } X. N ) ) ) = ( G gsum ( w e. { y } |-> ( G gsum ( z e. N |-> ( w ( F |` ( { y } X. N ) ) z ) ) ) ) ) ) |
96 |
|
ovres |
|- ( ( y e. K /\ z e. N ) -> ( y ( F |` ( K X. N ) ) z ) = ( y F z ) ) |
97 |
96
|
adantll |
|- ( ( ( ph /\ y e. K ) /\ z e. N ) -> ( y ( F |` ( K X. N ) ) z ) = ( y F z ) ) |
98 |
97
|
mpteq2dva |
|- ( ( ph /\ y e. K ) -> ( z e. N |-> ( y ( F |` ( K X. N ) ) z ) ) = ( z e. N |-> ( y F z ) ) ) |
99 |
98
|
oveq2d |
|- ( ( ph /\ y e. K ) -> ( G gsum ( z e. N |-> ( y ( F |` ( K X. N ) ) z ) ) ) = ( G gsum ( z e. N |-> ( y F z ) ) ) ) |
100 |
93 95 99
|
3eqtr4d |
|- ( ( ph /\ y e. K ) -> ( G gsum ( F |` ( { y } X. N ) ) ) = ( G gsum ( z e. N |-> ( y ( F |` ( K X. N ) ) z ) ) ) ) |
101 |
100
|
mpteq2dva |
|- ( ph -> ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) = ( y e. K |-> ( G gsum ( z e. N |-> ( y ( F |` ( K X. N ) ) z ) ) ) ) ) |
102 |
101
|
oveq2d |
|- ( ph -> ( G gsum ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) = ( G gsum ( y e. K |-> ( G gsum ( z e. N |-> ( y ( F |` ( K X. N ) ) z ) ) ) ) ) ) |
103 |
1 10 2 26 27 38 39
|
gsumxp |
|- ( ph -> ( G gsum ( F |` ( K X. N ) ) ) = ( G gsum ( y e. K |-> ( G gsum ( z e. N |-> ( y ( F |` ( K X. N ) ) z ) ) ) ) ) ) |
104 |
102 103
|
eqtr4d |
|- ( ph -> ( G gsum ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) = ( G gsum ( F |` ( K X. N ) ) ) ) |
105 |
104
|
oveq2d |
|- ( ph -> ( ( G gsum ( H |` K ) ) .- ( G gsum ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) = ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) |
106 |
66 71 105
|
3eqtr3d |
|- ( ph -> ( G gsum ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) = ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) |
107 |
|
oveq2 |
|- ( g = ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) -> ( G gsum g ) = ( G gsum ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) ) |
108 |
107
|
eleq1d |
|- ( g = ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) -> ( ( G gsum g ) e. T <-> ( G gsum ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) e. T ) ) |
109 |
|
fveq2 |
|- ( x = y -> ( H ` x ) = ( H ` y ) ) |
110 |
|
sneq |
|- ( x = y -> { x } = { y } ) |
111 |
110
|
xpeq1d |
|- ( x = y -> ( { x } X. N ) = ( { y } X. N ) ) |
112 |
111
|
reseq2d |
|- ( x = y -> ( F |` ( { x } X. N ) ) = ( F |` ( { y } X. N ) ) ) |
113 |
112
|
oveq2d |
|- ( x = y -> ( G gsum ( F |` ( { x } X. N ) ) ) = ( G gsum ( F |` ( { y } X. N ) ) ) ) |
114 |
109 113
|
oveq12d |
|- ( x = y -> ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. N ) ) ) ) = ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) |
115 |
114
|
eleq1d |
|- ( x = y -> ( ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. N ) ) ) ) e. L <-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) e. L ) ) |
116 |
115
|
rspccva |
|- ( ( A. x e. K ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. N ) ) ) ) e. L /\ y e. K ) -> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) e. L ) |
117 |
19 116
|
sylan |
|- ( ( ph /\ y e. K ) -> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) e. L ) |
118 |
117
|
fmpttd |
|- ( ph -> ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) : K --> L ) |
119 |
13 15
|
elmapd |
|- ( ph -> ( ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) e. ( L ^m K ) <-> ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) : K --> L ) ) |
120 |
118 119
|
mpbird |
|- ( ph -> ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) e. ( L ^m K ) ) |
121 |
108 21 120
|
rspcdva |
|- ( ph -> ( G gsum ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) e. T ) |
122 |
106 121
|
eqeltrrd |
|- ( ph -> ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) e. T ) |
123 |
|
oveq1 |
|- ( c = ( G gsum ( F |` ( K X. N ) ) ) -> ( c .+ d ) = ( ( G gsum ( F |` ( K X. N ) ) ) .+ d ) ) |
124 |
123
|
eleq1d |
|- ( c = ( G gsum ( F |` ( K X. N ) ) ) -> ( ( c .+ d ) e. U <-> ( ( G gsum ( F |` ( K X. N ) ) ) .+ d ) e. U ) ) |
125 |
|
oveq2 |
|- ( d = ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) -> ( ( G gsum ( F |` ( K X. N ) ) ) .+ d ) = ( ( G gsum ( F |` ( K X. N ) ) ) .+ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) ) |
126 |
125
|
eleq1d |
|- ( d = ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) -> ( ( ( G gsum ( F |` ( K X. N ) ) ) .+ d ) e. U <-> ( ( G gsum ( F |` ( K X. N ) ) ) .+ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) e. U ) ) |
127 |
124 126
|
rspc2va |
|- ( ( ( ( G gsum ( F |` ( K X. N ) ) ) e. S /\ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) e. T ) /\ A. c e. S A. d e. T ( c .+ d ) e. U ) -> ( ( G gsum ( F |` ( K X. N ) ) ) .+ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) e. U ) |
128 |
20 122 16 127
|
syl21anc |
|- ( ph -> ( ( G gsum ( F |` ( K X. N ) ) ) .+ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) e. U ) |
129 |
45 128
|
eqeltrrd |
|- ( ph -> ( G gsum ( H |` K ) ) e. U ) |