Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (𝐵 ↑𝑚
𝑤) = (𝐵 ↑𝑚
∅)) |
2 | 1 | mpteq1d 4666 |
. . . . . . 7
⊢ (𝑤 = ∅ → (𝑥 ∈ (𝐵 ↑𝑚 𝑤) ↦ (𝐺 Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑𝑚 ∅) ↦
(𝐺
Σg 𝑥))) |
3 | | xpeq1 5052 |
. . . . . . . . . 10
⊢ (𝑤 = ∅ → (𝑤 × {𝐽}) = (∅ × {𝐽})) |
4 | | 0xp 5122 |
. . . . . . . . . 10
⊢ (∅
× {𝐽}) =
∅ |
5 | 3, 4 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → (𝑤 × {𝐽}) = ∅) |
6 | 5 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑤 = ∅ →
(∏t‘(𝑤 × {𝐽})) =
(∏t‘∅)) |
7 | 6 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑤 = ∅ →
((∏t‘(𝑤 × {𝐽})) Cn 𝐽) = ((∏t‘∅) Cn
𝐽)) |
8 | 2, 7 | eleq12d 2682 |
. . . . . 6
⊢ (𝑤 = ∅ → ((𝑥 ∈ (𝐵 ↑𝑚 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽) ↔ (𝑥 ∈ (𝐵 ↑𝑚 ∅) ↦
(𝐺
Σg 𝑥)) ∈ ((∏t‘∅)
Cn 𝐽))) |
9 | 8 | imbi2d 329 |
. . . . 5
⊢ (𝑤 = ∅ → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑𝑚 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑𝑚 ∅) ↦
(𝐺
Σg 𝑥)) ∈ ((∏t‘∅)
Cn 𝐽)))) |
10 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → (𝐵 ↑𝑚 𝑤) = (𝐵 ↑𝑚 𝑦)) |
11 | 10 | mpteq1d 4666 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝑥 ∈ (𝐵 ↑𝑚 𝑤) ↦ (𝐺 Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥))) |
12 | | xpeq1 5052 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝑤 × {𝐽}) = (𝑦 × {𝐽})) |
13 | 12 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → (∏t‘(𝑤 × {𝐽})) = (∏t‘(𝑦 × {𝐽}))) |
14 | 13 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) = ((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) |
15 | 11, 14 | eleq12d 2682 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((𝑥 ∈ (𝐵 ↑𝑚 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽) ↔ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽))) |
16 | 15 | imbi2d 329 |
. . . . 5
⊢ (𝑤 = 𝑦 → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑𝑚 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)))) |
17 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝐵 ↑𝑚 𝑤) = (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) |
18 | 17 | mpteq1d 4666 |
. . . . . . 7
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑥 ∈ (𝐵 ↑𝑚 𝑤) ↦ (𝐺 Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥))) |
19 | | xpeq1 5052 |
. . . . . . . . 9
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑤 × {𝐽}) = ((𝑦 ∪ {𝑧}) × {𝐽})) |
20 | 19 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (∏t‘(𝑤 × {𝐽})) = (∏t‘((𝑦 ∪ {𝑧}) × {𝐽}))) |
21 | 20 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) = ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) |
22 | 18, 21 | eleq12d 2682 |
. . . . . 6
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑥 ∈ (𝐵 ↑𝑚 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽) ↔ (𝑥 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))) |
23 | 22 | imbi2d 329 |
. . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑𝑚 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)))) |
24 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑤 = 𝐴 → (𝐵 ↑𝑚 𝑤) = (𝐵 ↑𝑚 𝐴)) |
25 | 24 | mpteq1d 4666 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → (𝑥 ∈ (𝐵 ↑𝑚 𝑤) ↦ (𝐺 Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑥))) |
26 | | xpeq1 5052 |
. . . . . . . . 9
⊢ (𝑤 = 𝐴 → (𝑤 × {𝐽}) = (𝐴 × {𝐽})) |
27 | 26 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑤 = 𝐴 → (∏t‘(𝑤 × {𝐽})) = (∏t‘(𝐴 × {𝐽}))) |
28 | 27 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → ((∏t‘(𝑤 × {𝐽})) Cn 𝐽) = ((∏t‘(𝐴 × {𝐽})) Cn 𝐽)) |
29 | 25, 28 | eleq12d 2682 |
. . . . . 6
⊢ (𝑤 = 𝐴 → ((𝑥 ∈ (𝐵 ↑𝑚 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽) ↔ (𝑥 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝐴 × {𝐽})) Cn 𝐽))) |
30 | 29 | imbi2d 329 |
. . . . 5
⊢ (𝑤 = 𝐴 → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑𝑚 𝑤) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑤 × {𝐽})) Cn 𝐽)) ↔ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝐴 × {𝐽})) Cn 𝐽)))) |
31 | | elmapfn 7766 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐵 ↑𝑚 ∅) →
𝑥 Fn
∅) |
32 | | fn0 5924 |
. . . . . . . . . 10
⊢ (𝑥 Fn ∅ ↔ 𝑥 = ∅) |
33 | 31, 32 | sylib 207 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ↑𝑚 ∅) →
𝑥 =
∅) |
34 | 33 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ↑𝑚 ∅) →
(𝐺
Σg 𝑥) = (𝐺 Σg
∅)) |
35 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
36 | 35 | gsum0 17101 |
. . . . . . . 8
⊢ (𝐺 Σg
∅) = (0g‘𝐺) |
37 | 34, 36 | syl6eq 2660 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐵 ↑𝑚 ∅) →
(𝐺
Σg 𝑥) = (0g‘𝐺)) |
38 | 37 | mpteq2ia 4668 |
. . . . . 6
⊢ (𝑥 ∈ (𝐵 ↑𝑚 ∅) ↦
(𝐺
Σg 𝑥)) = (𝑥 ∈ (𝐵 ↑𝑚 ∅) ↦
(0g‘𝐺)) |
39 | | 0ex 4718 |
. . . . . . . 8
⊢ ∅
∈ V |
40 | | tmdgsum.j |
. . . . . . . . . 10
⊢ 𝐽 = (TopOpen‘𝐺) |
41 | | tmdgsum.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝐺) |
42 | 40, 41 | tmdtopon 21695 |
. . . . . . . . 9
⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝐵)) |
43 | 42 | adantl 481 |
. . . . . . . 8
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → 𝐽 ∈ (TopOn‘𝐵)) |
44 | 4 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(∏t‘(∅ × {𝐽})) =
(∏t‘∅) |
45 | 44 | eqcomi 2619 |
. . . . . . . . 9
⊢
(∏t‘∅) = (∏t‘(∅
× {𝐽})) |
46 | 45 | pttoponconst 21210 |
. . . . . . . 8
⊢ ((∅
∈ V ∧ 𝐽 ∈
(TopOn‘𝐵)) →
(∏t‘∅) ∈ (TopOn‘(𝐵 ↑𝑚
∅))) |
47 | 39, 43, 46 | sylancr 694 |
. . . . . . 7
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) →
(∏t‘∅) ∈ (TopOn‘(𝐵 ↑𝑚
∅))) |
48 | | tmdmnd 21689 |
. . . . . . . . 9
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd) |
49 | 48 | adantl 481 |
. . . . . . . 8
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → 𝐺 ∈ Mnd) |
50 | 41, 35 | mndidcl 17131 |
. . . . . . . 8
⊢ (𝐺 ∈ Mnd →
(0g‘𝐺)
∈ 𝐵) |
51 | 49, 50 | syl 17 |
. . . . . . 7
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) →
(0g‘𝐺)
∈ 𝐵) |
52 | 47, 43, 51 | cnmptc 21275 |
. . . . . 6
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑𝑚 ∅) ↦
(0g‘𝐺))
∈ ((∏t‘∅) Cn 𝐽)) |
53 | 38, 52 | syl5eqel 2692 |
. . . . 5
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑𝑚 ∅) ↦
(𝐺
Σg 𝑥)) ∈ ((∏t‘∅)
Cn 𝐽)) |
54 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → (𝐺 Σg 𝑥) = (𝐺 Σg 𝑤)) |
55 | 54 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) = (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑤)) |
56 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(+g‘𝐺) = (+g‘𝐺) |
57 | | simpl1l 1105 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → 𝐺 ∈ CMnd) |
58 | | simp2l 1080 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝑦 ∈ Fin) |
59 | | snfi 7923 |
. . . . . . . . . . . . . 14
⊢ {𝑧} ∈ Fin |
60 | | unfi 8112 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝑦 ∪ {𝑧}) ∈ Fin) |
61 | 58, 59, 60 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑦 ∪ {𝑧}) ∈ Fin) |
62 | 61 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → (𝑦 ∪ {𝑧}) ∈ Fin) |
63 | | elmapi 7765 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) → 𝑤:(𝑦 ∪ {𝑧})⟶𝐵) |
64 | 63 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → 𝑤:(𝑦 ∪ {𝑧})⟶𝐵) |
65 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐺) ∈ V |
66 | 65 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → (0g‘𝐺) ∈ V) |
67 | 64, 62, 66 | fdmfifsupp 8168 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → 𝑤 finSupp (0g‘𝐺)) |
68 | | simpl2r 1108 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → ¬ 𝑧 ∈ 𝑦) |
69 | | disjsn 4192 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) |
70 | 68, 69 | sylibr 223 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → (𝑦 ∩ {𝑧}) = ∅) |
71 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧})) |
72 | 41, 35, 56, 57, 62, 64, 67, 70, 71 | gsumsplit 18151 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → (𝐺 Σg 𝑤) = ((𝐺 Σg (𝑤 ↾ 𝑦))(+g‘𝐺)(𝐺 Σg (𝑤 ↾ {𝑧})))) |
73 | 72 | mpteq2dva 4672 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑤)) = (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ ((𝐺 Σg (𝑤 ↾ 𝑦))(+g‘𝐺)(𝐺 Σg (𝑤 ↾ {𝑧}))))) |
74 | 55, 73 | syl5eq 2656 |
. . . . . . . . 9
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑥 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) = (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ ((𝐺 Σg (𝑤 ↾ 𝑦))(+g‘𝐺)(𝐺 Σg (𝑤 ↾ {𝑧}))))) |
75 | | simp1r 1079 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝐺 ∈ TopMnd) |
76 | 75, 42 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝐽 ∈ (TopOn‘𝐵)) |
77 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) = (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) |
78 | 77 | pttoponconst 21210 |
. . . . . . . . . . 11
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ 𝐽 ∈ (TopOn‘𝐵)) → (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ∈ (TopOn‘(𝐵 ↑𝑚 (𝑦 ∪ {𝑧})))) |
79 | 61, 76, 78 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ∈ (TopOn‘(𝐵 ↑𝑚 (𝑦 ∪ {𝑧})))) |
80 | | toponuni 20542 |
. . . . . . . . . . . . . 14
⊢
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ∈ (TopOn‘(𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) = ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽}))) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) = ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽}))) |
82 | 81 | mpteq1d 4666 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝑤 ↾ 𝑦)) = (𝑤 ∈ ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤 ↾ 𝑦))) |
83 | | topontop 20541 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) |
84 | 75, 42, 83 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝐽 ∈ Top) |
85 | | fconst6g 6007 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ Top → ((𝑦 ∪ {𝑧}) × {𝐽}):(𝑦 ∪ {𝑧})⟶Top) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → ((𝑦 ∪ {𝑧}) × {𝐽}):(𝑦 ∪ {𝑧})⟶Top) |
87 | | ssun1 3738 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
88 | 87 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝑦 ⊆ (𝑦 ∪ {𝑧})) |
89 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ ∪ (∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) = ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) |
90 | | xpssres 5354 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (((𝑦 ∪ {𝑧}) × {𝐽}) ↾ 𝑦) = (𝑦 × {𝐽})) |
91 | 87, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∪ {𝑧}) × {𝐽}) ↾ 𝑦) = (𝑦 × {𝐽}) |
92 | 91 | eqcomi 2619 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 × {𝐽}) = (((𝑦 ∪ {𝑧}) × {𝐽}) ↾ 𝑦) |
93 | 92 | fveq2i 6106 |
. . . . . . . . . . . . . 14
⊢
(∏t‘(𝑦 × {𝐽})) = (∏t‘(((𝑦 ∪ {𝑧}) × {𝐽}) ↾ 𝑦)) |
94 | 89, 77, 93 | ptrescn 21252 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ ((𝑦 ∪ {𝑧}) × {𝐽}):(𝑦 ∪ {𝑧})⟶Top ∧ 𝑦 ⊆ (𝑦 ∪ {𝑧})) → (𝑤 ∈ ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤 ↾ 𝑦)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (∏t‘(𝑦 × {𝐽})))) |
95 | 61, 86, 88, 94 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤 ↾ 𝑦)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (∏t‘(𝑦 × {𝐽})))) |
96 | 82, 95 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝑤 ↾ 𝑦)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (∏t‘(𝑦 × {𝐽})))) |
97 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(∏t‘(𝑦 × {𝐽})) = (∏t‘(𝑦 × {𝐽})) |
98 | 97 | pttoponconst 21210 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ Fin ∧ 𝐽 ∈ (TopOn‘𝐵)) →
(∏t‘(𝑦 × {𝐽})) ∈ (TopOn‘(𝐵 ↑𝑚 𝑦))) |
99 | 58, 76, 98 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (∏t‘(𝑦 × {𝐽})) ∈ (TopOn‘(𝐵 ↑𝑚 𝑦))) |
100 | | simp3 1056 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) |
101 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑤 ↾ 𝑦) → (𝐺 Σg 𝑥) = (𝐺 Σg (𝑤 ↾ 𝑦))) |
102 | 79, 96, 99, 100, 101 | cnmpt11 21276 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg (𝑤 ↾ 𝑦))) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) |
103 | 64 | feqmptd 6159 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → 𝑤 = (𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ (𝑤‘𝑘))) |
104 | 103 | reseq1d 5316 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → (𝑤 ↾ {𝑧}) = ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ (𝑤‘𝑘)) ↾ {𝑧})) |
105 | | ssun2 3739 |
. . . . . . . . . . . . . . . 16
⊢ {𝑧} ⊆ (𝑦 ∪ {𝑧}) |
106 | | resmpt 5369 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ (𝑤‘𝑘)) ↾ {𝑧}) = (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘))) |
107 | 105, 106 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ (𝑦 ∪ {𝑧}) ↦ (𝑤‘𝑘)) ↾ {𝑧}) = (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘)) |
108 | 104, 107 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → (𝑤 ↾ {𝑧}) = (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘))) |
109 | 108 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → (𝐺 Σg (𝑤 ↾ {𝑧})) = (𝐺 Σg (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘)))) |
110 | | cmnmnd 18031 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
111 | 57, 110 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → 𝐺 ∈ Mnd) |
112 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑧 ∈ V |
113 | 112 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → 𝑧 ∈ V) |
114 | | vsnid 4156 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ {𝑧} |
115 | | elun2 3743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ {𝑧} → 𝑧 ∈ (𝑦 ∪ {𝑧})) |
116 | 114, 115 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → 𝑧 ∈ (𝑦 ∪ {𝑧})) |
117 | 64, 116 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → (𝑤‘𝑧) ∈ 𝐵) |
118 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑧 → (𝑤‘𝑘) = (𝑤‘𝑧)) |
119 | 41, 118 | gsumsn 18177 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Mnd ∧ 𝑧 ∈ V ∧ (𝑤‘𝑧) ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘))) = (𝑤‘𝑧)) |
120 | 111, 113,
117, 119 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → (𝐺 Σg (𝑘 ∈ {𝑧} ↦ (𝑤‘𝑘))) = (𝑤‘𝑧)) |
121 | 109, 120 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) ∧ 𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧}))) → (𝐺 Σg (𝑤 ↾ {𝑧})) = (𝑤‘𝑧)) |
122 | 121 | mpteq2dva 4672 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg (𝑤 ↾ {𝑧}))) = (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝑤‘𝑧))) |
123 | 81 | mpteq1d 4666 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝑤‘𝑧)) = (𝑤 ∈ ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤‘𝑧))) |
124 | 114, 115 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → 𝑧 ∈ (𝑦 ∪ {𝑧})) |
125 | 89, 77 | ptpjcn 21224 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 ∪ {𝑧}) ∈ Fin ∧ ((𝑦 ∪ {𝑧}) × {𝐽}):(𝑦 ∪ {𝑧})⟶Top ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})) → (𝑤 ∈ ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤‘𝑧)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧))) |
126 | 61, 86, 124, 125 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ ∪
(∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) ↦ (𝑤‘𝑧)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧))) |
127 | 123, 126 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝑤‘𝑧)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧))) |
128 | | fvconst2g 6372 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ 𝑧 ∈ (𝑦 ∪ {𝑧})) → (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧) = 𝐽) |
129 | 84, 124, 128 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧) = 𝐽) |
130 | 129 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn (((𝑦 ∪ {𝑧}) × {𝐽})‘𝑧)) = ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) |
131 | 127, 130 | eleqtrd 2690 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝑤‘𝑧)) ∈ ((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) |
132 | 122, 131 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg (𝑤 ↾ {𝑧}))) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) |
133 | 40, 56, 75, 79, 102, 132 | cnmpt1plusg 21701 |
. . . . . . . . 9
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑤 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ ((𝐺 Σg (𝑤 ↾ 𝑦))(+g‘𝐺)(𝐺 Σg (𝑤 ↾ {𝑧})))) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) |
134 | 74, 133 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) ∧ (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → (𝑥 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)) |
135 | 134 | 3expia 1259 |
. . . . . . 7
⊢ (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦)) → ((𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽) → (𝑥 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽))) |
136 | 135 | expcom 450 |
. . . . . 6
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → ((𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽) → (𝑥 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)))) |
137 | 136 | a2d 29 |
. . . . 5
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → (((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑𝑚 𝑦) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝑦 × {𝐽})) Cn 𝐽)) → ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑𝑚 (𝑦 ∪ {𝑧})) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘((𝑦 ∪ {𝑧}) × {𝐽})) Cn 𝐽)))) |
138 | 9, 16, 23, 30, 53, 137 | findcard2s 8086 |
. . . 4
⊢ (𝐴 ∈ Fin → ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝑥 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝐴 × {𝐽})) Cn 𝐽))) |
139 | 138 | com12 32 |
. . 3
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd) → (𝐴 ∈ Fin → (𝑥 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝐴 × {𝐽})) Cn 𝐽))) |
140 | 139 | 3impia 1253 |
. 2
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝑥 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑥)) ∈
((∏t‘(𝐴 × {𝐽})) Cn 𝐽)) |
141 | 42, 83 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ Top) |
142 | | xkopt 21268 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin) → (𝐽 ^ko 𝒫
𝐴) =
(∏t‘(𝐴 × {𝐽}))) |
143 | 141, 142 | sylan 487 |
. . . 4
⊢ ((𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝐽 ^ko 𝒫
𝐴) =
(∏t‘(𝐴 × {𝐽}))) |
144 | 143 | 3adant1 1072 |
. . 3
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝐽 ^ko 𝒫
𝐴) =
(∏t‘(𝐴 × {𝐽}))) |
145 | 144 | oveq1d 6564 |
. 2
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → ((𝐽 ^ko 𝒫
𝐴) Cn 𝐽) = ((∏t‘(𝐴 × {𝐽})) Cn 𝐽)) |
146 | 140, 145 | eleqtrrd 2691 |
1
⊢ ((𝐺 ∈ CMnd ∧ 𝐺 ∈ TopMnd ∧ 𝐴 ∈ Fin) → (𝑥 ∈ (𝐵 ↑𝑚 𝐴) ↦ (𝐺 Σg 𝑥)) ∈ ((𝐽 ^ko 𝒫 𝐴) Cn 𝐽)) |