MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tmdgsum Structured version   Visualization version   GIF version

Theorem tmdgsum 23819
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.
StepHypRef Expression
1 oveq2 7419 . . . . . . . 8 (𝑀 = βˆ… β†’ (𝐡 ↑m 𝑀) = (𝐡 ↑m βˆ…))
21mpteq1d 5242 . . . . . . 7 (𝑀 = βˆ… β†’ (π‘₯ ∈ (𝐡 ↑m 𝑀) ↦ (𝐺 Ξ£g π‘₯)) = (π‘₯ ∈ (𝐡 ↑m βˆ…) ↦ (𝐺 Ξ£g π‘₯)))
3 xpeq1 5689 . . . . . . . . . 10 (𝑀 = βˆ… β†’ (𝑀 Γ— {𝐽}) = (βˆ… Γ— {𝐽}))
4 0xp 5773 . . . . . . . . . 10 (βˆ… Γ— {𝐽}) = βˆ…
53, 4eqtrdi 2786 . . . . . . . . 9 (𝑀 = βˆ… β†’ (𝑀 Γ— {𝐽}) = βˆ…)
65fveq2d 6894 . . . . . . . 8 (𝑀 = βˆ… β†’ (∏tβ€˜(𝑀 Γ— {𝐽})) = (∏tβ€˜βˆ…))
76oveq1d 7426 . . . . . . 7 (𝑀 = βˆ… β†’ ((∏tβ€˜(𝑀 Γ— {𝐽})) Cn 𝐽) = ((∏tβ€˜βˆ…) Cn 𝐽))
82, 7eleq12d 2825 . . . . . 6 (𝑀 = βˆ… β†’ ((π‘₯ ∈ (𝐡 ↑m 𝑀) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑀 Γ— {𝐽})) Cn 𝐽) ↔ (π‘₯ ∈ (𝐡 ↑m βˆ…) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜βˆ…) Cn 𝐽)))
98imbi2d 339 . . . . 5 (𝑀 = βˆ… β†’ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (π‘₯ ∈ (𝐡 ↑m 𝑀) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑀 Γ— {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (π‘₯ ∈ (𝐡 ↑m βˆ…) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜βˆ…) Cn 𝐽))))
10 oveq2 7419 . . . . . . . 8 (𝑀 = 𝑦 β†’ (𝐡 ↑m 𝑀) = (𝐡 ↑m 𝑦))
1110mpteq1d 5242 . . . . . . 7 (𝑀 = 𝑦 β†’ (π‘₯ ∈ (𝐡 ↑m 𝑀) ↦ (𝐺 Ξ£g π‘₯)) = (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)))
12 xpeq1 5689 . . . . . . . . 9 (𝑀 = 𝑦 β†’ (𝑀 Γ— {𝐽}) = (𝑦 Γ— {𝐽}))
1312fveq2d 6894 . . . . . . . 8 (𝑀 = 𝑦 β†’ (∏tβ€˜(𝑀 Γ— {𝐽})) = (∏tβ€˜(𝑦 Γ— {𝐽})))
1413oveq1d 7426 . . . . . . 7 (𝑀 = 𝑦 β†’ ((∏tβ€˜(𝑀 Γ— {𝐽})) Cn 𝐽) = ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽))
1511, 14eleq12d 2825 . . . . . 6 (𝑀 = 𝑦 β†’ ((π‘₯ ∈ (𝐡 ↑m 𝑀) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑀 Γ— {𝐽})) Cn 𝐽) ↔ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)))
1615imbi2d 339 . . . . 5 (𝑀 = 𝑦 β†’ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (π‘₯ ∈ (𝐡 ↑m 𝑀) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑀 Γ— {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽))))
17 oveq2 7419 . . . . . . . 8 (𝑀 = (𝑦 βˆͺ {𝑧}) β†’ (𝐡 ↑m 𝑀) = (𝐡 ↑m (𝑦 βˆͺ {𝑧})))
1817mpteq1d 5242 . . . . . . 7 (𝑀 = (𝑦 βˆͺ {𝑧}) β†’ (π‘₯ ∈ (𝐡 ↑m 𝑀) ↦ (𝐺 Ξ£g π‘₯)) = (π‘₯ ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g π‘₯)))
19 xpeq1 5689 . . . . . . . . 9 (𝑀 = (𝑦 βˆͺ {𝑧}) β†’ (𝑀 Γ— {𝐽}) = ((𝑦 βˆͺ {𝑧}) Γ— {𝐽}))
2019fveq2d 6894 . . . . . . . 8 (𝑀 = (𝑦 βˆͺ {𝑧}) β†’ (∏tβ€˜(𝑀 Γ— {𝐽})) = (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})))
2120oveq1d 7426 . . . . . . 7 (𝑀 = (𝑦 βˆͺ {𝑧}) β†’ ((∏tβ€˜(𝑀 Γ— {𝐽})) Cn 𝐽) = ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn 𝐽))
2218, 21eleq12d 2825 . . . . . 6 (𝑀 = (𝑦 βˆͺ {𝑧}) β†’ ((π‘₯ ∈ (𝐡 ↑m 𝑀) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑀 Γ— {𝐽})) Cn 𝐽) ↔ (π‘₯ ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn 𝐽)))
2322imbi2d 339 . . . . 5 (𝑀 = (𝑦 βˆͺ {𝑧}) β†’ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (π‘₯ ∈ (𝐡 ↑m 𝑀) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑀 Γ— {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (π‘₯ ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn 𝐽))))
24 oveq2 7419 . . . . . . . 8 (𝑀 = 𝐴 β†’ (𝐡 ↑m 𝑀) = (𝐡 ↑m 𝐴))
2524mpteq1d 5242 . . . . . . 7 (𝑀 = 𝐴 β†’ (π‘₯ ∈ (𝐡 ↑m 𝑀) ↦ (𝐺 Ξ£g π‘₯)) = (π‘₯ ∈ (𝐡 ↑m 𝐴) ↦ (𝐺 Ξ£g π‘₯)))
26 xpeq1 5689 . . . . . . . . 9 (𝑀 = 𝐴 β†’ (𝑀 Γ— {𝐽}) = (𝐴 Γ— {𝐽}))
2726fveq2d 6894 . . . . . . . 8 (𝑀 = 𝐴 β†’ (∏tβ€˜(𝑀 Γ— {𝐽})) = (∏tβ€˜(𝐴 Γ— {𝐽})))
2827oveq1d 7426 . . . . . . 7 (𝑀 = 𝐴 β†’ ((∏tβ€˜(𝑀 Γ— {𝐽})) Cn 𝐽) = ((∏tβ€˜(𝐴 Γ— {𝐽})) Cn 𝐽))
2925, 28eleq12d 2825 . . . . . 6 (𝑀 = 𝐴 β†’ ((π‘₯ ∈ (𝐡 ↑m 𝑀) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑀 Γ— {𝐽})) Cn 𝐽) ↔ (π‘₯ ∈ (𝐡 ↑m 𝐴) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝐴 Γ— {𝐽})) Cn 𝐽)))
3029imbi2d 339 . . . . 5 (𝑀 = 𝐴 β†’ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (π‘₯ ∈ (𝐡 ↑m 𝑀) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑀 Γ— {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (π‘₯ ∈ (𝐡 ↑m 𝐴) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝐴 Γ— {𝐽})) Cn 𝐽))))
31 elmapfn 8861 . . . . . . . . . 10 (π‘₯ ∈ (𝐡 ↑m βˆ…) β†’ π‘₯ Fn βˆ…)
32 fn0 6680 . . . . . . . . . 10 (π‘₯ Fn βˆ… ↔ π‘₯ = βˆ…)
3331, 32sylib 217 . . . . . . . . 9 (π‘₯ ∈ (𝐡 ↑m βˆ…) β†’ π‘₯ = βˆ…)
3433oveq2d 7427 . . . . . . . 8 (π‘₯ ∈ (𝐡 ↑m βˆ…) β†’ (𝐺 Ξ£g π‘₯) = (𝐺 Ξ£g βˆ…))
35 eqid 2730 . . . . . . . . 9 (0gβ€˜πΊ) = (0gβ€˜πΊ)
3635gsum0 18609 . . . . . . . 8 (𝐺 Ξ£g βˆ…) = (0gβ€˜πΊ)
3734, 36eqtrdi 2786 . . . . . . 7 (π‘₯ ∈ (𝐡 ↑m βˆ…) β†’ (𝐺 Ξ£g π‘₯) = (0gβ€˜πΊ))
3837mpteq2ia 5250 . . . . . 6 (π‘₯ ∈ (𝐡 ↑m βˆ…) ↦ (𝐺 Ξ£g π‘₯)) = (π‘₯ ∈ (𝐡 ↑m βˆ…) ↦ (0gβ€˜πΊ))
39 0ex 5306 . . . . . . . 8 βˆ… ∈ V
40 tmdgsum.j . . . . . . . . . 10 𝐽 = (TopOpenβ€˜πΊ)
41 tmdgsum.b . . . . . . . . . 10 𝐡 = (Baseβ€˜πΊ)
4240, 41tmdtopon 23805 . . . . . . . . 9 (𝐺 ∈ TopMnd β†’ 𝐽 ∈ (TopOnβ€˜π΅))
4342adantl 480 . . . . . . . 8 ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ 𝐽 ∈ (TopOnβ€˜π΅))
444fveq2i 6893 . . . . . . . . . 10 (∏tβ€˜(βˆ… Γ— {𝐽})) = (∏tβ€˜βˆ…)
4544eqcomi 2739 . . . . . . . . 9 (∏tβ€˜βˆ…) = (∏tβ€˜(βˆ… Γ— {𝐽}))
4645pttoponconst 23321 . . . . . . . 8 ((βˆ… ∈ V ∧ 𝐽 ∈ (TopOnβ€˜π΅)) β†’ (∏tβ€˜βˆ…) ∈ (TopOnβ€˜(𝐡 ↑m βˆ…)))
4739, 43, 46sylancr 585 . . . . . . 7 ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (∏tβ€˜βˆ…) ∈ (TopOnβ€˜(𝐡 ↑m βˆ…)))
48 tmdmnd 23799 . . . . . . . . 9 (𝐺 ∈ TopMnd β†’ 𝐺 ∈ Mnd)
4948adantl 480 . . . . . . . 8 ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ 𝐺 ∈ Mnd)
5041, 35mndidcl 18674 . . . . . . . 8 (𝐺 ∈ Mnd β†’ (0gβ€˜πΊ) ∈ 𝐡)
5149, 50syl 17 . . . . . . 7 ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (0gβ€˜πΊ) ∈ 𝐡)
5247, 43, 51cnmptc 23386 . . . . . 6 ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (π‘₯ ∈ (𝐡 ↑m βˆ…) ↦ (0gβ€˜πΊ)) ∈ ((∏tβ€˜βˆ…) Cn 𝐽))
5338, 52eqeltrid 2835 . . . . 5 ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (π‘₯ ∈ (𝐡 ↑m βˆ…) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜βˆ…) Cn 𝐽))
54 oveq2 7419 . . . . . . . . . . 11 (π‘₯ = 𝑀 β†’ (𝐺 Ξ£g π‘₯) = (𝐺 Ξ£g 𝑀))
5554cbvmptv 5260 . . . . . . . . . 10 (π‘₯ ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g π‘₯)) = (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g 𝑀))
56 eqid 2730 . . . . . . . . . . . 12 (+gβ€˜πΊ) = (+gβ€˜πΊ)
57 simpl1l 1222 . . . . . . . . . . . 12 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ 𝐺 ∈ CMnd)
58 simp2l 1197 . . . . . . . . . . . . . 14 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ 𝑦 ∈ Fin)
59 snfi 9046 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
60 unfi 9174 . . . . . . . . . . . . . 14 ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) β†’ (𝑦 βˆͺ {𝑧}) ∈ Fin)
6158, 59, 60sylancl 584 . . . . . . . . . . . . 13 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝑦 βˆͺ {𝑧}) ∈ Fin)
6261adantr 479 . . . . . . . . . . . 12 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ (𝑦 βˆͺ {𝑧}) ∈ Fin)
63 elmapi 8845 . . . . . . . . . . . . 13 (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) β†’ 𝑀:(𝑦 βˆͺ {𝑧})⟢𝐡)
6463adantl 480 . . . . . . . . . . . 12 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ 𝑀:(𝑦 βˆͺ {𝑧})⟢𝐡)
65 fvexd 6905 . . . . . . . . . . . . 13 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ (0gβ€˜πΊ) ∈ V)
6664, 62, 65fdmfifsupp 9375 . . . . . . . . . . . 12 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ 𝑀 finSupp (0gβ€˜πΊ))
67 simpl2r 1225 . . . . . . . . . . . . 13 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ Β¬ 𝑧 ∈ 𝑦)
68 disjsn 4714 . . . . . . . . . . . . 13 ((𝑦 ∩ {𝑧}) = βˆ… ↔ Β¬ 𝑧 ∈ 𝑦)
6967, 68sylibr 233 . . . . . . . . . . . 12 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ (𝑦 ∩ {𝑧}) = βˆ…)
70 eqidd 2731 . . . . . . . . . . . 12 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ (𝑦 βˆͺ {𝑧}) = (𝑦 βˆͺ {𝑧}))
7141, 35, 56, 57, 62, 64, 66, 69, 70gsumsplit 19837 . . . . . . . . . . 11 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ (𝐺 Ξ£g 𝑀) = ((𝐺 Ξ£g (𝑀 β†Ύ 𝑦))(+gβ€˜πΊ)(𝐺 Ξ£g (𝑀 β†Ύ {𝑧}))))
7271mpteq2dva 5247 . . . . . . . . . 10 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g 𝑀)) = (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ ((𝐺 Ξ£g (𝑀 β†Ύ 𝑦))(+gβ€˜πΊ)(𝐺 Ξ£g (𝑀 β†Ύ {𝑧})))))
7355, 72eqtrid 2782 . . . . . . . . 9 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (π‘₯ ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g π‘₯)) = (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ ((𝐺 Ξ£g (𝑀 β†Ύ 𝑦))(+gβ€˜πΊ)(𝐺 Ξ£g (𝑀 β†Ύ {𝑧})))))
74 simp1r 1196 . . . . . . . . . 10 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ 𝐺 ∈ TopMnd)
7574, 42syl 17 . . . . . . . . . . 11 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ 𝐽 ∈ (TopOnβ€˜π΅))
76 eqid 2730 . . . . . . . . . . . 12 (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) = (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽}))
7776pttoponconst 23321 . . . . . . . . . . 11 (((𝑦 βˆͺ {𝑧}) ∈ Fin ∧ 𝐽 ∈ (TopOnβ€˜π΅)) β†’ (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) ∈ (TopOnβ€˜(𝐡 ↑m (𝑦 βˆͺ {𝑧}))))
7861, 75, 77syl2anc 582 . . . . . . . . . 10 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) ∈ (TopOnβ€˜(𝐡 ↑m (𝑦 βˆͺ {𝑧}))))
79 toponuni 22636 . . . . . . . . . . . . . 14 ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) ∈ (TopOnβ€˜(𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) = βˆͺ (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})))
8078, 79syl 17 . . . . . . . . . . . . 13 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) = βˆͺ (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})))
8180mpteq1d 5242 . . . . . . . . . . . 12 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝑀 β†Ύ 𝑦)) = (𝑀 ∈ βˆͺ (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) ↦ (𝑀 β†Ύ 𝑦)))
82 topontop 22635 . . . . . . . . . . . . . . 15 (𝐽 ∈ (TopOnβ€˜π΅) β†’ 𝐽 ∈ Top)
8374, 42, 823syl 18 . . . . . . . . . . . . . 14 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ 𝐽 ∈ Top)
84 fconst6g 6779 . . . . . . . . . . . . . 14 (𝐽 ∈ Top β†’ ((𝑦 βˆͺ {𝑧}) Γ— {𝐽}):(𝑦 βˆͺ {𝑧})⟢Top)
8583, 84syl 17 . . . . . . . . . . . . 13 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ ((𝑦 βˆͺ {𝑧}) Γ— {𝐽}):(𝑦 βˆͺ {𝑧})⟢Top)
86 ssun1 4171 . . . . . . . . . . . . . 14 𝑦 βŠ† (𝑦 βˆͺ {𝑧})
8786a1i 11 . . . . . . . . . . . . 13 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ 𝑦 βŠ† (𝑦 βˆͺ {𝑧}))
88 eqid 2730 . . . . . . . . . . . . . 14 βˆͺ (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) = βˆͺ (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽}))
89 xpssres 6017 . . . . . . . . . . . . . . . . 17 (𝑦 βŠ† (𝑦 βˆͺ {𝑧}) β†’ (((𝑦 βˆͺ {𝑧}) Γ— {𝐽}) β†Ύ 𝑦) = (𝑦 Γ— {𝐽}))
9086, 89ax-mp 5 . . . . . . . . . . . . . . . 16 (((𝑦 βˆͺ {𝑧}) Γ— {𝐽}) β†Ύ 𝑦) = (𝑦 Γ— {𝐽})
9190eqcomi 2739 . . . . . . . . . . . . . . 15 (𝑦 Γ— {𝐽}) = (((𝑦 βˆͺ {𝑧}) Γ— {𝐽}) β†Ύ 𝑦)
9291fveq2i 6893 . . . . . . . . . . . . . 14 (∏tβ€˜(𝑦 Γ— {𝐽})) = (∏tβ€˜(((𝑦 βˆͺ {𝑧}) Γ— {𝐽}) β†Ύ 𝑦))
9388, 76, 92ptrescn 23363 . . . . . . . . . . . . 13 (((𝑦 βˆͺ {𝑧}) ∈ Fin ∧ ((𝑦 βˆͺ {𝑧}) Γ— {𝐽}):(𝑦 βˆͺ {𝑧})⟢Top ∧ 𝑦 βŠ† (𝑦 βˆͺ {𝑧})) β†’ (𝑀 ∈ βˆͺ (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) ↦ (𝑀 β†Ύ 𝑦)) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn (∏tβ€˜(𝑦 Γ— {𝐽}))))
9461, 85, 87, 93syl3anc 1369 . . . . . . . . . . . 12 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝑀 ∈ βˆͺ (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) ↦ (𝑀 β†Ύ 𝑦)) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn (∏tβ€˜(𝑦 Γ— {𝐽}))))
9581, 94eqeltrd 2831 . . . . . . . . . . 11 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝑀 β†Ύ 𝑦)) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn (∏tβ€˜(𝑦 Γ— {𝐽}))))
96 eqid 2730 . . . . . . . . . . . . 13 (∏tβ€˜(𝑦 Γ— {𝐽})) = (∏tβ€˜(𝑦 Γ— {𝐽}))
9796pttoponconst 23321 . . . . . . . . . . . 12 ((𝑦 ∈ Fin ∧ 𝐽 ∈ (TopOnβ€˜π΅)) β†’ (∏tβ€˜(𝑦 Γ— {𝐽})) ∈ (TopOnβ€˜(𝐡 ↑m 𝑦)))
9858, 75, 97syl2anc 582 . . . . . . . . . . 11 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (∏tβ€˜(𝑦 Γ— {𝐽})) ∈ (TopOnβ€˜(𝐡 ↑m 𝑦)))
99 simp3 1136 . . . . . . . . . . 11 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽))
100 oveq2 7419 . . . . . . . . . . 11 (π‘₯ = (𝑀 β†Ύ 𝑦) β†’ (𝐺 Ξ£g π‘₯) = (𝐺 Ξ£g (𝑀 β†Ύ 𝑦)))
10178, 95, 98, 99, 100cnmpt11 23387 . . . . . . . . . 10 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g (𝑀 β†Ύ 𝑦))) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn 𝐽))
10264feqmptd 6959 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ 𝑀 = (π‘˜ ∈ (𝑦 βˆͺ {𝑧}) ↦ (π‘€β€˜π‘˜)))
103102reseq1d 5979 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ (𝑀 β†Ύ {𝑧}) = ((π‘˜ ∈ (𝑦 βˆͺ {𝑧}) ↦ (π‘€β€˜π‘˜)) β†Ύ {𝑧}))
104 ssun2 4172 . . . . . . . . . . . . . . . 16 {𝑧} βŠ† (𝑦 βˆͺ {𝑧})
105 resmpt 6036 . . . . . . . . . . . . . . . 16 ({𝑧} βŠ† (𝑦 βˆͺ {𝑧}) β†’ ((π‘˜ ∈ (𝑦 βˆͺ {𝑧}) ↦ (π‘€β€˜π‘˜)) β†Ύ {𝑧}) = (π‘˜ ∈ {𝑧} ↦ (π‘€β€˜π‘˜)))
106104, 105ax-mp 5 . . . . . . . . . . . . . . 15 ((π‘˜ ∈ (𝑦 βˆͺ {𝑧}) ↦ (π‘€β€˜π‘˜)) β†Ύ {𝑧}) = (π‘˜ ∈ {𝑧} ↦ (π‘€β€˜π‘˜))
107103, 106eqtrdi 2786 . . . . . . . . . . . . . 14 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ (𝑀 β†Ύ {𝑧}) = (π‘˜ ∈ {𝑧} ↦ (π‘€β€˜π‘˜)))
108107oveq2d 7427 . . . . . . . . . . . . 13 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ (𝐺 Ξ£g (𝑀 β†Ύ {𝑧})) = (𝐺 Ξ£g (π‘˜ ∈ {𝑧} ↦ (π‘€β€˜π‘˜))))
109 cmnmnd 19706 . . . . . . . . . . . . . . 15 (𝐺 ∈ CMnd β†’ 𝐺 ∈ Mnd)
11057, 109syl 17 . . . . . . . . . . . . . 14 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ 𝐺 ∈ Mnd)
111 vex 3476 . . . . . . . . . . . . . . 15 𝑧 ∈ V
112111a1i 11 . . . . . . . . . . . . . 14 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ 𝑧 ∈ V)
113 vsnid 4664 . . . . . . . . . . . . . . . 16 𝑧 ∈ {𝑧}
114 elun2 4176 . . . . . . . . . . . . . . . 16 (𝑧 ∈ {𝑧} β†’ 𝑧 ∈ (𝑦 βˆͺ {𝑧}))
115113, 114mp1i 13 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ 𝑧 ∈ (𝑦 βˆͺ {𝑧}))
11664, 115ffvelcdmd 7086 . . . . . . . . . . . . . 14 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ (π‘€β€˜π‘§) ∈ 𝐡)
117 fveq2 6890 . . . . . . . . . . . . . . 15 (π‘˜ = 𝑧 β†’ (π‘€β€˜π‘˜) = (π‘€β€˜π‘§))
11841, 117gsumsn 19863 . . . . . . . . . . . . . 14 ((𝐺 ∈ Mnd ∧ 𝑧 ∈ V ∧ (π‘€β€˜π‘§) ∈ 𝐡) β†’ (𝐺 Ξ£g (π‘˜ ∈ {𝑧} ↦ (π‘€β€˜π‘˜))) = (π‘€β€˜π‘§))
119110, 112, 116, 118syl3anc 1369 . . . . . . . . . . . . 13 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ (𝐺 Ξ£g (π‘˜ ∈ {𝑧} ↦ (π‘€β€˜π‘˜))) = (π‘€β€˜π‘§))
120108, 119eqtrd 2770 . . . . . . . . . . . 12 ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) ∧ 𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧}))) β†’ (𝐺 Ξ£g (𝑀 β†Ύ {𝑧})) = (π‘€β€˜π‘§))
121120mpteq2dva 5247 . . . . . . . . . . 11 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g (𝑀 β†Ύ {𝑧}))) = (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (π‘€β€˜π‘§)))
12280mpteq1d 5242 . . . . . . . . . . . . 13 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (π‘€β€˜π‘§)) = (𝑀 ∈ βˆͺ (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) ↦ (π‘€β€˜π‘§)))
123113, 114mp1i 13 . . . . . . . . . . . . . 14 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ 𝑧 ∈ (𝑦 βˆͺ {𝑧}))
12488, 76ptpjcn 23335 . . . . . . . . . . . . . 14 (((𝑦 βˆͺ {𝑧}) ∈ Fin ∧ ((𝑦 βˆͺ {𝑧}) Γ— {𝐽}):(𝑦 βˆͺ {𝑧})⟢Top ∧ 𝑧 ∈ (𝑦 βˆͺ {𝑧})) β†’ (𝑀 ∈ βˆͺ (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) ↦ (π‘€β€˜π‘§)) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn (((𝑦 βˆͺ {𝑧}) Γ— {𝐽})β€˜π‘§)))
12561, 85, 123, 124syl3anc 1369 . . . . . . . . . . . . 13 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝑀 ∈ βˆͺ (∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) ↦ (π‘€β€˜π‘§)) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn (((𝑦 βˆͺ {𝑧}) Γ— {𝐽})β€˜π‘§)))
126122, 125eqeltrd 2831 . . . . . . . . . . . 12 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (π‘€β€˜π‘§)) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn (((𝑦 βˆͺ {𝑧}) Γ— {𝐽})β€˜π‘§)))
127 fvconst2g 7204 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ 𝑧 ∈ (𝑦 βˆͺ {𝑧})) β†’ (((𝑦 βˆͺ {𝑧}) Γ— {𝐽})β€˜π‘§) = 𝐽)
12883, 123, 127syl2anc 582 . . . . . . . . . . . . 13 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (((𝑦 βˆͺ {𝑧}) Γ— {𝐽})β€˜π‘§) = 𝐽)
129128oveq2d 7427 . . . . . . . . . . . 12 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn (((𝑦 βˆͺ {𝑧}) Γ— {𝐽})β€˜π‘§)) = ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn 𝐽))
130126, 129eleqtrd 2833 . . . . . . . . . . 11 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (π‘€β€˜π‘§)) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn 𝐽))
131121, 130eqeltrd 2831 . . . . . . . . . 10 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g (𝑀 β†Ύ {𝑧}))) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn 𝐽))
13240, 56, 74, 78, 101, 131cnmpt1plusg 23811 . . . . . . . . 9 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (𝑀 ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ ((𝐺 Ξ£g (𝑀 β†Ύ 𝑦))(+gβ€˜πΊ)(𝐺 Ξ£g (𝑀 β†Ύ {𝑧})))) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn 𝐽))
13373, 132eqeltrd 2831 . . . . . . . 8 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) ∧ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ (π‘₯ ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn 𝐽))
1341333expia 1119 . . . . . . 7 (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦)) β†’ ((π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽) β†’ (π‘₯ ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn 𝐽)))
135134expcom 412 . . . . . 6 ((𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) β†’ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ ((π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽) β†’ (π‘₯ ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn 𝐽))))
136135a2d 29 . . . . 5 ((𝑦 ∈ Fin ∧ Β¬ 𝑧 ∈ 𝑦) β†’ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (π‘₯ ∈ (𝐡 ↑m 𝑦) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝑦 Γ— {𝐽})) Cn 𝐽)) β†’ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (π‘₯ ∈ (𝐡 ↑m (𝑦 βˆͺ {𝑧})) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜((𝑦 βˆͺ {𝑧}) Γ— {𝐽})) Cn 𝐽))))
1379, 16, 23, 30, 53, 136findcard2s 9167 . . . 4 (𝐴 ∈ Fin β†’ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (π‘₯ ∈ (𝐡 ↑m 𝐴) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝐴 Γ— {𝐽})) Cn 𝐽)))
138137com12 32 . . 3 ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) β†’ (𝐴 ∈ Fin β†’ (π‘₯ ∈ (𝐡 ↑m 𝐴) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝐴 Γ— {𝐽})) Cn 𝐽)))
1391383impia 1115 . 2 ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) β†’ (π‘₯ ∈ (𝐡 ↑m 𝐴) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((∏tβ€˜(𝐴 Γ— {𝐽})) Cn 𝐽))
14042, 82syl 17 . . . . 5 (𝐺 ∈ TopMnd β†’ 𝐽 ∈ Top)
141 xkopt 23379 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin) β†’ (𝐽 ↑ko 𝒫 𝐴) = (∏tβ€˜(𝐴 Γ— {𝐽})))
142140, 141sylan 578 . . . 4 ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) β†’ (𝐽 ↑ko 𝒫 𝐴) = (∏tβ€˜(𝐴 Γ— {𝐽})))
1431423adant1 1128 . . 3 ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) β†’ (𝐽 ↑ko 𝒫 𝐴) = (∏tβ€˜(𝐴 Γ— {𝐽})))
144143oveq1d 7426 . 2 ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) β†’ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽) = ((∏tβ€˜(𝐴 Γ— {𝐽})) Cn 𝐽))
145139, 144eleqtrrd 2834 1 ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) β†’ (π‘₯ ∈ (𝐡 ↑m 𝐴) ↦ (𝐺 Ξ£g π‘₯)) ∈ ((𝐽 ↑ko 𝒫 𝐴) Cn 𝐽))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  Vcvv 3472   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907   ↦ cmpt 5230   Γ— cxp 5673   β†Ύ cres 5677   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411   ↑m cmap 8822  Fincfn 8941  Basecbs 17148  +gcplusg 17201  TopOpenctopn 17371  βˆtcpt 17388  0gc0g 17389   Ξ£g cgsu 17390  Mndcmnd 18659  CMndccmn 19689  Topctop 22615  TopOnctopon 22632   Cn ccn 22948   ↑ko cxko 23285  TopMndctmd 23794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-n0 12477  df-z 12563  df-uz 12827  df-fz 13489  df-fzo 13632  df-seq 13971  df-hash 14295  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-rest 17372  df-0g 17391  df-gsum 17392  df-topgen 17393  df-pt 17394  df-mre 17534  df-mrc 17535  df-acs 17537  df-plusf 18564  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-submnd 18706  df-mulg 18987  df-cntz 19222  df-cmn 19691  df-top 22616  df-topon 22633  df-topsp 22655  df-bases 22669  df-cn 22951  df-cnp 22952  df-cmp 23111  df-tx 23286  df-xko 23287  df-tmd 23796
This theorem is referenced by:  tmdgsum2  23820
  Copyright terms: Public domain W3C validator