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 𝐵 = ( Base ‘ 𝐺 )
tsmsadd.p + = ( +g𝐺 )
tsmsadd.1 ( 𝜑𝐺 ∈ CMnd )
tsmsadd.2 ( 𝜑𝐺 ∈ TopMnd )
tsmsadd.a ( 𝜑𝐴𝑉 )
tsmsadd.f ( 𝜑𝐹 : 𝐴𝐵 )
tsmsadd.h ( 𝜑𝐻 : 𝐴𝐵 )
tsmsadd.x ( 𝜑𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
tsmsadd.y ( 𝜑𝑌 ∈ ( 𝐺 tsums 𝐻 ) )
Assertion tsmsadd ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝐺 tsums ( 𝐹f + 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 tsmsadd.b 𝐵 = ( Base ‘ 𝐺 )
2 tsmsadd.p + = ( +g𝐺 )
3 tsmsadd.1 ( 𝜑𝐺 ∈ CMnd )
4 tsmsadd.2 ( 𝜑𝐺 ∈ TopMnd )
5 tsmsadd.a ( 𝜑𝐴𝑉 )
6 tsmsadd.f ( 𝜑𝐹 : 𝐴𝐵 )
7 tsmsadd.h ( 𝜑𝐻 : 𝐴𝐵 )
8 tsmsadd.x ( 𝜑𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
9 tsmsadd.y ( 𝜑𝑌 ∈ ( 𝐺 tsums 𝐻 ) )
10 tmdtps ( 𝐺 ∈ TopMnd → 𝐺 ∈ TopSp )
11 4 10 syl ( 𝜑𝐺 ∈ TopSp )
12 1 3 11 5 6 tsmscl ( 𝜑 → ( 𝐺 tsums 𝐹 ) ⊆ 𝐵 )
13 12 8 sseldd ( 𝜑𝑋𝐵 )
14 1 3 11 5 7 tsmscl ( 𝜑 → ( 𝐺 tsums 𝐻 ) ⊆ 𝐵 )
15 14 9 sseldd ( 𝜑𝑌𝐵 )
16 eqid ( +𝑓𝐺 ) = ( +𝑓𝐺 )
17 1 2 16 plusfval ( ( 𝑋𝐵𝑌𝐵 ) → ( 𝑋 ( +𝑓𝐺 ) 𝑌 ) = ( 𝑋 + 𝑌 ) )
18 13 15 17 syl2anc ( 𝜑 → ( 𝑋 ( +𝑓𝐺 ) 𝑌 ) = ( 𝑋 + 𝑌 ) )
19 eqid ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
20 1 19 istps ( 𝐺 ∈ TopSp ↔ ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) )
21 11 20 sylib ( 𝜑 → ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) )
22 eqid ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin )
23 eqid ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) = ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } )
24 eqid ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) = ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } )
25 22 23 24 5 tsmsfbas ( 𝜑 → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ∈ ( fBas ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
26 fgcl ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ∈ ( fBas ‘ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
27 25 26 syl ( 𝜑 → ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
28 1 22 3 5 6 tsmslem1 ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹𝑧 ) ) ∈ 𝐵 )
29 1 22 3 5 7 tsmslem1 ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐻𝑧 ) ) ∈ 𝐵 )
30 1 19 22 24 3 5 6 tsmsval ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) ) )
31 8 30 eleqtrd ( 𝜑𝑋 ∈ ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) ) )
32 1 19 22 24 3 5 7 tsmsval ( 𝜑 → ( 𝐺 tsums 𝐻 ) = ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐻𝑧 ) ) ) ) )
33 9 32 eleqtrd ( 𝜑𝑌 ∈ ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐻𝑧 ) ) ) ) )
34 19 16 tmdcn ( 𝐺 ∈ TopMnd → ( +𝑓𝐺 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) )
35 4 34 syl ( 𝜑 → ( +𝑓𝐺 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) )
36 13 15 opelxpd ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐵 × 𝐵 ) )
37 txtopon ( ( ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) ∧ ( TopOpen ‘ 𝐺 ) ∈ ( TopOn ‘ 𝐵 ) ) → ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) ∈ ( TopOn ‘ ( 𝐵 × 𝐵 ) ) )
38 21 21 37 syl2anc ( 𝜑 → ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) ∈ ( TopOn ‘ ( 𝐵 × 𝐵 ) ) )
39 toponuni ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) ∈ ( TopOn ‘ ( 𝐵 × 𝐵 ) ) → ( 𝐵 × 𝐵 ) = ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) )
40 38 39 syl ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) )
41 36 40 eleqtrd ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) )
42 eqid ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) = ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) )
43 42 cncnpi ( ( ( +𝑓𝐺 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) Cn ( TopOpen ‘ 𝐺 ) ) ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) ) → ( +𝑓𝐺 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) CnP ( TopOpen ‘ 𝐺 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
44 35 41 43 syl2anc ( 𝜑 → ( +𝑓𝐺 ) ∈ ( ( ( ( TopOpen ‘ 𝐺 ) ×t ( TopOpen ‘ 𝐺 ) ) CnP ( TopOpen ‘ 𝐺 ) ) ‘ ⟨ 𝑋 , 𝑌 ⟩ ) )
45 21 21 27 28 29 31 33 44 flfcnp2 ( 𝜑 → ( 𝑋 ( +𝑓𝐺 ) 𝑌 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( 𝐺 Σg ( 𝐹𝑧 ) ) ( +𝑓𝐺 ) ( 𝐺 Σg ( 𝐻𝑧 ) ) ) ) ) )
46 18 45 eqeltrrd ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( 𝐺 Σg ( 𝐹𝑧 ) ) ( +𝑓𝐺 ) ( 𝐺 Σg ( 𝐻𝑧 ) ) ) ) ) )
47 cmnmnd ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
48 3 47 syl ( 𝜑𝐺 ∈ Mnd )
49 1 2 mndcl ( ( 𝐺 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
50 49 3expb ( ( 𝐺 ∈ Mnd ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
51 48 50 sylan ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
52 inidm ( 𝐴𝐴 ) = 𝐴
53 51 6 7 5 5 52 off ( 𝜑 → ( 𝐹f + 𝐻 ) : 𝐴𝐵 )
54 1 19 22 24 3 5 53 tsmsval ( 𝜑 → ( 𝐺 tsums ( 𝐹f + 𝐻 ) ) = ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( ( 𝐹f + 𝐻 ) ↾ 𝑧 ) ) ) ) )
55 eqid ( 0g𝐺 ) = ( 0g𝐺 )
56 3 adantr ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐺 ∈ CMnd )
57 elinel2 ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ∈ Fin )
58 57 adantl ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑧 ∈ Fin )
59 elfpw ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑧𝐴𝑧 ∈ Fin ) )
60 59 simplbi ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧𝐴 )
61 fssres ( ( 𝐹 : 𝐴𝐵𝑧𝐴 ) → ( 𝐹𝑧 ) : 𝑧𝐵 )
62 6 60 61 syl2an ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑧 ) : 𝑧𝐵 )
63 fssres ( ( 𝐻 : 𝐴𝐵𝑧𝐴 ) → ( 𝐻𝑧 ) : 𝑧𝐵 )
64 7 60 63 syl2an ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐻𝑧 ) : 𝑧𝐵 )
65 fvexd ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 0g𝐺 ) ∈ V )
66 62 58 65 fdmfifsupp ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑧 ) finSupp ( 0g𝐺 ) )
67 64 58 65 fdmfifsupp ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐻𝑧 ) finSupp ( 0g𝐺 ) )
68 1 55 2 56 58 62 64 66 67 gsumadd ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( ( 𝐹𝑧 ) ∘f + ( 𝐻𝑧 ) ) ) = ( ( 𝐺 Σg ( 𝐹𝑧 ) ) + ( 𝐺 Σg ( 𝐻𝑧 ) ) ) )
69 6 5 fexd ( 𝜑𝐹 ∈ V )
70 7 5 fexd ( 𝜑𝐻 ∈ V )
71 offres ( ( 𝐹 ∈ V ∧ 𝐻 ∈ V ) → ( ( 𝐹f + 𝐻 ) ↾ 𝑧 ) = ( ( 𝐹𝑧 ) ∘f + ( 𝐻𝑧 ) ) )
72 69 70 71 syl2anc ( 𝜑 → ( ( 𝐹f + 𝐻 ) ↾ 𝑧 ) = ( ( 𝐹𝑧 ) ∘f + ( 𝐻𝑧 ) ) )
73 72 adantr ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐹f + 𝐻 ) ↾ 𝑧 ) = ( ( 𝐹𝑧 ) ∘f + ( 𝐻𝑧 ) ) )
74 73 oveq2d ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( ( 𝐹f + 𝐻 ) ↾ 𝑧 ) ) = ( 𝐺 Σg ( ( 𝐹𝑧 ) ∘f + ( 𝐻𝑧 ) ) ) )
75 1 2 16 plusfval ( ( ( 𝐺 Σg ( 𝐹𝑧 ) ) ∈ 𝐵 ∧ ( 𝐺 Σg ( 𝐻𝑧 ) ) ∈ 𝐵 ) → ( ( 𝐺 Σg ( 𝐹𝑧 ) ) ( +𝑓𝐺 ) ( 𝐺 Σg ( 𝐻𝑧 ) ) ) = ( ( 𝐺 Σg ( 𝐹𝑧 ) ) + ( 𝐺 Σg ( 𝐻𝑧 ) ) ) )
76 28 29 75 syl2anc ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐺 Σg ( 𝐹𝑧 ) ) ( +𝑓𝐺 ) ( 𝐺 Σg ( 𝐻𝑧 ) ) ) = ( ( 𝐺 Σg ( 𝐹𝑧 ) ) + ( 𝐺 Σg ( 𝐻𝑧 ) ) ) )
77 68 74 76 3eqtr4d ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( ( 𝐹f + 𝐻 ) ↾ 𝑧 ) ) = ( ( 𝐺 Σg ( 𝐹𝑧 ) ) ( +𝑓𝐺 ) ( 𝐺 Σg ( 𝐻𝑧 ) ) ) )
78 77 mpteq2dva ( 𝜑 → ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( ( 𝐹f + 𝐻 ) ↾ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( 𝐺 Σg ( 𝐹𝑧 ) ) ( +𝑓𝐺 ) ( 𝐺 Σg ( 𝐻𝑧 ) ) ) ) )
79 78 fveq2d ( 𝜑 → ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( ( 𝐹f + 𝐻 ) ↾ 𝑧 ) ) ) ) = ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( 𝐺 Σg ( 𝐹𝑧 ) ) ( +𝑓𝐺 ) ( 𝐺 Σg ( 𝐻𝑧 ) ) ) ) ) )
80 54 79 eqtrd ( 𝜑 → ( 𝐺 tsums ( 𝐹f + 𝐻 ) ) = ( ( ( TopOpen ‘ 𝐺 ) fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( 𝐺 Σg ( 𝐹𝑧 ) ) ( +𝑓𝐺 ) ( 𝐺 Σg ( 𝐻𝑧 ) ) ) ) ) )
81 46 80 eleqtrrd ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝐺 tsums ( 𝐹f + 𝐻 ) ) )