Step |
Hyp |
Ref |
Expression |
1 |
|
tsmssplit.b |
|- B = ( Base ` G ) |
2 |
|
tsmssplit.p |
|- .+ = ( +g ` G ) |
3 |
|
tsmssplit.1 |
|- ( ph -> G e. CMnd ) |
4 |
|
tsmssplit.2 |
|- ( ph -> G e. TopMnd ) |
5 |
|
tsmssplit.a |
|- ( ph -> A e. V ) |
6 |
|
tsmssplit.f |
|- ( ph -> F : A --> B ) |
7 |
|
tsmssplit.x |
|- ( ph -> X e. ( G tsums ( F |` C ) ) ) |
8 |
|
tsmssplit.y |
|- ( ph -> Y e. ( G tsums ( F |` D ) ) ) |
9 |
|
tsmssplit.i |
|- ( ph -> ( C i^i D ) = (/) ) |
10 |
|
tsmssplit.u |
|- ( ph -> A = ( C u. D ) ) |
11 |
6
|
ffvelrnda |
|- ( ( ph /\ k e. A ) -> ( F ` k ) e. B ) |
12 |
|
cmnmnd |
|- ( G e. CMnd -> G e. Mnd ) |
13 |
3 12
|
syl |
|- ( ph -> G e. Mnd ) |
14 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
15 |
1 14
|
mndidcl |
|- ( G e. Mnd -> ( 0g ` G ) e. B ) |
16 |
13 15
|
syl |
|- ( ph -> ( 0g ` G ) e. B ) |
17 |
16
|
adantr |
|- ( ( ph /\ k e. A ) -> ( 0g ` G ) e. B ) |
18 |
11 17
|
ifcld |
|- ( ( ph /\ k e. A ) -> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) e. B ) |
19 |
18
|
fmpttd |
|- ( ph -> ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) : A --> B ) |
20 |
11 17
|
ifcld |
|- ( ( ph /\ k e. A ) -> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) e. B ) |
21 |
20
|
fmpttd |
|- ( ph -> ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) : A --> B ) |
22 |
6
|
feqmptd |
|- ( ph -> F = ( k e. A |-> ( F ` k ) ) ) |
23 |
22
|
reseq1d |
|- ( ph -> ( F |` C ) = ( ( k e. A |-> ( F ` k ) ) |` C ) ) |
24 |
|
ssun1 |
|- C C_ ( C u. D ) |
25 |
24 10
|
sseqtrrid |
|- ( ph -> C C_ A ) |
26 |
|
iftrue |
|- ( k e. C -> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) = ( F ` k ) ) |
27 |
26
|
mpteq2ia |
|- ( k e. C |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) = ( k e. C |-> ( F ` k ) ) |
28 |
|
resmpt |
|- ( C C_ A -> ( ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) |` C ) = ( k e. C |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) ) |
29 |
|
resmpt |
|- ( C C_ A -> ( ( k e. A |-> ( F ` k ) ) |` C ) = ( k e. C |-> ( F ` k ) ) ) |
30 |
27 28 29
|
3eqtr4a |
|- ( C C_ A -> ( ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) |` C ) = ( ( k e. A |-> ( F ` k ) ) |` C ) ) |
31 |
25 30
|
syl |
|- ( ph -> ( ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) |` C ) = ( ( k e. A |-> ( F ` k ) ) |` C ) ) |
32 |
23 31
|
eqtr4d |
|- ( ph -> ( F |` C ) = ( ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) |` C ) ) |
33 |
32
|
oveq2d |
|- ( ph -> ( G tsums ( F |` C ) ) = ( G tsums ( ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) |` C ) ) ) |
34 |
|
tmdtps |
|- ( G e. TopMnd -> G e. TopSp ) |
35 |
4 34
|
syl |
|- ( ph -> G e. TopSp ) |
36 |
|
eldifn |
|- ( k e. ( A \ C ) -> -. k e. C ) |
37 |
36
|
adantl |
|- ( ( ph /\ k e. ( A \ C ) ) -> -. k e. C ) |
38 |
37
|
iffalsed |
|- ( ( ph /\ k e. ( A \ C ) ) -> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) = ( 0g ` G ) ) |
39 |
38 5
|
suppss2 |
|- ( ph -> ( ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) supp ( 0g ` G ) ) C_ C ) |
40 |
1 14 3 35 5 19 39
|
tsmsres |
|- ( ph -> ( G tsums ( ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) |` C ) ) = ( G tsums ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) ) ) |
41 |
33 40
|
eqtrd |
|- ( ph -> ( G tsums ( F |` C ) ) = ( G tsums ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) ) ) |
42 |
7 41
|
eleqtrd |
|- ( ph -> X e. ( G tsums ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) ) ) |
43 |
22
|
reseq1d |
|- ( ph -> ( F |` D ) = ( ( k e. A |-> ( F ` k ) ) |` D ) ) |
44 |
|
ssun2 |
|- D C_ ( C u. D ) |
45 |
44 10
|
sseqtrrid |
|- ( ph -> D C_ A ) |
46 |
|
iftrue |
|- ( k e. D -> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) = ( F ` k ) ) |
47 |
46
|
mpteq2ia |
|- ( k e. D |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) = ( k e. D |-> ( F ` k ) ) |
48 |
|
resmpt |
|- ( D C_ A -> ( ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) |` D ) = ( k e. D |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) ) |
49 |
|
resmpt |
|- ( D C_ A -> ( ( k e. A |-> ( F ` k ) ) |` D ) = ( k e. D |-> ( F ` k ) ) ) |
50 |
47 48 49
|
3eqtr4a |
|- ( D C_ A -> ( ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) |` D ) = ( ( k e. A |-> ( F ` k ) ) |` D ) ) |
51 |
45 50
|
syl |
|- ( ph -> ( ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) |` D ) = ( ( k e. A |-> ( F ` k ) ) |` D ) ) |
52 |
43 51
|
eqtr4d |
|- ( ph -> ( F |` D ) = ( ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) |` D ) ) |
53 |
52
|
oveq2d |
|- ( ph -> ( G tsums ( F |` D ) ) = ( G tsums ( ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) |` D ) ) ) |
54 |
|
eldifn |
|- ( k e. ( A \ D ) -> -. k e. D ) |
55 |
54
|
adantl |
|- ( ( ph /\ k e. ( A \ D ) ) -> -. k e. D ) |
56 |
55
|
iffalsed |
|- ( ( ph /\ k e. ( A \ D ) ) -> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) = ( 0g ` G ) ) |
57 |
56 5
|
suppss2 |
|- ( ph -> ( ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) supp ( 0g ` G ) ) C_ D ) |
58 |
1 14 3 35 5 21 57
|
tsmsres |
|- ( ph -> ( G tsums ( ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) |` D ) ) = ( G tsums ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) ) ) |
59 |
53 58
|
eqtrd |
|- ( ph -> ( G tsums ( F |` D ) ) = ( G tsums ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) ) ) |
60 |
8 59
|
eleqtrd |
|- ( ph -> Y e. ( G tsums ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) ) ) |
61 |
1 2 3 4 5 19 21 42 60
|
tsmsadd |
|- ( ph -> ( X .+ Y ) e. ( G tsums ( ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) oF .+ ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) ) ) ) |
62 |
26
|
adantl |
|- ( ( ( ph /\ k e. A ) /\ k e. C ) -> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) = ( F ` k ) ) |
63 |
|
noel |
|- -. k e. (/) |
64 |
|
eleq2 |
|- ( ( C i^i D ) = (/) -> ( k e. ( C i^i D ) <-> k e. (/) ) ) |
65 |
63 64
|
mtbiri |
|- ( ( C i^i D ) = (/) -> -. k e. ( C i^i D ) ) |
66 |
9 65
|
syl |
|- ( ph -> -. k e. ( C i^i D ) ) |
67 |
66
|
adantr |
|- ( ( ph /\ k e. A ) -> -. k e. ( C i^i D ) ) |
68 |
|
elin |
|- ( k e. ( C i^i D ) <-> ( k e. C /\ k e. D ) ) |
69 |
67 68
|
sylnib |
|- ( ( ph /\ k e. A ) -> -. ( k e. C /\ k e. D ) ) |
70 |
|
imnan |
|- ( ( k e. C -> -. k e. D ) <-> -. ( k e. C /\ k e. D ) ) |
71 |
69 70
|
sylibr |
|- ( ( ph /\ k e. A ) -> ( k e. C -> -. k e. D ) ) |
72 |
71
|
imp |
|- ( ( ( ph /\ k e. A ) /\ k e. C ) -> -. k e. D ) |
73 |
72
|
iffalsed |
|- ( ( ( ph /\ k e. A ) /\ k e. C ) -> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) = ( 0g ` G ) ) |
74 |
62 73
|
oveq12d |
|- ( ( ( ph /\ k e. A ) /\ k e. C ) -> ( if ( k e. C , ( F ` k ) , ( 0g ` G ) ) .+ if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) = ( ( F ` k ) .+ ( 0g ` G ) ) ) |
75 |
1 2 14
|
mndrid |
|- ( ( G e. Mnd /\ ( F ` k ) e. B ) -> ( ( F ` k ) .+ ( 0g ` G ) ) = ( F ` k ) ) |
76 |
13 11 75
|
syl2an2r |
|- ( ( ph /\ k e. A ) -> ( ( F ` k ) .+ ( 0g ` G ) ) = ( F ` k ) ) |
77 |
76
|
adantr |
|- ( ( ( ph /\ k e. A ) /\ k e. C ) -> ( ( F ` k ) .+ ( 0g ` G ) ) = ( F ` k ) ) |
78 |
74 77
|
eqtrd |
|- ( ( ( ph /\ k e. A ) /\ k e. C ) -> ( if ( k e. C , ( F ` k ) , ( 0g ` G ) ) .+ if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) = ( F ` k ) ) |
79 |
71
|
con2d |
|- ( ( ph /\ k e. A ) -> ( k e. D -> -. k e. C ) ) |
80 |
79
|
imp |
|- ( ( ( ph /\ k e. A ) /\ k e. D ) -> -. k e. C ) |
81 |
80
|
iffalsed |
|- ( ( ( ph /\ k e. A ) /\ k e. D ) -> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) = ( 0g ` G ) ) |
82 |
46
|
adantl |
|- ( ( ( ph /\ k e. A ) /\ k e. D ) -> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) = ( F ` k ) ) |
83 |
81 82
|
oveq12d |
|- ( ( ( ph /\ k e. A ) /\ k e. D ) -> ( if ( k e. C , ( F ` k ) , ( 0g ` G ) ) .+ if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) = ( ( 0g ` G ) .+ ( F ` k ) ) ) |
84 |
1 2 14
|
mndlid |
|- ( ( G e. Mnd /\ ( F ` k ) e. B ) -> ( ( 0g ` G ) .+ ( F ` k ) ) = ( F ` k ) ) |
85 |
13 11 84
|
syl2an2r |
|- ( ( ph /\ k e. A ) -> ( ( 0g ` G ) .+ ( F ` k ) ) = ( F ` k ) ) |
86 |
85
|
adantr |
|- ( ( ( ph /\ k e. A ) /\ k e. D ) -> ( ( 0g ` G ) .+ ( F ` k ) ) = ( F ` k ) ) |
87 |
83 86
|
eqtrd |
|- ( ( ( ph /\ k e. A ) /\ k e. D ) -> ( if ( k e. C , ( F ` k ) , ( 0g ` G ) ) .+ if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) = ( F ` k ) ) |
88 |
10
|
eleq2d |
|- ( ph -> ( k e. A <-> k e. ( C u. D ) ) ) |
89 |
|
elun |
|- ( k e. ( C u. D ) <-> ( k e. C \/ k e. D ) ) |
90 |
88 89
|
bitrdi |
|- ( ph -> ( k e. A <-> ( k e. C \/ k e. D ) ) ) |
91 |
90
|
biimpa |
|- ( ( ph /\ k e. A ) -> ( k e. C \/ k e. D ) ) |
92 |
78 87 91
|
mpjaodan |
|- ( ( ph /\ k e. A ) -> ( if ( k e. C , ( F ` k ) , ( 0g ` G ) ) .+ if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) = ( F ` k ) ) |
93 |
92
|
mpteq2dva |
|- ( ph -> ( k e. A |-> ( if ( k e. C , ( F ` k ) , ( 0g ` G ) ) .+ if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) ) = ( k e. A |-> ( F ` k ) ) ) |
94 |
22 93
|
eqtr4d |
|- ( ph -> F = ( k e. A |-> ( if ( k e. C , ( F ` k ) , ( 0g ` G ) ) .+ if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) ) ) |
95 |
|
eqidd |
|- ( ph -> ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) = ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) ) |
96 |
|
eqidd |
|- ( ph -> ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) = ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) ) |
97 |
5 18 20 95 96
|
offval2 |
|- ( ph -> ( ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) oF .+ ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) ) = ( k e. A |-> ( if ( k e. C , ( F ` k ) , ( 0g ` G ) ) .+ if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) ) ) |
98 |
94 97
|
eqtr4d |
|- ( ph -> F = ( ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) oF .+ ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) ) ) |
99 |
98
|
oveq2d |
|- ( ph -> ( G tsums F ) = ( G tsums ( ( k e. A |-> if ( k e. C , ( F ` k ) , ( 0g ` G ) ) ) oF .+ ( k e. A |-> if ( k e. D , ( F ` k ) , ( 0g ` G ) ) ) ) ) ) |
100 |
61 99
|
eleqtrrd |
|- ( ph -> ( X .+ Y ) e. ( G tsums F ) ) |