tsmsxplem2

	Ref	Expression
Hypotheses	tsmsxp.b	$⊢ B = {Base}_{G}$
	tsmsxp.g	$⊢ φ \to G \in CMnd$
	tsmsxp.2	$⊢ φ \to G \in TopGrp$
	tsmsxp.a	$⊢ φ \to A \in V$
	tsmsxp.c	$⊢ φ \to C \in W$
	tsmsxp.f	$⊢ φ \to F : A \times C ⟶ B$
	tsmsxp.h	$⊢ φ \to H : A ⟶ B$
	tsmsxp.1	$⊢ (φ \land j \in A) \to H (j) \in (G tsums (k \in C ⟼ j F k))$
	tsmsxp.j	$⊢ J = TopOpen (G)$
	tsmsxp.z	$⊢ \underset{˙}{0} = 0_{G}$
	tsmsxp.p	$⊢ \underset{˙}{+} = +_{G}$
	tsmsxp.m	$⊢ \underset{˙}{-} = -_{G}$
	tsmsxp.l	$⊢ φ \to L \in J$
	tsmsxp.3	$⊢ φ \to \underset{˙}{0} \in L$
	tsmsxp.k	$⊢ φ \to K \in (𝒫 A \cap Fin)$
	tsmsxp.4	$⊢ φ \to \forall c \in S \forall d \in T c \underset{˙}{+} d \in U$
	tsmsxp.n	$⊢ φ \to N \in (𝒫 C \cap Fin)$
	tsmsxp.s	$⊢ φ \to D \subseteq K \times N$
	tsmsxp.x	$⊢ φ \to \forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times N)})) \in L$
	tsmsxp.5	$⊢ φ \to \sum_{G} ({F ↾}_{(K \times N)}) \in S$
	tsmsxp.6	$⊢ φ \to \forall g \in (L^{K}) \sum_{G} g \in T$
Assertion	tsmsxplem2	$⊢ φ \to \sum_{G} ({H ↾}_{K}) \in U$

Proof

