Metamath Proof Explorer

Theorem tsmsadd

Description: The sum of two infinite group sums. (Contributed by Mario Carneiro, 19-Sep-2015) (Proof shortened by AV, 24-Jul-2019)

Ref Expression
Hypotheses tsmsadd.b ⊢ B = Base G
tsmsadd.p ⊢ + ˙ = + G
tsmsadd.1 ⊢ φ → G ∈ CMnd
tsmsadd.2 ⊢ φ → G ∈ TopMnd
tsmsadd.a ⊢ φ → A ∈ V
tsmsadd.f ⊢ φ → F : A ⟶ B
tsmsadd.h ⊢ φ → H : A ⟶ B
tsmsadd.x ⊢ φ → X ∈ G tsums F
tsmsadd.y ⊢ φ → Y ∈ G tsums H
Assertion tsmsadd ⊢ φ → X + ˙ Y ∈ G tsums F + ˙ f H

Proof

Step Hyp Ref Expression
1 tsmsadd.b ⊢ B = Base G
2 tsmsadd.p ⊢ + ˙ = + G
3 tsmsadd.1 ⊢ φ → G ∈ CMnd
4 tsmsadd.2 ⊢ φ → G ∈ TopMnd
5 tsmsadd.a ⊢ φ → A ∈ V
6 tsmsadd.f ⊢ φ → F : A ⟶ B
7 tsmsadd.h ⊢ φ → H : A ⟶ B
8 tsmsadd.x ⊢ φ → X ∈ G tsums F
9 tsmsadd.y ⊢ φ → Y ∈ G tsums H
10 tmdtps ⊢ G ∈ TopMnd → G ∈ TopSp
11 4 10 syl ⊢ φ → G ∈ TopSp
12 1 3 11 5 6 tsmscl ⊢ φ → G tsums F ⊆ B
13 12 8 sseldd ⊢ φ → X ∈ B
14 1 3 11 5 7 tsmscl ⊢ φ → G tsums H ⊆ B
15 14 9 sseldd ⊢ φ → Y ∈ B
16 eqid ⊢ + 𝑓 ⁡ G = + 𝑓 ⁡ G
17 1 2 16 plusfval ⊢ X ∈ B ∧ Y ∈ B → X + 𝑓 ⁡ G Y = X + ˙ Y
18 13 15 17 syl2anc ⊢ φ → X + 𝑓 ⁡ G Y = X + ˙ Y
19 eqid ⊢ TopOpen ⁡ G = TopOpen ⁡ G
20 1 19 istps ⊢ G ∈ TopSp ↔ TopOpen ⁡ G ∈ TopOn ⁡ B
21 11 20 sylib ⊢ φ → TopOpen ⁡ G ∈ TopOn ⁡ B
22 eqid ⊢ 𝒫 A ∩ Fin = 𝒫 A ∩ Fin
23 eqid ⊢ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z = y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z
24 eqid ⊢ ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z = ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z
25 22 23 24 5 tsmsfbas ⊢ φ → ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ∈ fBas ⁡ 𝒫 A ∩ Fin
26 fgcl ⊢ ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ∈ fBas ⁡ 𝒫 A ∩ Fin → 𝒫 A ∩ Fin filGen ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ∈ Fil ⁡ 𝒫 A ∩ Fin
27 25 26 syl ⊢ φ → 𝒫 A ∩ Fin filGen ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ∈ Fil ⁡ 𝒫 A ∩ Fin
28 1 22 3 5 6 tsmslem1 ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → ∑ G F ↾ z ∈ B
29 1 22 3 5 7 tsmslem1 ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → ∑ G H ↾ z ∈ B
30 1 19 22 24 3 5 6 tsmsval ⊢ φ → G tsums F = TopOpen ⁡ G fLimf 𝒫 A ∩ Fin filGen ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ⁡ z ∈ 𝒫 A ∩ Fin ⟼ ∑ G F ↾ z
31 8 30 eleqtrd ⊢ φ → X ∈ TopOpen ⁡ G fLimf 𝒫 A ∩ Fin filGen ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ⁡ z ∈ 𝒫 A ∩ Fin ⟼ ∑ G F ↾ z
32 1 19 22 24 3 5 7 tsmsval ⊢ φ → G tsums H = TopOpen ⁡ G fLimf 𝒫 A ∩ Fin filGen ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ⁡ z ∈ 𝒫 A ∩ Fin ⟼ ∑ G H ↾ z
33 9 32 eleqtrd ⊢ φ → Y ∈ TopOpen ⁡ G fLimf 𝒫 A ∩ Fin filGen ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ⁡ z ∈ 𝒫 A ∩ Fin ⟼ ∑ G H ↾ z
34 19 16 tmdcn ⊢ G ∈ TopMnd → + 𝑓 ⁡ G ∈ TopOpen ⁡ G × t TopOpen ⁡ G Cn TopOpen ⁡ G
35 4 34 syl ⊢ φ → + 𝑓 ⁡ G ∈ TopOpen ⁡ G × t TopOpen ⁡ G Cn TopOpen ⁡ G
36 13 15 opelxpd ⊢ φ → X Y ∈ B × B
37 txtopon ⊢ TopOpen ⁡ G ∈ TopOn ⁡ B ∧ TopOpen ⁡ G ∈ TopOn ⁡ B → TopOpen ⁡ G × t TopOpen ⁡ G ∈ TopOn ⁡ B × B
38 21 21 37 syl2anc ⊢ φ → TopOpen ⁡ G × t TopOpen ⁡ G ∈ TopOn ⁡ B × B
39 toponuni ⊢ TopOpen ⁡ G × t TopOpen ⁡ G ∈ TopOn ⁡ B × B → B × B = ⋃ TopOpen ⁡ G × t TopOpen ⁡ G
40 38 39 syl ⊢ φ → B × B = ⋃ TopOpen ⁡ G × t TopOpen ⁡ G
41 36 40 eleqtrd ⊢ φ → X Y ∈ ⋃ TopOpen ⁡ G × t TopOpen ⁡ G
42 eqid ⊢ ⋃ TopOpen ⁡ G × t TopOpen ⁡ G = ⋃ TopOpen ⁡ G × t TopOpen ⁡ G
43 42 cncnpi ⊢ + 𝑓 ⁡ G ∈ TopOpen ⁡ G × t TopOpen ⁡ G Cn TopOpen ⁡ G ∧ X Y ∈ ⋃ TopOpen ⁡ G × t TopOpen ⁡ G → + 𝑓 ⁡ G ∈ TopOpen ⁡ G × t TopOpen ⁡ G CnP TopOpen ⁡ G ⁡ X Y
44 35 41 43 syl2anc ⊢ φ → + 𝑓 ⁡ G ∈ TopOpen ⁡ G × t TopOpen ⁡ G CnP TopOpen ⁡ G ⁡ X Y
45 21 21 27 28 29 31 33 44 flfcnp2 ⊢ φ → X + 𝑓 ⁡ G Y ∈ TopOpen ⁡ G fLimf 𝒫 A ∩ Fin filGen ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ⁡ z ∈ 𝒫 A ∩ Fin ⟼ ∑ G F ↾ z + 𝑓 ⁡ G ∑ G H ↾ z
46 18 45 eqeltrrd ⊢ φ → X + ˙ Y ∈ TopOpen ⁡ G fLimf 𝒫 A ∩ Fin filGen ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ⁡ z ∈ 𝒫 A ∩ Fin ⟼ ∑ G F ↾ z + 𝑓 ⁡ G ∑ G H ↾ z
47 cmnmnd ⊢ G ∈ CMnd → G ∈ Mnd
48 3 47 syl ⊢ φ → G ∈ Mnd
49 1 2 mndcl ⊢ G ∈ Mnd ∧ x ∈ B ∧ y ∈ B → x + ˙ y ∈ B
50 49 3expb ⊢ G ∈ Mnd ∧ x ∈ B ∧ y ∈ B → x + ˙ y ∈ B
51 48 50 sylan ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + ˙ y ∈ B
52 inidm ⊢ A ∩ A = A
53 51 6 7 5 5 52 off ⊢ φ → F + ˙ f H : A ⟶ B
54 1 19 22 24 3 5 53 tsmsval ⊢ φ → G tsums F + ˙ f H = TopOpen ⁡ G fLimf 𝒫 A ∩ Fin filGen ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ⁡ z ∈ 𝒫 A ∩ Fin ⟼ ∑ G F + ˙ f H ↾ z
55 eqid ⊢ 0 G = 0 G
56 3 adantr ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → G ∈ CMnd
57 elinel2 ⊢ z ∈ 𝒫 A ∩ Fin → z ∈ Fin
58 57 adantl ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → z ∈ Fin
59 elfpw ⊢ z ∈ 𝒫 A ∩ Fin ↔ z ⊆ A ∧ z ∈ Fin
60 59 simplbi ⊢ z ∈ 𝒫 A ∩ Fin → z ⊆ A
61 fssres ⊢ F : A ⟶ B ∧ z ⊆ A → F ↾ z : z ⟶ B
62 6 60 61 syl2an ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → F ↾ z : z ⟶ B
63 fssres ⊢ H : A ⟶ B ∧ z ⊆ A → H ↾ z : z ⟶ B
64 7 60 63 syl2an ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → H ↾ z : z ⟶ B
65 fvexd ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → 0 G ∈ V
66 62 58 65 fdmfifsupp ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → finSupp 0 G⁡ F ↾ z
67 64 58 65 fdmfifsupp ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → finSupp 0 G⁡ H ↾ z
68 1 55 2 56 58 62 64 66 67 gsumadd ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → ∑ G F ↾ z + ˙ f H ↾ z = ∑ G F ↾ z + ˙ ∑ G H ↾ z
69 1 fvexi ⊢ B ∈ V
70 69 a1i ⊢ φ → B ∈ V
71 fex2 ⊢ F : A ⟶ B ∧ A ∈ V ∧ B ∈ V → F ∈ V
72 6 5 70 71 syl3anc ⊢ φ → F ∈ V
73 fex2 ⊢ H : A ⟶ B ∧ A ∈ V ∧ B ∈ V → H ∈ V
74 7 5 70 73 syl3anc ⊢ φ → H ∈ V
75 offres ⊢ F ∈ V ∧ H ∈ V → F + ˙ f H ↾ z = F ↾ z + ˙ f H ↾ z
76 72 74 75 syl2anc ⊢ φ → F + ˙ f H ↾ z = F ↾ z + ˙ f H ↾ z
77 76 adantr ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → F + ˙ f H ↾ z = F ↾ z + ˙ f H ↾ z
78 77 oveq2d ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → ∑ G F + ˙ f H ↾ z = ∑ G F ↾ z + ˙ f H ↾ z
79 1 2 16 plusfval ⊢ ∑ G F ↾ z ∈ B ∧ ∑ G H ↾ z ∈ B → ∑ G F ↾ z + 𝑓 ⁡ G ∑ G H ↾ z = ∑ G F ↾ z + ˙ ∑ G H ↾ z
80 28 29 79 syl2anc ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → ∑ G F ↾ z + 𝑓 ⁡ G ∑ G H ↾ z = ∑ G F ↾ z + ˙ ∑ G H ↾ z
81 68 78 80 3eqtr4d ⊢ φ ∧ z ∈ 𝒫 A ∩ Fin → ∑ G F + ˙ f H ↾ z = ∑ G F ↾ z + 𝑓 ⁡ G ∑ G H ↾ z
82 81 mpteq2dva ⊢ φ → z ∈ 𝒫 A ∩ Fin ⟼ ∑ G F + ˙ f H ↾ z = z ∈ 𝒫 A ∩ Fin ⟼ ∑ G F ↾ z + 𝑓 ⁡ G ∑ G H ↾ z
83 82 fveq2d ⊢ φ → TopOpen ⁡ G fLimf 𝒫 A ∩ Fin filGen ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ⁡ z ∈ 𝒫 A ∩ Fin ⟼ ∑ G F + ˙ f H ↾ z = TopOpen ⁡ G fLimf 𝒫 A ∩ Fin filGen ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ⁡ z ∈ 𝒫 A ∩ Fin ⟼ ∑ G F ↾ z + 𝑓 ⁡ G ∑ G H ↾ z
84 54 83 eqtrd ⊢ φ → G tsums F + ˙ f H = TopOpen ⁡ G fLimf 𝒫 A ∩ Fin filGen ran ⁡ y ∈ 𝒫 A ∩ Fin ⟼ z ∈ 𝒫 A ∩ Fin | y ⊆ z ⁡ z ∈ 𝒫 A ∩ Fin ⟼ ∑ G F ↾ z + 𝑓 ⁡ G ∑ G H ↾ z
85 46 84 eleqtrrd ⊢ φ → X + ˙ Y ∈ G tsums F + ˙ f H