tsmssub

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

	Ref	Expression
Hypotheses	tsmssub.b	$⊢ B = {Base}_{G}$
	tsmssub.p	$⊢ \underset{˙}{-} = -_{G}$
	tsmssub.1	$⊢ φ \to G \in CMnd$
	tsmssub.2	$⊢ φ \to G \in TopGrp$
	tsmssub.a	$⊢ φ \to A \in V$
	tsmssub.f	$⊢ φ \to F : A ⟶ B$
	tsmssub.h	$⊢ φ \to H : A ⟶ B$
	tsmssub.x	$⊢ φ \to X \in (G tsums F)$
	tsmssub.y	$⊢ φ \to Y \in (G tsums H)$
Assertion	tsmssub	$⊢ φ \to X \underset{˙}{-} Y \in (G tsums (F {\underset{˙}{-}}_{f} H))$

Proof

Step	Hyp	Ref	Expression
1		tsmssub.b	$⊢ B = {Base}_{G}$
2		tsmssub.p	$⊢ \underset{˙}{-} = -_{G}$
3		tsmssub.1	$⊢ φ \to G \in CMnd$
4		tsmssub.2	$⊢ φ \to G \in TopGrp$
5		tsmssub.a	$⊢ φ \to A \in V$
6		tsmssub.f	$⊢ φ \to F : A ⟶ B$
7		tsmssub.h	$⊢ φ \to H : A ⟶ B$
8		tsmssub.x	$⊢ φ \to X \in (G tsums F)$
9		tsmssub.y	$⊢ φ \to Y \in (G tsums H)$
10		eqid	$⊢ +_{G} = +_{G}$
11		tgptmd	$⊢ G \in TopGrp \to G \in TopMnd$
12	4 11	syl	$⊢ φ \to G \in TopMnd$
13		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
14		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
15	1 14	grpinvf	$⊢ G \in Grp \to {inv}_{g} (G) : B ⟶ B$
16	4 13 15	3syl	$⊢ φ \to {inv}_{g} (G) : B ⟶ B$
17		fco	$⊢ ({inv}_{g} (G) : B ⟶ B \land H : A ⟶ B) \to ({inv}_{g} (G) \circ H) : A ⟶ B$
18	16 7 17	syl2anc	$⊢ φ \to ({inv}_{g} (G) \circ H) : A ⟶ B$
19	1 14 3 4 5 7 9	tsmsinv	$⊢ φ \to {inv}_{g} (G) (Y) \in (G tsums ({inv}_{g} (G) \circ H))$
20	1 10 3 12 5 6 18 8 19	tsmsadd	$⊢ φ \to X +_{G} {inv}_{g} (G) (Y) \in (G tsums (F {+_{G}}_{f} ({inv}_{g} (G) \circ H)))$
21		tgptps	$⊢ G \in TopGrp \to G \in TopSp$
22	4 21	syl	$⊢ φ \to G \in TopSp$
23	1 3 22 5 6	tsmscl	$⊢ φ \to G tsums F \subseteq B$
24	23 8	sseldd	$⊢ φ \to X \in B$
25	1 3 22 5 7	tsmscl	$⊢ φ \to G tsums H \subseteq B$
26	25 9	sseldd	$⊢ φ \to Y \in B$
27	1 10 14 2	grpsubval	$⊢ (X \in B \land Y \in B) \to X \underset{˙}{-} Y = X +_{G} {inv}_{g} (G) (Y)$
28	24 26 27	syl2anc	$⊢ φ \to X \underset{˙}{-} Y = X +_{G} {inv}_{g} (G) (Y)$
29	6	ffvelrnda	$⊢ (φ \land k \in A) \to F (k) \in B$
30	7	ffvelrnda	$⊢ (φ \land k \in A) \to H (k) \in B$
31	1 10 14 2	grpsubval	$⊢ (F (k) \in B \land H (k) \in B) \to F (k) \underset{˙}{-} H (k) = F (k) +_{G} {inv}_{g} (G) (H (k))$
32	29 30 31	syl2anc	$⊢ (φ \land k \in A) \to F (k) \underset{˙}{-} H (k) = F (k) +_{G} {inv}_{g} (G) (H (k))$
33	32	mpteq2dva	$⊢ φ \to (k \in A ⟼ F (k) \underset{˙}{-} H (k)) = (k \in A ⟼ F (k) +_{G} {inv}_{g} (G) (H (k)))$
34	6	feqmptd	$⊢ φ \to F = (k \in A ⟼ F (k))$
35	7	feqmptd	$⊢ φ \to H = (k \in A ⟼ H (k))$
36	5 29 30 34 35	offval2	$⊢ φ \to F {\underset{˙}{-}}_{f} H = (k \in A ⟼ F (k) \underset{˙}{-} H (k))$
37		fvexd	$⊢ (φ \land k \in A) \to {inv}_{g} (G) (H (k)) \in V$
38	16	feqmptd	$⊢ φ \to {inv}_{g} (G) = (x \in B ⟼ {inv}_{g} (G) (x))$
39		fveq2	$⊢ x = H (k) \to {inv}_{g} (G) (x) = {inv}_{g} (G) (H (k))$
40	30 35 38 39	fmptco	$⊢ φ \to {inv}_{g} (G) \circ H = (k \in A ⟼ {inv}_{g} (G) (H (k)))$
41	5 29 37 34 40	offval2	$⊢ φ \to F {+_{G}}_{f} ({inv}_{g} (G) \circ H) = (k \in A ⟼ F (k) +_{G} {inv}_{g} (G) (H (k)))$
42	33 36 41	3eqtr4d	$⊢ φ \to F {\underset{˙}{-}}_{f} H = F {+_{G}}_{f} ({inv}_{g} (G) \circ H)$
43	42	oveq2d	$⊢ φ \to G tsums (F {\underset{˙}{-}}_{f} H) = G tsums (F {+_{G}}_{f} ({inv}_{g} (G) \circ H))$
44	20 28 43	3eltr4d	$⊢ φ \to X \underset{˙}{-} Y \in (G tsums (F {\underset{˙}{-}}_{f} H))$

Metamath Proof Explorer

Theorem tsmssub

Proof