Step | Hyp | Ref
| Expression |
1 | | tsmsxp.2 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TopGrp) |
2 | | tgpgrp 21882 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ Grp) |
4 | | tsmsxp.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ CMnd) |
5 | | isabl 18197 |
. . . 4
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
6 | 3, 4, 5 | sylanbrc 698 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Abel) |
7 | | tsmsxp.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
8 | | tsmsxp.z |
. . . 4
⊢ 0 =
(0g‘𝐺) |
9 | | tsmsxp.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐴 ∩ Fin)) |
10 | | elfpw 8268 |
. . . . . . 7
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐾 ⊆ 𝐴 ∧ 𝐾 ∈ Fin)) |
11 | 10 | simprbi 480 |
. . . . . 6
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ∈ Fin) |
12 | 9, 11 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ Fin) |
13 | | tsmsxp.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (𝒫 𝐶 ∩ Fin)) |
14 | | elfpw 8268 |
. . . . . . 7
⊢ (𝑁 ∈ (𝒫 𝐶 ∩ Fin) ↔ (𝑁 ⊆ 𝐶 ∧ 𝑁 ∈ Fin)) |
15 | 14 | simprbi 480 |
. . . . . 6
⊢ (𝑁 ∈ (𝒫 𝐶 ∩ Fin) → 𝑁 ∈ Fin) |
16 | 13, 15 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ Fin) |
17 | | xpfi 8231 |
. . . . 5
⊢ ((𝐾 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝐾 × 𝑁) ∈ Fin) |
18 | 12, 16, 17 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝐾 × 𝑁) ∈ Fin) |
19 | | tsmsxp.f |
. . . . 5
⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
20 | 10 | simplbi 476 |
. . . . . . 7
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ⊆ 𝐴) |
21 | 9, 20 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 ⊆ 𝐴) |
22 | 14 | simplbi 476 |
. . . . . . 7
⊢ (𝑁 ∈ (𝒫 𝐶 ∩ Fin) → 𝑁 ⊆ 𝐶) |
23 | 13, 22 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑁 ⊆ 𝐶) |
24 | | xpss12 5225 |
. . . . . 6
⊢ ((𝐾 ⊆ 𝐴 ∧ 𝑁 ⊆ 𝐶) → (𝐾 × 𝑁) ⊆ (𝐴 × 𝐶)) |
25 | 21, 23, 24 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐾 × 𝑁) ⊆ (𝐴 × 𝐶)) |
26 | 19, 25 | fssresd 6071 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ (𝐾 × 𝑁)):(𝐾 × 𝑁)⟶𝐵) |
27 | | tsmsxp.3 |
. . . . 5
⊢ (𝜑 → 0 ∈ 𝐿) |
28 | 26, 18, 27 | fdmfifsupp 8285 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ (𝐾 × 𝑁)) finSupp 0 ) |
29 | 7, 8, 4, 18, 26, 28 | gsumcl 18316 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) ∈ 𝐵) |
30 | | tsmsxp.h |
. . . . 5
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) |
31 | 30, 21 | fssresd 6071 |
. . . 4
⊢ (𝜑 → (𝐻 ↾ 𝐾):𝐾⟶𝐵) |
32 | 31, 12, 27 | fdmfifsupp 8285 |
. . . 4
⊢ (𝜑 → (𝐻 ↾ 𝐾) finSupp 0 ) |
33 | 7, 8, 4, 12, 31, 32 | gsumcl 18316 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐻 ↾ 𝐾)) ∈ 𝐵) |
34 | | tsmsxp.p |
. . . 4
⊢ + =
(+g‘𝐺) |
35 | | tsmsxp.m |
. . . 4
⊢ − =
(-g‘𝐺) |
36 | 7, 34, 35 | ablpncan3 18222 |
. . 3
⊢ ((𝐺 ∈ Abel ∧ ((𝐺 Σg
(𝐹 ↾ (𝐾 × 𝑁))) ∈ 𝐵 ∧ (𝐺 Σg (𝐻 ↾ 𝐾)) ∈ 𝐵)) → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) = (𝐺 Σg (𝐻 ↾ 𝐾))) |
37 | 6, 29, 33, 36 | syl12anc 1324 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) = (𝐺 Σg (𝐻 ↾ 𝐾))) |
38 | | tsmsxp.5 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) ∈ 𝑆) |
39 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝐺 ∈ CMnd) |
40 | | snfi 8038 |
. . . . . . . . 9
⊢ {𝑦} ∈ Fin |
41 | 16 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝑁 ∈ Fin) |
42 | | xpfi 8231 |
. . . . . . . . 9
⊢ (({𝑦} ∈ Fin ∧ 𝑁 ∈ Fin) → ({𝑦} × 𝑁) ∈ Fin) |
43 | 40, 41, 42 | sylancr 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → ({𝑦} × 𝑁) ∈ Fin) |
44 | 19 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
45 | 21 | sselda 3603 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝑦 ∈ 𝐴) |
46 | 45 | snssd 4340 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → {𝑦} ⊆ 𝐴) |
47 | 23 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝑁 ⊆ 𝐶) |
48 | | xpss12 5225 |
. . . . . . . . . 10
⊢ (({𝑦} ⊆ 𝐴 ∧ 𝑁 ⊆ 𝐶) → ({𝑦} × 𝑁) ⊆ (𝐴 × 𝐶)) |
49 | 46, 47, 48 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → ({𝑦} × 𝑁) ⊆ (𝐴 × 𝐶)) |
50 | 44, 49 | fssresd 6071 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹 ↾ ({𝑦} × 𝑁)):({𝑦} × 𝑁)⟶𝐵) |
51 | | fvex 6201 |
. . . . . . . . . . 11
⊢
(0g‘𝐺) ∈ V |
52 | 8, 51 | eqeltri 2697 |
. . . . . . . . . 10
⊢ 0 ∈
V |
53 | 52 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 0 ∈ V) |
54 | 50, 43, 53 | fdmfifsupp 8285 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹 ↾ ({𝑦} × 𝑁)) finSupp 0 ) |
55 | 7, 8, 39, 43, 50, 54 | gsumcl 18316 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))) ∈ 𝐵) |
56 | | eqid 2622 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) = (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) |
57 | 55, 56 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))):𝐾⟶𝐵) |
58 | | ovexd 6680 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))) ∈ V) |
59 | 56, 12, 58, 27 | fsuppmptdm 8286 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) finSupp 0 ) |
60 | 7, 8, 35, 6, 12, 31, 57, 32, 59 | gsumsub 18348 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg ((𝐻 ↾ 𝐾) ∘𝑓 − (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))))) |
61 | | fvexd 6203 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐻‘𝑦) ∈ V) |
62 | 30, 21 | feqresmpt 6250 |
. . . . . . 7
⊢ (𝜑 → (𝐻 ↾ 𝐾) = (𝑦 ∈ 𝐾 ↦ (𝐻‘𝑦))) |
63 | | eqidd 2623 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) = (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) |
64 | 12, 61, 58, 62, 63 | offval2 6914 |
. . . . . 6
⊢ (𝜑 → ((𝐻 ↾ 𝐾) ∘𝑓 − (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) = (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) |
65 | 64 | oveq2d 6666 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg ((𝐻 ↾ 𝐾) ∘𝑓 − (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) = (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))))) |
66 | | cmnmnd 18208 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
67 | 39, 66 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝐺 ∈ Mnd) |
68 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝑦 ∈ 𝐾) |
69 | 44 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
70 | 45 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → 𝑦 ∈ 𝐴) |
71 | 47 | sselda 3603 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → 𝑧 ∈ 𝐶) |
72 | 69, 70, 71 | fovrnd 6806 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → (𝑦𝐹𝑧) ∈ 𝐵) |
73 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)) = (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)) |
74 | 72, 73 | fmptd 6385 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)):𝑁⟶𝐵) |
75 | | ovexd 6680 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → (𝑦𝐹𝑧) ∈ V) |
76 | 73, 41, 75, 53 | fsuppmptdm 8286 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)) finSupp 0 ) |
77 | 7, 8, 39, 41, 74, 76 | gsumcl 18316 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧))) ∈ 𝐵) |
78 | | velsn 4193 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {𝑦} ↔ 𝑤 = 𝑦) |
79 | | ovres 6800 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ {𝑦} ∧ 𝑧 ∈ 𝑁) → (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧) = (𝑤𝐹𝑧)) |
80 | 78, 79 | sylanbr 490 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 = 𝑦 ∧ 𝑧 ∈ 𝑁) → (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧) = (𝑤𝐹𝑧)) |
81 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑦 → (𝑤𝐹𝑧) = (𝑦𝐹𝑧)) |
82 | 81 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 = 𝑦 ∧ 𝑧 ∈ 𝑁) → (𝑤𝐹𝑧) = (𝑦𝐹𝑧)) |
83 | 80, 82 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 = 𝑦 ∧ 𝑧 ∈ 𝑁) → (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧) = (𝑦𝐹𝑧)) |
84 | 83 | mpteq2dva 4744 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑦 → (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧)) = (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧))) |
85 | 84 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑦 → (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)))) |
86 | 7, 85 | gsumsn 18354 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝐾 ∧ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧))) ∈ 𝐵) → (𝐺 Σg (𝑤 ∈ {𝑦} ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧))))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)))) |
87 | 67, 68, 77, 86 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝑤 ∈ {𝑦} ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧))))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)))) |
88 | 40 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → {𝑦} ∈ Fin) |
89 | 7, 8, 39, 88, 41, 50, 54 | gsumxp 18375 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))) = (𝐺 Σg (𝑤 ∈ {𝑦} ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧)))))) |
90 | | ovres 6800 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝑁) → (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧) = (𝑦𝐹𝑧)) |
91 | 90 | adantll 750 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧) = (𝑦𝐹𝑧)) |
92 | 91 | mpteq2dva 4744 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧)) = (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧))) |
93 | 92 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)))) |
94 | 87, 89, 93 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧)))) |
95 | 94 | mpteq2dva 4744 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) = (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧))))) |
96 | 95 | oveq2d 6666 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) = (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧)))))) |
97 | 7, 8, 4, 12, 16, 26, 28 | gsumxp 18375 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) = (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧)))))) |
98 | 96, 97 | eqtr4d 2659 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) = (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) |
99 | 98 | oveq2d 6666 |
. . . . 5
⊢ (𝜑 → ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) |
100 | 60, 65, 99 | 3eqtr3d 2664 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) |
101 | | tsmsxp.x |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁)))) ∈ 𝐿) |
102 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦)) |
103 | | sneq 4187 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
104 | 103 | xpeq1d 5138 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ({𝑥} × 𝑁) = ({𝑦} × 𝑁)) |
105 | 104 | reseq2d 5396 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝐹 ↾ ({𝑥} × 𝑁)) = (𝐹 ↾ ({𝑦} × 𝑁))) |
106 | 105 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁))) = (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) |
107 | 102, 106 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁)))) = ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) |
108 | 107 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁)))) ∈ 𝐿 ↔ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) ∈ 𝐿)) |
109 | 108 | rspccva 3308 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁)))) ∈ 𝐿 ∧ 𝑦 ∈ 𝐾) → ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) ∈ 𝐿) |
110 | 101, 109 | sylan 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) ∈ 𝐿) |
111 | | eqid 2622 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) = (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) |
112 | 110, 111 | fmptd 6385 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))):𝐾⟶𝐿) |
113 | | tsmsxp.l |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ 𝐽) |
114 | 113, 9 | elmapd 7871 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) ∈ (𝐿 ↑𝑚 𝐾) ↔ (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))):𝐾⟶𝐿)) |
115 | 112, 114 | mpbird 247 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) ∈ (𝐿 ↑𝑚 𝐾)) |
116 | | tsmsxp.6 |
. . . . 5
⊢ (𝜑 → ∀𝑔 ∈ (𝐿 ↑𝑚 𝐾)(𝐺 Σg 𝑔) ∈ 𝑇) |
117 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑔 = (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) → (𝐺 Σg 𝑔) = (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))))) |
118 | 117 | eleq1d 2686 |
. . . . . 6
⊢ (𝑔 = (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) → ((𝐺 Σg 𝑔) ∈ 𝑇 ↔ (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) ∈ 𝑇)) |
119 | 118 | rspcv 3305 |
. . . . 5
⊢ ((𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) ∈ (𝐿 ↑𝑚 𝐾) → (∀𝑔 ∈ (𝐿 ↑𝑚 𝐾)(𝐺 Σg 𝑔) ∈ 𝑇 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) ∈ 𝑇)) |
120 | 115, 116,
119 | sylc 65 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) ∈ 𝑇) |
121 | 100, 120 | eqeltrrd 2702 |
. . 3
⊢ (𝜑 → ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) ∈ 𝑇) |
122 | | tsmsxp.4 |
. . 3
⊢ (𝜑 → ∀𝑐 ∈ 𝑆 ∀𝑑 ∈ 𝑇 (𝑐 + 𝑑) ∈ 𝑈) |
123 | | oveq1 6657 |
. . . . 5
⊢ (𝑐 = (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) → (𝑐 + 𝑑) = ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + 𝑑)) |
124 | 123 | eleq1d 2686 |
. . . 4
⊢ (𝑐 = (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) → ((𝑐 + 𝑑) ∈ 𝑈 ↔ ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + 𝑑) ∈ 𝑈)) |
125 | | oveq2 6658 |
. . . . 5
⊢ (𝑑 = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + 𝑑) = ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))))) |
126 | 125 | eleq1d 2686 |
. . . 4
⊢ (𝑑 = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) → (((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + 𝑑) ∈ 𝑈 ↔ ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) ∈ 𝑈)) |
127 | 124, 126 | rspc2va 3323 |
. . 3
⊢ ((((𝐺 Σg
(𝐹 ↾ (𝐾 × 𝑁))) ∈ 𝑆 ∧ ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) ∈ 𝑇) ∧ ∀𝑐 ∈ 𝑆 ∀𝑑 ∈ 𝑇 (𝑐 + 𝑑) ∈ 𝑈) → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) ∈ 𝑈) |
128 | 38, 121, 122, 127 | syl21anc 1325 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) ∈ 𝑈) |
129 | 37, 128 | eqeltrrd 2702 |
1
⊢ (𝜑 → (𝐺 Σg (𝐻 ↾ 𝐾)) ∈ 𝑈) |