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 eqtrid ⊢ ( ( ( 𝐺 ∈ 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 ffvelcdmd ⊢ ( ( ( ( 𝐺 ∈ 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 𝐽 ) )