Theorem tsmssub 24473

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

Hypotheses

Ref	Expression
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

Ref	Expression
tsmssub	⊢ (𝜑 → (𝑋 − 𝑌) ∈ (𝐺 tsums (𝐹 ∘f − 𝐻)))

Proof of Theorem tsmssub

Dummy variables 𝑘 𝑥 are mutually distinct and distinct from all other variables.

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  Vcvv 3450   ↦ cmpt 5185   ∘ ccom 5654  ⟶wf 6534  ‘cfv 6538  (class class class)co 7420   ∘_f cof 7691  Basecbs 17392  +_gcplusg 17433  Grpcgrp 19149  inv_gcminusg 19150  -_gcsg 19151  CMndccmn 19999  TopSpctps 23255  TopMndctmd 24394  TopGrpctgp 24395   tsums ctsu 24450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11259  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279  ax-pre-mulgt0 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7693  df-om 7878  df-1st 8001  df-2nd 8002  df-supp 8180  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-1o 8479  df-er 8720  df-map 8852  df-en 8977  df-dom 8978  df-sdom 8979  df-fin 8980  df-fsupp 9357  df-oi 9507  df-card 10023  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-sub 11546  df-neg 11547  df-nn 12339  df-2 12408  df-n0 12610  df-z 12697  df-uz 12969  df-fz 13643  df-fzo 13792  df-seq 14148  df-hash 14478  df-sets 17347  df-slot 17365  df-ndx 17377  df-base 17393  df-ress 17414  df-plusg 17446  df-0g 17617  df-gsum 17618  df-topgen 17619  df-plusf 18820  df-mgm 18821  df-sgrp 18913  df-mnd 18929  df-mhm 18983  df-submnd 18984  df-grp 19152  df-minusg 19153  df-sbg 19154  df-ghm 19433  df-cntz 19536  df-cmn 20001  df-abl 20002  df-fbas 21680  df-fg 21681  df-top 23217  df-topon 23234  df-topsp 23256  df-bases 23269  df-ntr 23343  df-nei 23421  df-cn 23550  df-cnp 23551  df-tx 23886  df-fil 24170  df-fm 24262  df-flim 24263  df-flf 24264  df-tmd 24396  df-tgp 24397  df-tsms 24451

This theorem is used by:  tgptsmscls  24474