Step	Hyp	Ref	Expression
1		tsmsxp.b	$⊢ B = {Base}_{G}$
2		tsmsxp.g	$⊢ φ \to G \in CMnd$
3		tsmsxp.2	$⊢ φ \to G \in TopGrp$
4		tsmsxp.a	$⊢ φ \to A \in V$
5		tsmsxp.c	$⊢ φ \to C \in W$
6		tsmsxp.f	$⊢ φ \to F : A \times C ⟶ B$
7		tsmsxp.h	$⊢ φ \to H : A ⟶ B$
8		tsmsxp.1	$⊢ (φ \land j \in A) \to H (j) \in (G tsums (k \in C ⟼ j F k))$
9		tsmsxp.j	$⊢ J = TopOpen (G)$
10		tsmsxp.z	$⊢ \underset{˙}{0} = 0_{G}$
11		tsmsxp.p	$⊢ \underset{˙}{+} = +_{G}$
12		tsmsxp.m	$⊢ \underset{˙}{-} = -_{G}$
13		tsmsxp.l	$⊢ φ \to L \in J$
14		tsmsxp.3	$⊢ φ \to \underset{˙}{0} \in L$
15		tsmsxp.k	$⊢ φ \to K \in (𝒫 A \cap Fin)$
16		tsmsxp.4	$⊢ φ \to \forall c \in S \forall d \in T c \underset{˙}{+} d \in U$
17		tsmsxp.n	$⊢ φ \to N \in (𝒫 C \cap Fin)$
18		tsmsxp.s	$⊢ φ \to D \subseteq K \times N$
19		tsmsxp.x	$⊢ φ \to \forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times N)})) \in L$
20		tsmsxp.5	$⊢ φ \to \sum_{G} ({F ↾}_{(K \times N)}) \in S$
21		tsmsxp.6	$⊢ φ \to \forall g \in (L^{K}) \sum_{G} g \in T$
22		tgpgrp	$⊢ G \in TopGrp \to G \in Grp$
23	3 22	syl	$⊢ φ \to G \in Grp$
24		isabl	$⊢ G \in Abel \leftrightarrow (G \in Grp \land G \in CMnd)$
25	23 2 24	sylanbrc	$⊢ φ \to G \in Abel$
26	15	elin2d	$⊢ φ \to K \in Fin$
27	17	elin2d	$⊢ φ \to N \in Fin$
28		xpfi	$⊢ (K \in Fin \land N \in Fin) \to K \times N \in Fin$
29	26 27 28	syl2anc	$⊢ φ \to K \times N \in Fin$
30		elfpw	$⊢ K \in (𝒫 A \cap Fin) \leftrightarrow (K \subseteq A \land K \in Fin)$
31	30	simplbi	$⊢ K \in (𝒫 A \cap Fin) \to K \subseteq A$
32	15 31	syl	$⊢ φ \to K \subseteq A$
33		elfpw	$⊢ N \in (𝒫 C \cap Fin) \leftrightarrow (N \subseteq C \land N \in Fin)$
34	33	simplbi	$⊢ N \in (𝒫 C \cap Fin) \to N \subseteq C$
35	17 34	syl	$⊢ φ \to N \subseteq C$
36		xpss12	$⊢ (K \subseteq A \land N \subseteq C) \to K \times N \subseteq A \times C$
37	32 35 36	syl2anc	$⊢ φ \to K \times N \subseteq A \times C$
38	6 37	fssresd	$⊢ φ \to ({F ↾}_{(K \times N)}) : K \times N ⟶ B$
39	38 29 14	fdmfifsupp	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (({F ↾}_{(K \times N)}))$
40	1 10 2 29 38 39	gsumcl	$⊢ φ \to \sum_{G} ({F ↾}_{(K \times N)}) \in B$
41	7 32	fssresd	$⊢ φ \to ({H ↾}_{K}) : K ⟶ B$
42	41 26 14	fdmfifsupp	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (({H ↾}_{K}))$
43	1 10 2 15 41 42	gsumcl	$⊢ φ \to \sum_{G} ({H ↾}_{K}) \in B$
44	1 11 12	ablpncan3	$⊢ (G \in Abel \land (\sum_{G} ({F ↾}_{(K \times N)}) \in B \land \sum_{G} ({H ↾}_{K}) \in B)) \to (\sum_{G}, ({F ↾}_{(K \times N)})) \underset{˙}{+} ((\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(K \times N)}))) = \sum_{G} ({H ↾}_{K})$
45	25 40 43 44	syl12anc	$⊢ φ \to (\sum_{G}, ({F ↾}_{(K \times N)})) \underset{˙}{+} ((\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(K \times N)}))) = \sum_{G} ({H ↾}_{K})$
46	2	adantr	$⊢ (φ \land y \in K) \to G \in CMnd$
47		snfi	$⊢ \{y\} \in Fin$
48	27	adantr	$⊢ (φ \land y \in K) \to N \in Fin$
49		xpfi	$⊢ (\{y\} \in Fin \land N \in Fin) \to \{y\} \times N \in Fin$
50	47 48 49	sylancr	$⊢ (φ \land y \in K) \to \{y\} \times N \in Fin$
51	6	adantr	$⊢ (φ \land y \in K) \to F : A \times C ⟶ B$
52	32	sselda	$⊢ (φ \land y \in K) \to y \in A$
53	52	snssd	$⊢ (φ \land y \in K) \to \{y\} \subseteq A$
54	35	adantr	$⊢ (φ \land y \in K) \to N \subseteq C$
55		xpss12	$⊢ (\{y\} \subseteq A \land N \subseteq C) \to \{y\} \times N \subseteq A \times C$
56	53 54 55	syl2anc	$⊢ (φ \land y \in K) \to \{y\} \times N \subseteq A \times C$
57	51 56	fssresd	$⊢ (φ \land y \in K) \to ({F ↾}_{(\{y\} \times N)}) : \{y\} \times N ⟶ B$
58	10	fvexi	$⊢ \underset{˙}{0} \in V$
59	58	a1i	$⊢ (φ \land y \in K) \to \underset{˙}{0} \in V$
60	57 50 59	fdmfifsupp	$⊢ (φ \land y \in K) \to {finSupp}_{\underset{˙}{0}} (({F ↾}_{(\{y\} \times N)}))$
61	1 10 46 50 57 60	gsumcl	$⊢ (φ \land y \in K) \to \sum_{G} ({F ↾}_{(\{y\} \times N)}) \in B$
62	61	fmpttd	$⊢ φ \to (y \in K ⟼ \sum_{G} ({F ↾}_{(\{y\} \times N)})) : K ⟶ B$
63		eqid	$⊢ (y \in K ⟼ \sum_{G} ({F ↾}_{(\{y\} \times N)})) = (y \in K ⟼ \sum_{G} ({F ↾}_{(\{y\} \times N)}))$
64		ovexd	$⊢ (φ \land y \in K) \to \sum_{G} ({F ↾}_{(\{y\} \times N)}) \in V$
65	63 26 64 14	fsuppmptdm	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((y \in K ⟼ \sum_{G} ({F ↾}_{(\{y\} \times N)})))$
66	1 10 12 25 15 41 62 42 65	gsumsub	$⊢ φ \to \sum_{G} (({H ↾}_{K}) {\underset{˙}{-}}_{f} (y \in K ⟼ \sum_{G} ({F ↾}_{(\{y\} \times N)}))) = (\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\underset{y \in K}{\sum_{G}}, (\sum_{G}, ({F ↾}_{(\{y\} \times N)})))$
67		fvexd	$⊢ (φ \land y \in K) \to H (y) \in V$
68	7 32	feqresmpt	$⊢ φ \to {H ↾}_{K} = (y \in K ⟼ H (y))$
69		eqidd	$⊢ φ \to (y \in K ⟼ \sum_{G} ({F ↾}_{(\{y\} \times N)})) = (y \in K ⟼ \sum_{G} ({F ↾}_{(\{y\} \times N)}))$
70	15 67 64 68 69	offval2	$⊢ φ \to ({H ↾}_{K}) {\underset{˙}{-}}_{f} (y \in K ⟼ \sum_{G} ({F ↾}_{(\{y\} \times N)})) = (y \in K ⟼ H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)})))$
71	70	oveq2d	$⊢ φ \to \sum_{G} (({H ↾}_{K}) {\underset{˙}{-}}_{f} (y \in K ⟼ \sum_{G} ({F ↾}_{(\{y\} \times N)}))) = \underset{y \in K}{\sum_{G}} (H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)})))$
72		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
73	46 72	syl	$⊢ (φ \land y \in K) \to G \in Mnd$
74		simpr	$⊢ (φ \land y \in K) \to y \in K$
75	51	adantr	$⊢ ((φ \land y \in K) \land z \in N) \to F : A \times C ⟶ B$
76	52	adantr	$⊢ ((φ \land y \in K) \land z \in N) \to y \in A$
77	54	sselda	$⊢ ((φ \land y \in K) \land z \in N) \to z \in C$
78	75 76 77	fovrnd	$⊢ ((φ \land y \in K) \land z \in N) \to y F z \in B$
79	78	fmpttd	$⊢ (φ \land y \in K) \to (z \in N ⟼ y F z) : N ⟶ B$
80		eqid	$⊢ (z \in N ⟼ y F z) = (z \in N ⟼ y F z)$
81		ovexd	$⊢ ((φ \land y \in K) \land z \in N) \to y F z \in V$
82	80 48 81 59	fsuppmptdm	$⊢ (φ \land y \in K) \to {finSupp}_{\underset{˙}{0}} ((z \in N ⟼ y F z))$
83	1 10 46 48 79 82	gsumcl	$⊢ (φ \land y \in K) \to \underset{z \in N}{\sum_{G}} (y F z) \in B$
84		velsn	$⊢ w \in \{y\} \leftrightarrow w = y$
85		ovres	$⊢ (w \in \{y\} \land z \in N) \to w ({F ↾}_{(\{y\} \times N)}) z = w F z$
86	84 85	sylanbr	$⊢ (w = y \land z \in N) \to w ({F ↾}_{(\{y\} \times N)}) z = w F z$
87		oveq1	$⊢ w = y \to w F z = y F z$
88	87	adantr	$⊢ (w = y \land z \in N) \to w F z = y F z$
89	86 88	eqtrd	$⊢ (w = y \land z \in N) \to w ({F ↾}_{(\{y\} \times N)}) z = y F z$
90	89	mpteq2dva	$⊢ w = y \to (z \in N ⟼ w ({F ↾}_{(\{y\} \times N)}) z) = (z \in N ⟼ y F z)$
91	90	oveq2d	$⊢ w = y \to \underset{z \in N}{\sum_{G}} (w ({F ↾}_{(\{y\} \times N)}) z) = \underset{z \in N}{\sum_{G}} (y F z)$
92	1 91	gsumsn	$⊢ (G \in Mnd \land y \in K \land \underset{z \in N}{\sum_{G}} (y F z) \in B) \to \underset{w \in \{y\}}{\sum_{G}} (\underset{z \in N}{\sum_{G}}, (w ({F ↾}_{(\{y\} \times N)}) z)) = \underset{z \in N}{\sum_{G}} (y F z)$
93	73 74 83 92	syl3anc	$⊢ (φ \land y \in K) \to \underset{w \in \{y\}}{\sum_{G}} (\underset{z \in N}{\sum_{G}}, (w ({F ↾}_{(\{y\} \times N)}) z)) = \underset{z \in N}{\sum_{G}} (y F z)$
94	47	a1i	$⊢ (φ \land y \in K) \to \{y\} \in Fin$
95	1 10 46 94 48 57 60	gsumxp	$⊢ (φ \land y \in K) \to \sum_{G} ({F ↾}_{(\{y\} \times N)}) = \underset{w \in \{y\}}{\sum_{G}} (\underset{z \in N}{\sum_{G}}, (w ({F ↾}_{(\{y\} \times N)}) z))$
96		ovres	$⊢ (y \in K \land z \in N) \to y ({F ↾}_{(K \times N)}) z = y F z$
97	96	adantll	$⊢ ((φ \land y \in K) \land z \in N) \to y ({F ↾}_{(K \times N)}) z = y F z$
98	97	mpteq2dva	$⊢ (φ \land y \in K) \to (z \in N ⟼ y ({F ↾}_{(K \times N)}) z) = (z \in N ⟼ y F z)$
99	98	oveq2d	$⊢ (φ \land y \in K) \to \underset{z \in N}{\sum_{G}} (y ({F ↾}_{(K \times N)}) z) = \underset{z \in N}{\sum_{G}} (y F z)$
100	93 95 99	3eqtr4d	$⊢ (φ \land y \in K) \to \sum_{G} ({F ↾}_{(\{y\} \times N)}) = \underset{z \in N}{\sum_{G}} (y ({F ↾}_{(K \times N)}) z)$
101	100	mpteq2dva	$⊢ φ \to (y \in K ⟼ \sum_{G} ({F ↾}_{(\{y\} \times N)})) = (y \in K ⟼ \underset{z \in N}{\sum_{G}} (y ({F ↾}_{(K \times N)}) z))$
102	101	oveq2d	$⊢ φ \to \underset{y \in K}{\sum_{G}} (\sum_{G}, ({F ↾}_{(\{y\} \times N)})) = \underset{y \in K}{\sum_{G}} (\underset{z \in N}{\sum_{G}}, (y ({F ↾}_{(K \times N)}) z))$
103	1 10 2 26 27 38 39	gsumxp	$⊢ φ \to \sum_{G} ({F ↾}_{(K \times N)}) = \underset{y \in K}{\sum_{G}} (\underset{z \in N}{\sum_{G}}, (y ({F ↾}_{(K \times N)}) z))$
104	102 103	eqtr4d	$⊢ φ \to \underset{y \in K}{\sum_{G}} (\sum_{G}, ({F ↾}_{(\{y\} \times N)})) = \sum_{G} ({F ↾}_{(K \times N)})$
105	104	oveq2d	$⊢ φ \to (\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\underset{y \in K}{\sum_{G}}, (\sum_{G}, ({F ↾}_{(\{y\} \times N)}))) = (\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(K \times N)}))$
106	66 71 105	3eqtr3d	$⊢ φ \to \underset{y \in K}{\sum_{G}} (H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)}))) = (\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(K \times N)}))$
107		oveq2	$⊢ g = (y \in K ⟼ H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)}))) \to \sum_{G} g = \underset{y \in K}{\sum_{G}} (H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)})))$
108	107	eleq1d	$⊢ g = (y \in K ⟼ H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)}))) \to (\sum_{G} g \in T \leftrightarrow \underset{y \in K}{\sum_{G}} (H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)}))) \in T)$
109		fveq2	$⊢ x = y \to H (x) = H (y)$
110		sneq	$⊢ x = y \to \{x\} = \{y\}$
111	110	xpeq1d	$⊢ x = y \to \{x\} \times N = \{y\} \times N$
112	111	reseq2d	$⊢ x = y \to {F ↾}_{(\{x\} \times N)} = {F ↾}_{(\{y\} \times N)}$
113	112	oveq2d	$⊢ x = y \to \sum_{G} ({F ↾}_{(\{x\} \times N)}) = \sum_{G} ({F ↾}_{(\{y\} \times N)})$
114	109 113	oveq12d	$⊢ x = y \to H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times N)})) = H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)}))$
115	114	eleq1d	$⊢ x = y \to (H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times N)})) \in L \leftrightarrow H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)})) \in L)$
116	115	rspccva	$⊢ (\forall x \in K H (x) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{x\} \times N)})) \in L \land y \in K) \to H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)})) \in L$
117	19 116	sylan	$⊢ (φ \land y \in K) \to H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)})) \in L$
118	117	fmpttd	$⊢ φ \to (y \in K ⟼ H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)}))) : K ⟶ L$
119	13 15	elmapd	$⊢ φ \to ((y \in K ⟼ H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)}))) \in (L^{K}) \leftrightarrow (y \in K ⟼ H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)}))) : K ⟶ L)$
120	118 119	mpbird	$⊢ φ \to (y \in K ⟼ H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)}))) \in (L^{K})$
121	108 21 120	rspcdva	$⊢ φ \to \underset{y \in K}{\sum_{G}} (H (y) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(\{y\} \times N)}))) \in T$
122	106 121	eqeltrrd	$⊢ φ \to (\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(K \times N)})) \in T$
123		oveq1	$⊢ c = \sum_{G} ({F ↾}_{(K \times N)}) \to c \underset{˙}{+} d = (\sum_{G}, ({F ↾}_{(K \times N)})) \underset{˙}{+} d$
124	123	eleq1d	$⊢ c = \sum_{G} ({F ↾}_{(K \times N)}) \to (c \underset{˙}{+} d \in U \leftrightarrow (\sum_{G}, ({F ↾}_{(K \times N)})) \underset{˙}{+} d \in U)$
125		oveq2	$⊢ d = (\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(K \times N)})) \to (\sum_{G}, ({F ↾}_{(K \times N)})) \underset{˙}{+} d = (\sum_{G}, ({F ↾}_{(K \times N)})) \underset{˙}{+} ((\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(K \times N)})))$
126	125	eleq1d	$⊢ d = (\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(K \times N)})) \to ((\sum_{G}, ({F ↾}_{(K \times N)})) \underset{˙}{+} d \in U \leftrightarrow (\sum_{G}, ({F ↾}_{(K \times N)})) \underset{˙}{+} ((\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(K \times N)}))) \in U)$
127	124 126	rspc2va	$⊢ ((\sum_{G} ({F ↾}_{(K \times N)}) \in S \land (\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(K \times N)})) \in T) \land \forall c \in S \forall d \in T c \underset{˙}{+} d \in U) \to (\sum_{G}, ({F ↾}_{(K \times N)})) \underset{˙}{+} ((\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(K \times N)}))) \in U$
128	20 122 16 127	syl21anc	$⊢ φ \to (\sum_{G}, ({F ↾}_{(K \times N)})) \underset{˙}{+} ((\sum_{G}, ({H ↾}_{K})) \underset{˙}{-} (\sum_{G}, ({F ↾}_{(K \times N)}))) \in U$
129	45 128	eqeltrrd	$⊢ φ \to \sum_{G} ({H ↾}_{K}) \in U$

Metamath Proof Explorer

Theorem tsmsxplem2

Proof