tmdgsum

Description: In a topological monoid, the group sum operation is a continuous function from the function space to the base topology. This theorem is not true when A is infinite, because in this case for any basic open set of the domain one of the factors will be the whole space, so by varying the value of the functions to sum at this index, one can achieve any desired sum. (Contributed by Mario Carneiro, 19-Sep-2015) (Proof shortened by AV, 24-Jul-2019)

	Ref	Expression
Hypotheses	tmdgsum.j	$⊢ J = TopOpen (G)$
	tmdgsum.b	$⊢ B = {Base}_{G}$
Assertion	tmdgsum	$⊢ (G \in CMnd \land G \in TopMnd \land A \in Fin) \to (x \in (B^{A}) ⟼ \sum_{G} x) \in ((J^_{ko} 𝒫 A) Cn J)$

Proof

Step	Hyp	Ref	Expression
1		tmdgsum.j	$⊢ J = TopOpen (G)$
2		tmdgsum.b	$⊢ B = {Base}_{G}$
3		oveq2	$⊢ w = \emptyset \to B^{w} = B^{\emptyset}$
4	3	mpteq1d	$⊢ w = \emptyset \to (x \in (B^{w}) ⟼ \sum_{G} x) = (x \in (B^{\emptyset}) ⟼ \sum_{G} x)$
5		xpeq1	$⊢ w = \emptyset \to w \times \{J\} = \emptyset \times \{J\}$
6		0xp	$⊢ \emptyset \times \{J\} = \emptyset$
7	5 6	eqtrdi	$⊢ w = \emptyset \to w \times \{J\} = \emptyset$
8	7	fveq2d	$⊢ w = \emptyset \to \prod_{𝑡} (w \times \{J\}) = \prod_{𝑡} (\emptyset)$
9	8	oveq1d	$⊢ w = \emptyset \to \prod_{𝑡} (w \times \{J\}) Cn J = \prod_{𝑡} (\emptyset) Cn J$
10	4 9	eleq12d	$⊢ w = \emptyset \to ((x \in (B^{w}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (w \times \{J\}) Cn J) \leftrightarrow (x \in (B^{\emptyset}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (\emptyset) Cn J))$
11	10	imbi2d	$⊢ w = \emptyset \to (((G \in CMnd \land G \in TopMnd) \to (x \in (B^{w}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (w \times \{J\}) Cn J)) \leftrightarrow ((G \in CMnd \land G \in TopMnd) \to (x \in (B^{\emptyset}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (\emptyset) Cn J)))$
12		oveq2	$⊢ w = y \to B^{w} = B^{y}$
13	12	mpteq1d	$⊢ w = y \to (x \in (B^{w}) ⟼ \sum_{G} x) = (x \in (B^{y}) ⟼ \sum_{G} x)$
14		xpeq1	$⊢ w = y \to w \times \{J\} = y \times \{J\}$
15	14	fveq2d	$⊢ w = y \to \prod_{𝑡} (w \times \{J\}) = \prod_{𝑡} (y \times \{J\})$
16	15	oveq1d	$⊢ w = y \to \prod_{𝑡} (w \times \{J\}) Cn J = \prod_{𝑡} (y \times \{J\}) Cn J$
17	13 16	eleq12d	$⊢ w = y \to ((x \in (B^{w}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (w \times \{J\}) Cn J) \leftrightarrow (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J))$
18	17	imbi2d	$⊢ w = y \to (((G \in CMnd \land G \in TopMnd) \to (x \in (B^{w}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (w \times \{J\}) Cn J)) \leftrightarrow ((G \in CMnd \land G \in TopMnd) \to (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)))$
19		oveq2	$⊢ w = y \cup \{z\} \to B^{w} = B^{(y \cup \{z\})}$
20	19	mpteq1d	$⊢ w = y \cup \{z\} \to (x \in (B^{w}) ⟼ \sum_{G} x) = (x \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} x)$
21		xpeq1	$⊢ w = y \cup \{z\} \to w \times \{J\} = (y \cup \{z\}) \times \{J\}$
22	21	fveq2d	$⊢ w = y \cup \{z\} \to \prod_{𝑡} (w \times \{J\}) = \prod_{𝑡} ((y \cup \{z\}) \times \{J\})$
23	22	oveq1d	$⊢ w = y \cup \{z\} \to \prod_{𝑡} (w \times \{J\}) Cn J = \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn J$
24	20 23	eleq12d	$⊢ w = y \cup \{z\} \to ((x \in (B^{w}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (w \times \{J\}) Cn J) \leftrightarrow (x \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} x) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn J))$
25	24	imbi2d	$⊢ w = y \cup \{z\} \to (((G \in CMnd \land G \in TopMnd) \to (x \in (B^{w}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (w \times \{J\}) Cn J)) \leftrightarrow ((G \in CMnd \land G \in TopMnd) \to (x \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} x) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn J)))$
26		oveq2	$⊢ w = A \to B^{w} = B^{A}$
27	26	mpteq1d	$⊢ w = A \to (x \in (B^{w}) ⟼ \sum_{G} x) = (x \in (B^{A}) ⟼ \sum_{G} x)$
28		xpeq1	$⊢ w = A \to w \times \{J\} = A \times \{J\}$
29	28	fveq2d	$⊢ w = A \to \prod_{𝑡} (w \times \{J\}) = \prod_{𝑡} (A \times \{J\})$
30	29	oveq1d	$⊢ w = A \to \prod_{𝑡} (w \times \{J\}) Cn J = \prod_{𝑡} (A \times \{J\}) Cn J$
31	27 30	eleq12d	$⊢ w = A \to ((x \in (B^{w}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (w \times \{J\}) Cn J) \leftrightarrow (x \in (B^{A}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (A \times \{J\}) Cn J))$
32	31	imbi2d	$⊢ w = A \to (((G \in CMnd \land G \in TopMnd) \to (x \in (B^{w}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (w \times \{J\}) Cn J)) \leftrightarrow ((G \in CMnd \land G \in TopMnd) \to (x \in (B^{A}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (A \times \{J\}) Cn J)))$
33		elmapfn	$⊢ x \in (B^{\emptyset}) \to x Fn \emptyset$
34		fn0	$⊢ x Fn \emptyset \leftrightarrow x = \emptyset$
35	33 34	sylib	$⊢ x \in (B^{\emptyset}) \to x = \emptyset$
36	35	oveq2d	$⊢ x \in (B^{\emptyset}) \to \sum_{G} x = \sum_{G} \emptyset$
37		eqid	$⊢ 0_{G} = 0_{G}$
38	37	gsum0	$⊢ \sum_{G} \emptyset = 0_{G}$
39	36 38	eqtrdi	$⊢ x \in (B^{\emptyset}) \to \sum_{G} x = 0_{G}$
40	39	mpteq2ia	$⊢ (x \in (B^{\emptyset}) ⟼ \sum_{G} x) = (x \in (B^{\emptyset}) ⟼ 0_{G})$
41		0ex	$⊢ \emptyset \in V$
42	1 2	tmdtopon	$⊢ G \in TopMnd \to J \in TopOn (B)$
43	42	adantl	$⊢ (G \in CMnd \land G \in TopMnd) \to J \in TopOn (B)$
44	6	fveq2i	$⊢ \prod_{𝑡} (\emptyset \times \{J\}) = \prod_{𝑡} (\emptyset)$
45	44	eqcomi	$⊢ \prod_{𝑡} (\emptyset) = \prod_{𝑡} (\emptyset \times \{J\})$
46	45	pttoponconst	$⊢ (\emptyset \in V \land J \in TopOn (B)) \to \prod_{𝑡} (\emptyset) \in TopOn (B^{\emptyset})$
47	41 43 46	sylancr	$⊢ (G \in CMnd \land G \in TopMnd) \to \prod_{𝑡} (\emptyset) \in TopOn (B^{\emptyset})$
48		tmdmnd	$⊢ G \in TopMnd \to G \in Mnd$
49	48	adantl	$⊢ (G \in CMnd \land G \in TopMnd) \to G \in Mnd$
50	2 37	mndidcl	$⊢ G \in Mnd \to 0_{G} \in B$
51	49 50	syl	$⊢ (G \in CMnd \land G \in TopMnd) \to 0_{G} \in B$
52	47 43 51	cnmptc	$⊢ (G \in CMnd \land G \in TopMnd) \to (x \in (B^{\emptyset}) ⟼ 0_{G}) \in (\prod_{𝑡} (\emptyset) Cn J)$
53	40 52	eqeltrid	$⊢ (G \in CMnd \land G \in TopMnd) \to (x \in (B^{\emptyset}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (\emptyset) Cn J)$
54		oveq2	$⊢ x = w \to \sum_{G} x = \sum_{G} w$
55	54	cbvmptv	$⊢ (x \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} x) = (w \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} w)$
56		eqid	$⊢ +_{G} = +_{G}$
57		simpl1l	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to G \in CMnd$
58		simp2l	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to y \in Fin$
59		snfi	$⊢ \{z\} \in Fin$
60		unfi	$⊢ (y \in Fin \land \{z\} \in Fin) \to y \cup \{z\} \in Fin$
61	58 59 60	sylancl	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to y \cup \{z\} \in Fin$
62	61	adantr	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to y \cup \{z\} \in Fin$
63		elmapi	$⊢ w \in (B^{(y \cup \{z\})}) \to w : y \cup \{z\} ⟶ B$
64	63	adantl	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to w : y \cup \{z\} ⟶ B$
65		fvexd	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to 0_{G} \in V$
66	64 62 65	fdmfifsupp	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to {finSupp}_{0_{G}} (w)$
67		simpl2r	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to \neg z \in y$
68		disjsn	$⊢ y \cap \{z\} = \emptyset \leftrightarrow \neg z \in y$
69	67 68	sylibr	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to y \cap \{z\} = \emptyset$
70		eqidd	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to y \cup \{z\} = y \cup \{z\}$
71	2 37 56 57 62 64 66 69 70	gsumsplit	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to \sum_{G} w = (\sum_{G}, ({w ↾}_{y})) +_{G} (\sum_{G}, ({w ↾}_{\{z\}}))$
72	71	mpteq2dva	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (w \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} w) = (w \in (B^{(y \cup \{z\})}) ⟼ (\sum_{G}, ({w ↾}_{y})) +_{G} (\sum_{G}, ({w ↾}_{\{z\}})))$
73	55 72	syl5eq	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (x \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} x) = (w \in (B^{(y \cup \{z\})}) ⟼ (\sum_{G}, ({w ↾}_{y})) +_{G} (\sum_{G}, ({w ↾}_{\{z\}})))$
74		simp1r	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to G \in TopMnd$
75	74 42	syl	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to J \in TopOn (B)$
76		eqid	$⊢ \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) = \prod_{𝑡} ((y \cup \{z\}) \times \{J\})$
77	76	pttoponconst	$⊢ (y \cup \{z\} \in Fin \land J \in TopOn (B)) \to \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) \in TopOn (B^{(y \cup \{z\})})$
78	61 75 77	syl2anc	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) \in TopOn (B^{(y \cup \{z\})})$
79		toponuni	$⊢ \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) \in TopOn (B^{(y \cup \{z\})}) \to B^{(y \cup \{z\})} = ⋃ \prod_{𝑡} ((y \cup \{z\}) \times \{J\})$
80	78 79	syl	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to B^{(y \cup \{z\})} = ⋃ \prod_{𝑡} ((y \cup \{z\}) \times \{J\})$
81	80	mpteq1d	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (w \in (B^{(y \cup \{z\})}) ⟼ {w ↾}_{y}) = (w \in ⋃ \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) ⟼ {w ↾}_{y})$
82		topontop	$⊢ J \in TopOn (B) \to J \in Top$
83	74 42 82	3syl	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to J \in Top$
84		fconst6g	$⊢ J \in Top \to ((y \cup \{z\}) \times \{J\}) : y \cup \{z\} ⟶ Top$
85	83 84	syl	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to ((y \cup \{z\}) \times \{J\}) : y \cup \{z\} ⟶ Top$
86		ssun1	$⊢ y \subseteq y \cup \{z\}$
87	86	a1i	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to y \subseteq y \cup \{z\}$
88		eqid	$⊢ ⋃ \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) = ⋃ \prod_{𝑡} ((y \cup \{z\}) \times \{J\})$
89		xpssres	$⊢ y \subseteq y \cup \{z\} \to {((y \cup \{z\}) \times \{J\}) ↾}_{y} = y \times \{J\}$
90	86 89	ax-mp	$⊢ {((y \cup \{z\}) \times \{J\}) ↾}_{y} = y \times \{J\}$
91	90	eqcomi	$⊢ y \times \{J\} = {((y \cup \{z\}) \times \{J\}) ↾}_{y}$
92	91	fveq2i	$⊢ \prod_{𝑡} (y \times \{J\}) = \prod_{𝑡} ({((y \cup \{z\}) \times \{J\}) ↾}_{y})$
93	88 76 92	ptrescn	$⊢ (y \cup \{z\} \in Fin \land ((y \cup \{z\}) \times \{J\}) : y \cup \{z\} ⟶ Top \land y \subseteq y \cup \{z\}) \to (w \in ⋃ \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) ⟼ {w ↾}_{y}) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn \prod_{𝑡} (y \times \{J\}))$
94	61 85 87 93	syl3anc	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (w \in ⋃ \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) ⟼ {w ↾}_{y}) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn \prod_{𝑡} (y \times \{J\}))$
95	81 94	eqeltrd	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (w \in (B^{(y \cup \{z\})}) ⟼ {w ↾}_{y}) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn \prod_{𝑡} (y \times \{J\}))$
96		eqid	$⊢ \prod_{𝑡} (y \times \{J\}) = \prod_{𝑡} (y \times \{J\})$
97	96	pttoponconst	$⊢ (y \in Fin \land J \in TopOn (B)) \to \prod_{𝑡} (y \times \{J\}) \in TopOn (B^{y})$
98	58 75 97	syl2anc	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to \prod_{𝑡} (y \times \{J\}) \in TopOn (B^{y})$
99		simp3	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)$
100		oveq2	$⊢ x = {w ↾}_{y} \to \sum_{G} x = \sum_{G} ({w ↾}_{y})$
101	78 95 98 99 100	cnmpt11	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (w \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} ({w ↾}_{y})) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn J)$
102	64	feqmptd	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to w = (k \in (y \cup \{z\}) ⟼ w (k))$
103	102	reseq1d	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to {w ↾}_{\{z\}} = {(k \in (y \cup \{z\}) ⟼ w (k)) ↾}_{\{z\}}$
104		ssun2	$⊢ \{z\} \subseteq y \cup \{z\}$
105		resmpt	$⊢ \{z\} \subseteq y \cup \{z\} \to {(k \in (y \cup \{z\}) ⟼ w (k)) ↾}_{\{z\}} = (k \in \{z\} ⟼ w (k))$
106	104 105	ax-mp	$⊢ {(k \in (y \cup \{z\}) ⟼ w (k)) ↾}_{\{z\}} = (k \in \{z\} ⟼ w (k))$
107	103 106	eqtrdi	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to {w ↾}_{\{z\}} = (k \in \{z\} ⟼ w (k))$
108	107	oveq2d	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to \sum_{G} ({w ↾}_{\{z\}}) = \underset{k \in \{z\}}{\sum_{G}} w (k)$
109		cmnmnd	$⊢ G \in CMnd \to G \in Mnd$
110	57 109	syl	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to G \in Mnd$
111		vex	$⊢ z \in V$
112	111	a1i	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to z \in V$
113		vsnid	$⊢ z \in \{z\}$
114		elun2	$⊢ z \in \{z\} \to z \in (y \cup \{z\})$
115	113 114	mp1i	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to z \in (y \cup \{z\})$
116	64 115	ffvelrnd	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to w (z) \in B$
117		fveq2	$⊢ k = z \to w (k) = w (z)$
118	2 117	gsumsn	$⊢ (G \in Mnd \land z \in V \land w (z) \in B) \to \underset{k \in \{z\}}{\sum_{G}} w (k) = w (z)$
119	110 112 116 118	syl3anc	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to \underset{k \in \{z\}}{\sum_{G}} w (k) = w (z)$
120	108 119	eqtrd	$⊢ (((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \land w \in (B^{(y \cup \{z\})})) \to \sum_{G} ({w ↾}_{\{z\}}) = w (z)$
121	120	mpteq2dva	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (w \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} ({w ↾}_{\{z\}})) = (w \in (B^{(y \cup \{z\})}) ⟼ w (z))$
122	80	mpteq1d	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (w \in (B^{(y \cup \{z\})}) ⟼ w (z)) = (w \in ⋃ \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) ⟼ w (z))$
123	113 114	mp1i	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to z \in (y \cup \{z\})$
124	88 76	ptpjcn	$⊢ (y \cup \{z\} \in Fin \land ((y \cup \{z\}) \times \{J\}) : y \cup \{z\} ⟶ Top \land z \in (y \cup \{z\})) \to (w \in ⋃ \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) ⟼ w (z)) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn ((y \cup \{z\}) \times \{J\}) (z))$
125	61 85 123 124	syl3anc	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (w \in ⋃ \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) ⟼ w (z)) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn ((y \cup \{z\}) \times \{J\}) (z))$
126	122 125	eqeltrd	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (w \in (B^{(y \cup \{z\})}) ⟼ w (z)) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn ((y \cup \{z\}) \times \{J\}) (z))$
127		fvconst2g	$⊢ (J \in Top \land z \in (y \cup \{z\})) \to ((y \cup \{z\}) \times \{J\}) (z) = J$
128	83 123 127	syl2anc	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to ((y \cup \{z\}) \times \{J\}) (z) = J$
129	128	oveq2d	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn ((y \cup \{z\}) \times \{J\}) (z) = \prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn J$
130	126 129	eleqtrd	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (w \in (B^{(y \cup \{z\})}) ⟼ w (z)) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn J)$
131	121 130	eqeltrd	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (w \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} ({w ↾}_{\{z\}})) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn J)$
132	1 56 74 78 101 131	cnmpt1plusg	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (w \in (B^{(y \cup \{z\})}) ⟼ (\sum_{G}, ({w ↾}_{y})) +_{G} (\sum_{G}, ({w ↾}_{\{z\}}))) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn J)$
133	73 132	eqeltrd	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y) \land (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to (x \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} x) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn J)$
134	133	3expia	$⊢ ((G \in CMnd \land G \in TopMnd) \land (y \in Fin \land \neg z \in y)) \to ((x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J) \to (x \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} x) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn J))$
135	134	expcom	$⊢ (y \in Fin \land \neg z \in y) \to ((G \in CMnd \land G \in TopMnd) \to ((x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J) \to (x \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} x) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn J)))$
136	135	a2d	$⊢ (y \in Fin \land \neg z \in y) \to (((G \in CMnd \land G \in TopMnd) \to (x \in (B^{y}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (y \times \{J\}) Cn J)) \to ((G \in CMnd \land G \in TopMnd) \to (x \in (B^{(y \cup \{z\})}) ⟼ \sum_{G} x) \in (\prod_{𝑡} ((y \cup \{z\}) \times \{J\}) Cn J)))$
137	11 18 25 32 53 136	findcard2s	$⊢ A \in Fin \to ((G \in CMnd \land G \in TopMnd) \to (x \in (B^{A}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (A \times \{J\}) Cn J))$
138	137	com12	$⊢ (G \in CMnd \land G \in TopMnd) \to (A \in Fin \to (x \in (B^{A}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (A \times \{J\}) Cn J))$
139	138	3impia	$⊢ (G \in CMnd \land G \in TopMnd \land A \in Fin) \to (x \in (B^{A}) ⟼ \sum_{G} x) \in (\prod_{𝑡} (A \times \{J\}) Cn J)$
140	42 82	syl	$⊢ G \in TopMnd \to J \in Top$
141		xkopt	$⊢ (J \in Top \land A \in Fin) \to J^_{ko} 𝒫 A = \prod_{𝑡} (A \times \{J\})$
142	140 141	sylan	$⊢ (G \in TopMnd \land A \in Fin) \to J^_{ko} 𝒫 A = \prod_{𝑡} (A \times \{J\})$
143	142	3adant1	$⊢ (G \in CMnd \land G \in TopMnd \land A \in Fin) \to J^_{ko} 𝒫 A = \prod_{𝑡} (A \times \{J\})$
144	143	oveq1d	$⊢ (G \in CMnd \land G \in TopMnd \land A \in Fin) \to (J^_{ko} 𝒫 A) Cn J = \prod_{𝑡} (A \times \{J\}) Cn J$
145	139 144	eleqtrrd	$⊢ (G \in CMnd \land G \in TopMnd \land A \in Fin) \to (x \in (B^{A}) ⟼ \sum_{G} x) \in ((J^_{ko} 𝒫 A) Cn J)$

Metamath Proof Explorer

Theorem tmdgsum

Proof