Theorem tmdgsum 22686

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 𝐴 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.)

Hypotheses

Ref	Expression
tmdgsum.j	⊢ 𝐽 = (TopOpen‘𝐺)
tmdgsum.b	⊢ 𝐵 = (Base‘𝐺)

Assertion

Ref	Expression
tmdgsum	⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐽   𝑥,𝐵   𝑥,𝐺

Proof of Theorem tmdgsum

Dummy variables 𝑘 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7150	. . . . . . . 8 ⊢ (𝑤 = ∅ → (𝐵 ↑m 𝑤) = (𝐵 ↑m ∅))
2	1	mpteq1d 5141	. . . . . . 7 ⊢ (𝑤 = ∅ → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑m ∅) ↦ (𝐺 Σg 𝑥)))
3		xpeq1 5555	. . . . . . . . . 10 ⊢ (𝑤 = ∅ → (𝑤 × {𝐽}) = (∅ × {𝐽}))
4		0xp 5635	. . . . . . . . . 10 ⊢ (∅ × {𝐽}) = ∅
5	3, 4	syl6eq 2872	. . . . . . . . 9 ⊢ (𝑤 = ∅ → (𝑤 × {𝐽}) = ∅)
6	5	fveq2d 6660	. . . . . . . 8 ⊢ (𝑤 = ∅ → (∏t‘(𝑤 × {𝐽})) = (∏t‘∅))
7	6	oveq1d 7157	. . . . . . 7 ⊢ (𝑤 = ∅ → ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) = ((∏t‘∅) Cn 𝐽))
8	2, 7	eleq12d 2907	. . . . . 6 ⊢ (𝑤 = ∅ → ((𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) ↔ (𝑥 ∈ (𝐵 ↑m ∅) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘∅) Cn 𝐽)))
9	8	imbi2d 343	. . . . 5 ⊢ (𝑤 = ∅ → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑤 × {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m ∅) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘∅) Cn 𝐽))))
10		oveq2 7150	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → (𝐵 ↑m 𝑤) = (𝐵 ↑m 𝑦))
11	10	mpteq1d 5141	. . . . . . 7 ⊢ (𝑤 = 𝑦 → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)))
12		xpeq1 5555	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → (𝑤 × {𝐽}) = (𝑦 × {𝐽}))
13	12	fveq2d 6660	. . . . . . . 8 ⊢ (𝑤 = 𝑦 → (∏t‘(𝑤 × {𝐽})) = (∏t‘(𝑦 × {𝐽})))
14	13	oveq1d 7157	. . . . . . 7 ⊢ (𝑤 = 𝑦 → ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) = ((∏t‘(𝑦 × {𝐽})) Cn 𝐽))
15	11, 14	eleq12d 2907	. . . . . 6 ⊢ (𝑤 = 𝑦 → ((𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) ↔ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)))
16	15	imbi2d 343	. . . . 5 ⊢ (𝑤 = 𝑦 → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑤 × {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽))))
17		oveq2 7150	. . . . . . . 8 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝐵 ↑m 𝑤) = (𝐵 ↑m (𝑦 ∪ {𝑧})))
18	17	mpteq1d 5141	. . . . . . 7 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)))
19		xpeq1 5555	. . . . . . . . 9 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑤 × {𝐽}) = ((𝑦 ∪ {𝑧}) × {𝐽}))
20	19	fveq2d 6660	. . . . . . . 8 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∏t‘(𝑤 × {𝐽})) = (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})))
21	20	oveq1d 7157	. . . . . . 7 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) = ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))
22	18, 21	eleq12d 2907	. . . . . 6 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) ↔ (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)))
23	22	imbi2d 343	. . . . 5 ⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑤 × {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))))
24		oveq2 7150	. . . . . . . 8 ⊢ (𝑤 = 𝐴 → (𝐵 ↑m 𝑤) = (𝐵 ↑m 𝐴))
25	24	mpteq1d 5141	. . . . . . 7 ⊢ (𝑤 = 𝐴 → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)))
26		xpeq1 5555	. . . . . . . . 9 ⊢ (𝑤 = 𝐴 → (𝑤 × {𝐽}) = (𝐴 × {𝐽}))
27	26	fveq2d 6660	. . . . . . . 8 ⊢ (𝑤 = 𝐴 → (∏t‘(𝑤 × {𝐽})) = (∏t‘(𝐴 × {𝐽})))
28	27	oveq1d 7157	. . . . . . 7 ⊢ (𝑤 = 𝐴 → ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) = ((∏t‘(𝐴 × {𝐽})) Cn 𝐽))
29	25, 28	eleq12d 2907	. . . . . 6 ⊢ (𝑤 = 𝐴 → ((𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) ↔ (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝐴 × {𝐽})) Cn 𝐽)))
30	29	imbi2d 343	. . . . 5 ⊢ (𝑤 = 𝐴 → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝑤) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑤 × {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝐴 × {𝐽})) Cn 𝐽))))
31		elmapfn 8415	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐵 ↑m ∅) → 𝑥 Fn ∅)
32		fn0 6465	. . . . . . . . . 10 ⊢ (𝑥 Fn ∅ ↔ 𝑥 = ∅)
33	31, 32	sylib 220	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐵 ↑m ∅) → 𝑥 = ∅)
34	33	oveq2d 7158	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐵 ↑m ∅) → (𝐺 Σg 𝑥) = (𝐺 Σg ∅))
35		eqid 2821	. . . . . . . . 9 ⊢ (0g‘𝐺) = (0g‘𝐺)
36	35	gsum0 17877	. . . . . . . 8 ⊢ (𝐺 Σg ∅) = (0g‘𝐺)
37	34, 36	syl6eq 2872	. . . . . . 7 ⊢ (𝑥 ∈ (𝐵 ↑m ∅) → (𝐺 Σg 𝑥) = (0g‘𝐺))
38	37	mpteq2ia 5143	. . . . . 6 ⊢ (𝑥 ∈ (𝐵 ↑m ∅) ↦ (𝐺 Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑m ∅) ↦ (0g‘𝐺))
39		0ex 5197	. . . . . . . 8 ⊢ ∅ ∈ V
40		tmdgsum.j	. . . . . . . . . 10 ⊢ 𝐽 = (TopOpen‘𝐺)
41		tmdgsum.b	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝐺)
42	40, 41	tmdtopon 22672	. . . . . . . . 9 ⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵))
43	42	adantl 484	. . . . . . . 8 ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → 𝐽 ∈ (TopOn‘𝐵))
44	4	fveq2i 6659	. . . . . . . . . 10 ⊢ (∏t‘(∅ × {𝐽})) = (∏t‘∅)
45	44	eqcomi 2830	. . . . . . . . 9 ⊢ (∏t‘∅) = (∏t‘(∅ × {𝐽}))
46	45	pttoponconst 22188	. . . . . . . 8 ⊢ ((∅ ∈ V ∧ 𝐽 ∈ (TopOn‘𝐵)) → (∏t‘∅) ∈ (TopOn‘(𝐵 ↑m ∅)))
47	39, 43, 46	sylancr 589	. . . . . . 7 ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (∏t‘∅) ∈ (TopOn‘(𝐵 ↑m ∅)))
48		tmdmnd 22666	. . . . . . . . 9 ⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd)
49	48	adantl 484	. . . . . . . 8 ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → 𝐺 ∈ Mnd)
50	41, 35	mndidcl 17909	. . . . . . . 8 ⊢ (𝐺 ∈ Mnd → (0g‘𝐺) ∈ 𝐵)
51	49, 50	syl 17	. . . . . . 7 ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (0g‘𝐺) ∈ 𝐵)
52	47, 43, 51	cnmptc 22253	. . . . . 6 ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m ∅) ↦ (0g‘𝐺)) ∈ ((∏t‘∅) Cn 𝐽))
53	38, 52	eqeltrid 2917	. . . . 5 ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m ∅) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘∅) Cn 𝐽))
54		oveq2 7150	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑤 → (𝐺 Σg 𝑥) = (𝐺 Σg 𝑤))
55	54	cbvmptv 5155	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) = (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑤))
56		eqid 2821	. . . . . . . . . . . 12 ⊢ (+g‘𝐺) = (+g‘𝐺)
57		simpl1l 1220	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝐺 ∈ CMnd)
58		simp2l 1195	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝑦 ∈ Fin)
59		snfi 8580	. . . . . . . . . . . . . 14 ⊢ {𝑧} ∈ Fin
60		unfi 8771	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin)
61	58, 59, 60	sylancl 588	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑦 ∪ {𝑧}) ∈ Fin)
62	61	adantr 483	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝑦 ∪ {𝑧}) ∈ Fin)
63		elmapi 8414	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) → 𝑤:(𝑦 ∪ {𝑧})⟶𝐵)
64	63	adantl 484	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝑤:(𝑦 ∪ {𝑧})⟶𝐵)
65		fvexd 6671	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (0g‘𝐺) ∈ V)
66	64, 62, 65	fdmfifsupp 8829	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝑤 finSupp (0g‘𝐺))
67		simpl2r 1223	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → ¬ 𝑧 ∈ 𝑦)
68		disjsn 4633	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦)
69	67, 68	sylibr 236	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝑦 ∩ {𝑧}) = ∅)
70		eqidd 2822	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧}))
71	41, 35, 56, 57, 62, 64, 66, 69, 70	gsumsplit 19031	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝐺 Σg 𝑤) = ((𝐺 Σg (𝑤 ↾ 𝑦))(+g‘𝐺)(𝐺 Σg (𝑤 ↾ {𝑧}))))
72	71	mpteq2dva 5147	. . . . . . . . . 10 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑤)) = (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ ((𝐺 Σg (𝑤 ↾ 𝑦))(+g‘𝐺)(𝐺 Σg (𝑤 ↾ {𝑧})))))
73	55, 72	syl5eq 2868	. . . . . . . . 9 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) = (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ ((𝐺 Σg (𝑤 ↾ 𝑦))(+g‘𝐺)(𝐺 Σg (𝑤 ↾ {𝑧})))))
74		simp1r 1194	. . . . . . . . . 10 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝐺 ∈ TopMnd)
75	74, 42	syl 17	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝐽 ∈ (TopOn‘𝐵))
76		eqid 2821	. . . . . . . . . . . 12 ⊢ (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) = (∏t‘((𝑦 ∪ {𝑧}) × {𝐽}))
77	76	pttoponconst 22188	. . . . . . . . . . 11 ⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝐽 ∈ (TopOn‘𝐵)) → (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ∈ (TopOn‘(𝐵 ↑m (𝑦 ∪ {𝑧}))))
78	61, 75, 77	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ∈ (TopOn‘(𝐵 ↑m (𝑦 ∪ {𝑧}))))
79		toponuni 21505	. . . . . . . . . . . . . 14 ⊢ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ∈ (TopOn‘(𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝐵 ↑m (𝑦 ∪ {𝑧})) = ∪ (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})))
80	78, 79	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝐵 ↑m (𝑦 ∪ {𝑧})) = ∪ (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})))
81	80	mpteq1d 5141	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝑤 ↾ 𝑦)) = (𝑤 ∈ ∪ (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤 ↾ 𝑦)))
82		topontop 21504	. . . . . . . . . . . . . . 15 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
83	74, 42, 82	3syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝐽 ∈ Top)
84		fconst6g 6554	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ Top → ((𝑦 ∪ {𝑧}) × {𝐽}):(𝑦 ∪ {𝑧})⟶Top)
85	83, 84	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → ((𝑦 ∪ {𝑧}) × {𝐽}):(𝑦 ∪ {𝑧})⟶Top)
86		ssun1 4136	. . . . . . . . . . . . . 14 ⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧})
87	86	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝑦 ⊆ (𝑦 ∪ {𝑧}))
88		eqid 2821	. . . . . . . . . . . . . 14 ⊢ ∪ (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) = ∪ (∏t‘((𝑦 ∪ {𝑧}) × {𝐽}))
89		xpssres 5875	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (((𝑦 ∪ {𝑧}) × {𝐽}) ↾ 𝑦) = (𝑦 × {𝐽}))
90	86, 89	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∪ {𝑧}) × {𝐽}) ↾ 𝑦) = (𝑦 × {𝐽})
91	90	eqcomi 2830	. . . . . . . . . . . . . . 15 ⊢ (𝑦 × {𝐽}) = (((𝑦 ∪ {𝑧}) × {𝐽}) ↾ 𝑦)
92	91	fveq2i 6659	. . . . . . . . . . . . . 14 ⊢ (∏t‘(𝑦 × {𝐽})) = (∏t‘(((𝑦 ∪ {𝑧}) × {𝐽}) ↾ 𝑦))
93	88, 76, 92	ptrescn 22230	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ ((𝑦 ∪ {𝑧}) × {𝐽}):(𝑦 ∪ {𝑧})⟶Top ∧ 𝑦 ⊆ (𝑦 ∪ {𝑧})) → (𝑤 ∈ ∪ (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤 ↾ 𝑦)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (∏t‘(𝑦 × {𝐽}))))
94	61, 85, 87, 93	syl3anc 1367	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ ∪ (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤 ↾ 𝑦)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (∏t‘(𝑦 × {𝐽}))))
95	81, 94	eqeltrd 2913	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝑤 ↾ 𝑦)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (∏t‘(𝑦 × {𝐽}))))
96		eqid 2821	. . . . . . . . . . . . 13 ⊢ (∏t‘(𝑦 × {𝐽})) = (∏t‘(𝑦 × {𝐽}))
97	96	pttoponconst 22188	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ Fin ∧ 𝐽 ∈ (TopOn‘𝐵)) → (∏t‘(𝑦 × {𝐽})) ∈ (TopOn‘(𝐵 ↑m 𝑦)))
98	58, 75, 97	syl2anc 586	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (∏t‘(𝑦 × {𝐽})) ∈ (TopOn‘(𝐵 ↑m 𝑦)))
99		simp3 1134	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽))
100		oveq2 7150	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑤 ↾ 𝑦) → (𝐺 Σg 𝑥) = (𝐺 Σg (𝑤 ↾ 𝑦)))
101	78, 95, 98, 99, 100	cnmpt11 22254	. . . . . . . . . 10 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg (𝑤 ↾ 𝑦))) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))
102	64	feqmptd 6719	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝑤 = (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ (𝑤‘𝑘)))
103	102	reseq1d 5838	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝑤 ↾ {𝑧}) = ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ (𝑤‘𝑘)) ↾ {𝑧}))
104		ssun2 4137	. . . . . . . . . . . . . . . 16 ⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧})
105		resmpt 5891	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ (𝑤‘𝑘)) ↾ {𝑧}) = (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘)))
106	104, 105	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ (𝑤‘𝑘)) ↾ {𝑧}) = (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘))
107	103, 106	syl6eq 2872	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝑤 ↾ {𝑧}) = (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘)))
108	107	oveq2d 7158	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝐺 Σg (𝑤 ↾ {𝑧})) = (𝐺 Σg (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘))))
109		cmnmnd 18905	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd)
110	57, 109	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝐺 ∈ Mnd)
111		vex 3489	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
112	111	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝑧 ∈ V)
113		vsnid 4588	. . . . . . . . . . . . . . . 16 ⊢ 𝑧 ∈ {𝑧}
114		elun2 4141	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ {𝑧} → 𝑧 ∈ (𝑦 ∪ {𝑧}))
115	113, 114	mp1i 13	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → 𝑧 ∈ (𝑦 ∪ {𝑧}))
116	64, 115	ffvelrnd 6838	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝑤‘𝑧) ∈ 𝐵)
117		fveq2 6656	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑧 → (𝑤‘𝑘) = (𝑤‘𝑧))
118	41, 117	gsumsn 19057	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Mnd ∧ 𝑧 ∈ V ∧ (𝑤‘𝑧) ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘))) = (𝑤‘𝑧))
119	110, 112, 116, 118	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝐺 Σg (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘))) = (𝑤‘𝑧))
120	108, 119	eqtrd 2856	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧}))) → (𝐺 Σg (𝑤 ↾ {𝑧})) = (𝑤‘𝑧))
121	120	mpteq2dva 5147	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg (𝑤 ↾ {𝑧}))) = (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝑤‘𝑧)))
122	80	mpteq1d 5141	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝑤‘𝑧)) = (𝑤 ∈ ∪ (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤‘𝑧)))
123	113, 114	mp1i 13	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝑧 ∈ (𝑦 ∪ {𝑧}))
124	88, 76	ptpjcn 22202	. . . . . . . . . . . . . 14 ⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ ((𝑦 ∪ {𝑧}) × {𝐽}):(𝑦 ∪ {𝑧})⟶Top ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})) → (𝑤 ∈ ∪ (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤‘𝑧)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧)))
125	61, 85, 123, 124	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ ∪ (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤‘𝑧)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧)))
126	122, 125	eqeltrd 2913	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝑤‘𝑧)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧)))
127		fvconst2g 6950	. . . . . . . . . . . . . 14 ⊢ ((𝐽 ∈ Top ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})) → (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧) = 𝐽)
128	83, 123, 127	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧) = 𝐽)
129	128	oveq2d 7158	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧)) = ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))
130	126, 129	eleqtrd 2915	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝑤‘𝑧)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))
131	121, 130	eqeltrd 2913	. . . . . . . . . 10 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg (𝑤 ↾ {𝑧}))) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))
132	40, 56, 74, 78, 101, 131	cnmpt1plusg 22678	. . . . . . . . 9 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ ((𝐺 Σg (𝑤 ↾ 𝑦))(+g‘𝐺)(𝐺 Σg (𝑤 ↾ {𝑧})))) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))
133	73, 132	eqeltrd 2913	. . . . . . . 8 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))
134	133	3expia 1117	. . . . . . 7 ⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽) → (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)))
135	134	expcom 416	. . . . . 6 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → ((𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽) → (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))))
136	135	a2d 29	. . . . 5 ⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝑦) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))))
137	9, 16, 23, 30, 53, 136	findcard2s 8745	. . . 4 ⊢ (𝐴 ∈ Fin → ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝐴 × {𝐽})) Cn 𝐽)))
138	137	com12 32	. . 3 ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝐴 ∈ Fin → (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝐴 × {𝐽})) Cn 𝐽)))
139	138	3impia 1113	. 2 ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈ ((∏t‘(𝐴 × {𝐽})) Cn 𝐽))
140	42, 82	syl 17	. . . . 5 ⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ Top)
141		xkopt 22246	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin) → (𝐽 ↑ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝐽})))
142	140, 141	sylan 582	. . . 4 ⊢ ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝐽 ↑ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝐽})))
143	142	3adant1 1126	. . 3 ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝐽 ↑ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝐽})))
144	143	oveq1d 7157	. 2 ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽) = ((∏t‘(𝐴 × {𝐽})) Cn 𝐽))
145	139, 144	eleqtrrd 2916	1 ⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝑥 ∈ (𝐵 ↑m 𝐴) ↦ (𝐺 Σg 𝑥)) ∈ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  Vcvv 3486   ∪ cun 3922   ∩ cin 3923   ⊆ wss 3924  ∅c0 4279  𝒫 cpw 4525  {csn 4553  ∪ cuni 4824   ↦ cmpt 5132   × cxp 5539   ↾ cres 5543   Fn wfn 6336  ⟶wf 6337  ‘cfv 6341  (class class class)co 7142   ↑_m cmap 8392  Fincfn 8495  Basecbs 16466  +_gcplusg 16548  TopOpenctopn 16678  ∏_tcpt 16695  0_gc0g 16696   Σ_g cgsu 16697  Mndcmnd 17894  CMndccmn 18889  Topctop 21484  TopOnctopon 21501   Cn ccn 21815   ↑_ko cxko 22152  TopMndctmd 22661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-cnex 10579  ax-resscn 10580  ax-1cn 10581  ax-icn 10582  ax-addcl 10583  ax-addrcl 10584  ax-mulcl 10585  ax-mulrcl 10586  ax-mulcom 10587  ax-addass 10588  ax-mulass 10589  ax-distr 10590  ax-i2m1 10591  ax-1ne0 10592  ax-1rid 10593  ax-rnegex 10594  ax-rrecex 10595  ax-cnre 10596  ax-pre-lttri 10597  ax-pre-lttrn 10598  ax-pre-ltadd 10599  ax-pre-mulgt0 10600

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-pss 3942  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-tp 4558  df-op 4560  df-uni 4825  df-int 4863  df-iun 4907  df-iin 4908  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5446  df-eprel 5451  df-po 5460  df-so 5461  df-fr 5500  df-se 5501  df-we 5502  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-pred 6134  df-ord 6180  df-on 6181  df-lim 6182  df-suc 6183  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-isom 6350  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-of 7395  df-om 7567  df-1st 7675  df-2nd 7676  df-supp 7817  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-2o 8089  df-oadd 8092  df-er 8275  df-map 8394  df-ixp 8448  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-fsupp 8820  df-fi 8861  df-oi 8960  df-card 9354  df-pnf 10663  df-mnf 10664  df-xr 10665  df-ltxr 10666  df-le 10667  df-sub 10858  df-neg 10859  df-nn 11625  df-2 11687  df-n0 11885  df-z 11969  df-uz 12231  df-fz 12883  df-fzo 13024  df-seq 13360  df-hash 13681  df-ndx 16469  df-slot 16470  df-base 16472  df-sets 16473  df-ress 16474  df-plusg 16561  df-rest 16679  df-0g 16698  df-gsum 16699  df-topgen 16700  df-pt 16701  df-mre 16840  df-mrc 16841  df-acs 16843  df-plusf 17834  df-mgm 17835  df-sgrp 17884  df-mnd 17895  df-submnd 17940  df-mulg 18208  df-cntz 18430  df-cmn 18891  df-top 21485  df-topon 21502  df-topsp 21524  df-bases 21537  df-cn 21818  df-cnp 21819  df-cmp 21978  df-tx 22153  df-xko 22154  df-tmd 22663

This theorem is referenced by:  tmdgsum2  22687