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