Metamath Proof Explorer

Theorem tsmssplit

Description: Split a topological group sum into two parts. (Contributed by Mario Carneiro, 19-Sep-2015) (Proof shortened by AV, 24-Jul-2019)

Ref Expression
Hypotheses tsmssplit.b 
|- B = ( Base ` G )
tsmssplit.p 
|- .+ = ( +g ` G )
tsmssplit.1 
|- ( ph -> G e. CMnd )
tsmssplit.2 
|- ( ph -> G e. TopMnd )
tsmssplit.a 
|- ( ph -> A e. V )
tsmssplit.f 
|- ( ph -> F : A --> B )
tsmssplit.x 
|- ( ph -> X e. ( G tsums ( F |` C ) ) )
tsmssplit.y 
|- ( ph -> Y e. ( G tsums ( F |` D ) ) )
tsmssplit.i 
|- ( ph -> ( C i^i D ) = (/) )
tsmssplit.u 
|- ( ph -> A = ( C u. D ) )
Assertion tsmssplit 
|- ( ph -> ( X .+ Y ) e. ( G tsums F ) )

Proof

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 ) )