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
tsmssplit.1 ⊢ φ → G ∈ CMnd
tsmssplit.2 ⊢ φ → G ∈ TopMnd
tsmssplit.a ⊢ φ → A ∈ V
tsmssplit.f ⊢ φ → F : A ⟶ B
tsmssplit.x ⊢ φ → X ∈ G tsums F ↾ C
tsmssplit.y ⊢ φ → Y ∈ G tsums F ↾ D
tsmssplit.i ⊢ φ → C ∩ D = ∅
tsmssplit.u ⊢ φ → A = C ∪ D
Assertion tsmssplit ⊢ φ → X + ˙ Y ∈ G tsums F

Proof

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