Metamath Proof Explorer

Theorem tsmssub

Description: The difference of two infinite group sums. (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypotheses tsmssub.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
tsmssub.p ⊢ − = ( -g ‘ 𝐺 )
tsmssub.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tsmssub.2 ⊢ ( 𝜑 → 𝐺 ∈ TopGrp )
tsmssub.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tsmssub.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
tsmssub.h ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
tsmssub.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
tsmssub.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐺 tsums 𝐻 ) )
Assertion tsmssub ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ ( 𝐺 tsums ( 𝐹 ∘f − 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 tsmssub.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tsmssub.p ⊢ − = ( -g ‘ 𝐺 )
3 tsmssub.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 tsmssub.2 ⊢ ( 𝜑 → 𝐺 ∈ TopGrp )
5 tsmssub.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 tsmssub.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 tsmssub.h ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
8 tsmssub.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
9 tsmssub.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐺 tsums 𝐻 ) )
10 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
11 tgptmd ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd )
12 4 11 syl ⊢ ( 𝜑 → 𝐺 ∈ TopMnd )
13 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
14 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
15 1 14 grpinvf ⊢ ( 𝐺 ∈ Grp → ( invg ‘ 𝐺 ) : 𝐵 ⟶ 𝐵 )
16 4 13 15 3syl ⊢ ( 𝜑 → ( invg ‘ 𝐺 ) : 𝐵 ⟶ 𝐵 )
17 fco ⊢ ( ( ( invg ‘ 𝐺 ) : 𝐵 ⟶ 𝐵 ∧ 𝐻 : 𝐴 ⟶ 𝐵 ) → ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) : 𝐴 ⟶ 𝐵 )
18 16 7 17 syl2anc ⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) : 𝐴 ⟶ 𝐵 )
19 1 14 3 4 5 7 9 tsmsinv ⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ∈ ( 𝐺 tsums ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) )
20 1 10 3 12 5 6 18 8 19 tsmsadd ⊢ ( 𝜑 → ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) ∈ ( 𝐺 tsums ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) )
21 tgptps ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopSp )
22 4 21 syl ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
23 1 3 22 5 6 tsmscl ⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) ⊆ 𝐵 )
24 23 8 sseldd ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
25 1 3 22 5 7 tsmscl ⊢ ( 𝜑 → ( 𝐺 tsums 𝐻 ) ⊆ 𝐵 )
26 25 9 sseldd ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
27 1 10 14 2 grpsubval ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
28 24 26 27 syl2anc ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑌 ) ) )
29 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 )
30 7 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑘 ) ∈ 𝐵 )
31 1 10 14 2 grpsubval ⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑘 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐻 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) )
32 29 30 31 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐻 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) )
33 32 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐻 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
34 6 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
35 7 feqmptd ⊢ ( 𝜑 → 𝐻 = ( 𝑘 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑘 ) ) )
36 5 29 30 34 35 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐻 ) = ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐻 ‘ 𝑘 ) ) ) )
37 fvexd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ∈ V )
38 16 feqmptd ⊢ ( 𝜑 → ( invg ‘ 𝐺 ) = ( 𝑥 ∈ 𝐵 ↦ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) )
39 fveq2 ⊢ ( 𝑥 = ( 𝐻 ‘ 𝑘 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) )
40 30 35 38 39 fmptco ⊢ ( 𝜑 → ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) = ( 𝑘 ∈ 𝐴 ↦ ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) )
41 5 29 37 34 40 offval2 ⊢ ( 𝜑 → ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) = ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ ( 𝐻 ‘ 𝑘 ) ) ) ) )
42 33 36 41 3eqtr4d ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐻 ) = ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) )
43 42 oveq2d ⊢ ( 𝜑 → ( 𝐺 tsums ( 𝐹 ∘f − 𝐻 ) ) = ( 𝐺 tsums ( 𝐹 ∘f ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ∘ 𝐻 ) ) ) )
44 20 28 43 3eltr4d ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ ( 𝐺 tsums ( 𝐹 ∘f − 𝐻 ) ) )