Step | Hyp | Ref
| Expression |
1 | | tsmsxp.2 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TopGrp) |
2 | | tgpgrp 21692 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ Grp) |
4 | | tsmsxp.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ CMnd) |
5 | | isabl 18020 |
. . . 4
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
6 | 3, 4, 5 | sylanbrc 695 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Abel) |
7 | | tsmsxp.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
8 | | tsmsxp.z |
. . . 4
⊢ 0 =
(0g‘𝐺) |
9 | | tsmsxp.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐴 ∩ Fin)) |
10 | | elfpw 8151 |
. . . . . . 7
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐾 ⊆ 𝐴 ∧ 𝐾 ∈ Fin)) |
11 | 10 | simprbi 479 |
. . . . . 6
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ∈ Fin) |
12 | 9, 11 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ Fin) |
13 | | tsmsxp.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (𝒫 𝐶 ∩ Fin)) |
14 | | elfpw 8151 |
. . . . . . 7
⊢ (𝑁 ∈ (𝒫 𝐶 ∩ Fin) ↔ (𝑁 ⊆ 𝐶 ∧ 𝑁 ∈ Fin)) |
15 | 14 | simprbi 479 |
. . . . . 6
⊢ (𝑁 ∈ (𝒫 𝐶 ∩ Fin) → 𝑁 ∈ Fin) |
16 | 13, 15 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ Fin) |
17 | | xpfi 8116 |
. . . . 5
⊢ ((𝐾 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝐾 × 𝑁) ∈ Fin) |
18 | 12, 16, 17 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝐾 × 𝑁) ∈ Fin) |
19 | | tsmsxp.f |
. . . . 5
⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
20 | 10 | simplbi 475 |
. . . . . . 7
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ⊆ 𝐴) |
21 | 9, 20 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 ⊆ 𝐴) |
22 | 14 | simplbi 475 |
. . . . . . 7
⊢ (𝑁 ∈ (𝒫 𝐶 ∩ Fin) → 𝑁 ⊆ 𝐶) |
23 | 13, 22 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑁 ⊆ 𝐶) |
24 | | xpss12 5148 |
. . . . . 6
⊢ ((𝐾 ⊆ 𝐴 ∧ 𝑁 ⊆ 𝐶) → (𝐾 × 𝑁) ⊆ (𝐴 × 𝐶)) |
25 | 21, 23, 24 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐾 × 𝑁) ⊆ (𝐴 × 𝐶)) |
26 | 19, 25 | fssresd 5984 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ (𝐾 × 𝑁)):(𝐾 × 𝑁)⟶𝐵) |
27 | | tsmsxp.3 |
. . . . 5
⊢ (𝜑 → 0 ∈ 𝐿) |
28 | 26, 18, 27 | fdmfifsupp 8168 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ (𝐾 × 𝑁)) finSupp 0 ) |
29 | 7, 8, 4, 18, 26, 28 | gsumcl 18139 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) ∈ 𝐵) |
30 | | tsmsxp.h |
. . . . 5
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) |
31 | 30, 21 | fssresd 5984 |
. . . 4
⊢ (𝜑 → (𝐻 ↾ 𝐾):𝐾⟶𝐵) |
32 | 31, 12, 27 | fdmfifsupp 8168 |
. . . 4
⊢ (𝜑 → (𝐻 ↾ 𝐾) finSupp 0 ) |
33 | 7, 8, 4, 12, 31, 32 | gsumcl 18139 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐻 ↾ 𝐾)) ∈ 𝐵) |
34 | | tsmsxp.p |
. . . 4
⊢ + =
(+g‘𝐺) |
35 | | tsmsxp.m |
. . . 4
⊢ − =
(-g‘𝐺) |
36 | 7, 34, 35 | ablpncan3 18045 |
. . 3
⊢ ((𝐺 ∈ Abel ∧ ((𝐺 Σg
(𝐹 ↾ (𝐾 × 𝑁))) ∈ 𝐵 ∧ (𝐺 Σg (𝐻 ↾ 𝐾)) ∈ 𝐵)) → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) = (𝐺 Σg (𝐻 ↾ 𝐾))) |
37 | 6, 29, 33, 36 | syl12anc 1316 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) = (𝐺 Σg (𝐻 ↾ 𝐾))) |
38 | | tsmsxp.5 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) ∈ 𝑆) |
39 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝐺 ∈ CMnd) |
40 | | snfi 7923 |
. . . . . . . . 9
⊢ {𝑦} ∈ Fin |
41 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝑁 ∈ Fin) |
42 | | xpfi 8116 |
. . . . . . . . 9
⊢ (({𝑦} ∈ Fin ∧ 𝑁 ∈ Fin) → ({𝑦} × 𝑁) ∈ Fin) |
43 | 40, 41, 42 | sylancr 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → ({𝑦} × 𝑁) ∈ Fin) |
44 | 19 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
45 | 21 | sselda 3568 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝑦 ∈ 𝐴) |
46 | 45 | snssd 4281 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → {𝑦} ⊆ 𝐴) |
47 | 23 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝑁 ⊆ 𝐶) |
48 | | xpss12 5148 |
. . . . . . . . . 10
⊢ (({𝑦} ⊆ 𝐴 ∧ 𝑁 ⊆ 𝐶) → ({𝑦} × 𝑁) ⊆ (𝐴 × 𝐶)) |
49 | 46, 47, 48 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → ({𝑦} × 𝑁) ⊆ (𝐴 × 𝐶)) |
50 | 44, 49 | fssresd 5984 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹 ↾ ({𝑦} × 𝑁)):({𝑦} × 𝑁)⟶𝐵) |
51 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(0g‘𝐺) ∈ V |
52 | 8, 51 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 0 ∈
V |
53 | 52 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 0 ∈ V) |
54 | 50, 43, 53 | fdmfifsupp 8168 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹 ↾ ({𝑦} × 𝑁)) finSupp 0 ) |
55 | 7, 8, 39, 43, 50, 54 | gsumcl 18139 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))) ∈ 𝐵) |
56 | | eqid 2610 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) = (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) |
57 | 55, 56 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))):𝐾⟶𝐵) |
58 | | ovex 6577 |
. . . . . . . 8
⊢ (𝐺 Σg
(𝐹 ↾ ({𝑦} × 𝑁))) ∈ V |
59 | 58 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))) ∈ V) |
60 | 56, 12, 59, 27 | fsuppmptdm 8169 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) finSupp 0 ) |
61 | 7, 8, 35, 6, 12, 31, 57, 32, 60 | gsumsub 18171 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg ((𝐻 ↾ 𝐾) ∘𝑓 − (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))))) |
62 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐻‘𝑦) ∈ V |
63 | 62 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐻‘𝑦) ∈ V) |
64 | 30, 21 | feqresmpt 6160 |
. . . . . . 7
⊢ (𝜑 → (𝐻 ↾ 𝐾) = (𝑦 ∈ 𝐾 ↦ (𝐻‘𝑦))) |
65 | | eqidd 2611 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) = (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) |
66 | 12, 63, 59, 64, 65 | offval2 6812 |
. . . . . 6
⊢ (𝜑 → ((𝐻 ↾ 𝐾) ∘𝑓 − (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) = (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) |
67 | 66 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg ((𝐻 ↾ 𝐾) ∘𝑓 − (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) = (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))))) |
68 | | cmnmnd 18031 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
69 | 39, 68 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝐺 ∈ Mnd) |
70 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝑦 ∈ 𝐾) |
71 | 44 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
72 | 45 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → 𝑦 ∈ 𝐴) |
73 | 47 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → 𝑧 ∈ 𝐶) |
74 | 71, 72, 73 | fovrnd 6704 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → (𝑦𝐹𝑧) ∈ 𝐵) |
75 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)) = (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)) |
76 | 74, 75 | fmptd 6292 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)):𝑁⟶𝐵) |
77 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ (𝑦𝐹𝑧) ∈ V |
78 | 77 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → (𝑦𝐹𝑧) ∈ V) |
79 | 75, 41, 78, 53 | fsuppmptdm 8169 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)) finSupp 0 ) |
80 | 7, 8, 39, 41, 76, 79 | gsumcl 18139 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧))) ∈ 𝐵) |
81 | | velsn 4141 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {𝑦} ↔ 𝑤 = 𝑦) |
82 | | ovres 6698 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ {𝑦} ∧ 𝑧 ∈ 𝑁) → (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧) = (𝑤𝐹𝑧)) |
83 | 81, 82 | sylanbr 489 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 = 𝑦 ∧ 𝑧 ∈ 𝑁) → (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧) = (𝑤𝐹𝑧)) |
84 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑦 → (𝑤𝐹𝑧) = (𝑦𝐹𝑧)) |
85 | 84 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 = 𝑦 ∧ 𝑧 ∈ 𝑁) → (𝑤𝐹𝑧) = (𝑦𝐹𝑧)) |
86 | 83, 85 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 = 𝑦 ∧ 𝑧 ∈ 𝑁) → (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧) = (𝑦𝐹𝑧)) |
87 | 86 | mpteq2dva 4672 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑦 → (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧)) = (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧))) |
88 | 87 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑦 → (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)))) |
89 | 7, 88 | gsumsn 18177 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝐾 ∧ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧))) ∈ 𝐵) → (𝐺 Σg (𝑤 ∈ {𝑦} ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧))))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)))) |
90 | 69, 70, 80, 89 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝑤 ∈ {𝑦} ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧))))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)))) |
91 | 40 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → {𝑦} ∈ Fin) |
92 | 7, 8, 39, 91, 41, 50, 54 | gsumxp 18198 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))) = (𝐺 Σg (𝑤 ∈ {𝑦} ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧)))))) |
93 | | ovres 6698 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝑁) → (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧) = (𝑦𝐹𝑧)) |
94 | 93 | adantll 746 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧) = (𝑦𝐹𝑧)) |
95 | 94 | mpteq2dva 4672 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧)) = (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧))) |
96 | 95 | oveq2d 6565 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)))) |
97 | 90, 92, 96 | 3eqtr4d 2654 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧)))) |
98 | 97 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) = (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧))))) |
99 | 98 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) = (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧)))))) |
100 | 7, 8, 4, 12, 16, 26, 28 | gsumxp 18198 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) = (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧)))))) |
101 | 99, 100 | eqtr4d 2647 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) = (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) |
102 | 101 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) |
103 | 61, 67, 102 | 3eqtr3d 2652 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) |
104 | | tsmsxp.x |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁)))) ∈ 𝐿) |
105 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦)) |
106 | | sneq 4135 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
107 | 106 | xpeq1d 5062 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ({𝑥} × 𝑁) = ({𝑦} × 𝑁)) |
108 | 107 | reseq2d 5317 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝐹 ↾ ({𝑥} × 𝑁)) = (𝐹 ↾ ({𝑦} × 𝑁))) |
109 | 108 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁))) = (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) |
110 | 105, 109 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁)))) = ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) |
111 | 110 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁)))) ∈ 𝐿 ↔ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) ∈ 𝐿)) |
112 | 111 | rspccva 3281 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁)))) ∈ 𝐿 ∧ 𝑦 ∈ 𝐾) → ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) ∈ 𝐿) |
113 | 104, 112 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) ∈ 𝐿) |
114 | | eqid 2610 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) = (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) |
115 | 113, 114 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))):𝐾⟶𝐿) |
116 | | tsmsxp.l |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ 𝐽) |
117 | 116, 9 | elmapd 7758 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) ∈ (𝐿 ↑𝑚 𝐾) ↔ (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))):𝐾⟶𝐿)) |
118 | 115, 117 | mpbird 246 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) ∈ (𝐿 ↑𝑚 𝐾)) |
119 | | tsmsxp.6 |
. . . . 5
⊢ (𝜑 → ∀𝑔 ∈ (𝐿 ↑𝑚 𝐾)(𝐺 Σg 𝑔) ∈ 𝑇) |
120 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑔 = (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) → (𝐺 Σg 𝑔) = (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))))) |
121 | 120 | eleq1d 2672 |
. . . . . 6
⊢ (𝑔 = (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) → ((𝐺 Σg 𝑔) ∈ 𝑇 ↔ (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) ∈ 𝑇)) |
122 | 121 | rspcv 3278 |
. . . . 5
⊢ ((𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) ∈ (𝐿 ↑𝑚 𝐾) → (∀𝑔 ∈ (𝐿 ↑𝑚 𝐾)(𝐺 Σg 𝑔) ∈ 𝑇 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) ∈ 𝑇)) |
123 | 118, 119,
122 | sylc 63 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) ∈ 𝑇) |
124 | 103, 123 | eqeltrrd 2689 |
. . 3
⊢ (𝜑 → ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) ∈ 𝑇) |
125 | | tsmsxp.4 |
. . 3
⊢ (𝜑 → ∀𝑐 ∈ 𝑆 ∀𝑑 ∈ 𝑇 (𝑐 + 𝑑) ∈ 𝑈) |
126 | | oveq1 6556 |
. . . . 5
⊢ (𝑐 = (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) → (𝑐 + 𝑑) = ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + 𝑑)) |
127 | 126 | eleq1d 2672 |
. . . 4
⊢ (𝑐 = (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) → ((𝑐 + 𝑑) ∈ 𝑈 ↔ ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + 𝑑) ∈ 𝑈)) |
128 | | oveq2 6557 |
. . . . 5
⊢ (𝑑 = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + 𝑑) = ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))))) |
129 | 128 | eleq1d 2672 |
. . . 4
⊢ (𝑑 = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) → (((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + 𝑑) ∈ 𝑈 ↔ ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) ∈ 𝑈)) |
130 | 127, 129 | rspc2va 3294 |
. . 3
⊢ ((((𝐺 Σg
(𝐹 ↾ (𝐾 × 𝑁))) ∈ 𝑆 ∧ ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) ∈ 𝑇) ∧ ∀𝑐 ∈ 𝑆 ∀𝑑 ∈ 𝑇 (𝑐 + 𝑑) ∈ 𝑈) → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) ∈ 𝑈) |
131 | 38, 124, 125, 130 | syl21anc 1317 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) ∈ 𝑈) |
132 | 37, 131 | eqeltrrd 2689 |
1
⊢ (𝜑 → (𝐺 Σg (𝐻 ↾ 𝐾)) ∈ 𝑈) |