Metamath Proof Explorer


Theorem 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 𝐽 = ( TopOpen ‘ 𝐺 )
tmdgsum.b 𝐵 = ( Base ‘ 𝐺 )
Assertion tmdgsum ( ( 𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin ) → ( 𝑥 ∈ ( 𝐵m 𝐴 ) ↦ ( 𝐺 Σg 𝑥 ) ) ∈ ( ( 𝐽ko 𝒫 𝐴 ) Cn 𝐽 ) )

Proof

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