Step | Hyp | Ref
| Expression |
1 | | tsmsxp.2 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ TopGrp) |
2 | | tgpgrp 22102 |
. . . . 5
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ Grp) |
4 | | tsmsxp.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ CMnd) |
5 | | isabl 18404 |
. . . 4
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) |
6 | 3, 4, 5 | sylanbrc 572 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Abel) |
7 | | tsmsxp.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
8 | | tsmsxp.z |
. . . 4
⊢ 0 =
(0g‘𝐺) |
9 | | tsmsxp.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐴 ∩ Fin)) |
10 | | elfpw 8424 |
. . . . . . 7
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝐾 ⊆ 𝐴 ∧ 𝐾 ∈ Fin)) |
11 | 10 | simprbi 484 |
. . . . . 6
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ∈ Fin) |
12 | 9, 11 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ Fin) |
13 | | tsmsxp.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (𝒫 𝐶 ∩ Fin)) |
14 | | elfpw 8424 |
. . . . . . 7
⊢ (𝑁 ∈ (𝒫 𝐶 ∩ Fin) ↔ (𝑁 ⊆ 𝐶 ∧ 𝑁 ∈ Fin)) |
15 | 14 | simprbi 484 |
. . . . . 6
⊢ (𝑁 ∈ (𝒫 𝐶 ∩ Fin) → 𝑁 ∈ Fin) |
16 | 13, 15 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ Fin) |
17 | | xpfi 8387 |
. . . . 5
⊢ ((𝐾 ∈ Fin ∧ 𝑁 ∈ Fin) → (𝐾 × 𝑁) ∈ Fin) |
18 | 12, 16, 17 | syl2anc 573 |
. . . 4
⊢ (𝜑 → (𝐾 × 𝑁) ∈ Fin) |
19 | | tsmsxp.f |
. . . . 5
⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
20 | 10 | simplbi 485 |
. . . . . . 7
⊢ (𝐾 ∈ (𝒫 𝐴 ∩ Fin) → 𝐾 ⊆ 𝐴) |
21 | 9, 20 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐾 ⊆ 𝐴) |
22 | 14 | simplbi 485 |
. . . . . . 7
⊢ (𝑁 ∈ (𝒫 𝐶 ∩ Fin) → 𝑁 ⊆ 𝐶) |
23 | 13, 22 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑁 ⊆ 𝐶) |
24 | | xpss12 5264 |
. . . . . 6
⊢ ((𝐾 ⊆ 𝐴 ∧ 𝑁 ⊆ 𝐶) → (𝐾 × 𝑁) ⊆ (𝐴 × 𝐶)) |
25 | 21, 23, 24 | syl2anc 573 |
. . . . 5
⊢ (𝜑 → (𝐾 × 𝑁) ⊆ (𝐴 × 𝐶)) |
26 | 19, 25 | fssresd 6211 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ (𝐾 × 𝑁)):(𝐾 × 𝑁)⟶𝐵) |
27 | | tsmsxp.3 |
. . . . 5
⊢ (𝜑 → 0 ∈ 𝐿) |
28 | 26, 18, 27 | fdmfifsupp 8441 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ (𝐾 × 𝑁)) finSupp 0 ) |
29 | 7, 8, 4, 18, 26, 28 | gsumcl 18523 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) ∈ 𝐵) |
30 | | tsmsxp.h |
. . . . 5
⊢ (𝜑 → 𝐻:𝐴⟶𝐵) |
31 | 30, 21 | fssresd 6211 |
. . . 4
⊢ (𝜑 → (𝐻 ↾ 𝐾):𝐾⟶𝐵) |
32 | 31, 12, 27 | fdmfifsupp 8441 |
. . . 4
⊢ (𝜑 → (𝐻 ↾ 𝐾) finSupp 0 ) |
33 | 7, 8, 4, 12, 31, 32 | gsumcl 18523 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐻 ↾ 𝐾)) ∈ 𝐵) |
34 | | tsmsxp.p |
. . . 4
⊢ + =
(+g‘𝐺) |
35 | | tsmsxp.m |
. . . 4
⊢ − =
(-g‘𝐺) |
36 | 7, 34, 35 | ablpncan3 18429 |
. . 3
⊢ ((𝐺 ∈ Abel ∧ ((𝐺 Σg
(𝐹 ↾ (𝐾 × 𝑁))) ∈ 𝐵 ∧ (𝐺 Σg (𝐻 ↾ 𝐾)) ∈ 𝐵)) → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) = (𝐺 Σg (𝐻 ↾ 𝐾))) |
37 | 6, 29, 33, 36 | syl12anc 1474 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) = (𝐺 Σg (𝐻 ↾ 𝐾))) |
38 | | tsmsxp.5 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) ∈ 𝑆) |
39 | 4 | adantr 466 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝐺 ∈ CMnd) |
40 | | snfi 8194 |
. . . . . . . . 9
⊢ {𝑦} ∈ Fin |
41 | 16 | adantr 466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝑁 ∈ Fin) |
42 | | xpfi 8387 |
. . . . . . . . 9
⊢ (({𝑦} ∈ Fin ∧ 𝑁 ∈ Fin) → ({𝑦} × 𝑁) ∈ Fin) |
43 | 40, 41, 42 | sylancr 575 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → ({𝑦} × 𝑁) ∈ Fin) |
44 | 19 | adantr 466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
45 | 21 | sselda 3752 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝑦 ∈ 𝐴) |
46 | 45 | snssd 4475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → {𝑦} ⊆ 𝐴) |
47 | 23 | adantr 466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝑁 ⊆ 𝐶) |
48 | | xpss12 5264 |
. . . . . . . . . 10
⊢ (({𝑦} ⊆ 𝐴 ∧ 𝑁 ⊆ 𝐶) → ({𝑦} × 𝑁) ⊆ (𝐴 × 𝐶)) |
49 | 46, 47, 48 | syl2anc 573 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → ({𝑦} × 𝑁) ⊆ (𝐴 × 𝐶)) |
50 | 44, 49 | fssresd 6211 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹 ↾ ({𝑦} × 𝑁)):({𝑦} × 𝑁)⟶𝐵) |
51 | | fvex 6342 |
. . . . . . . . . . 11
⊢
(0g‘𝐺) ∈ V |
52 | 8, 51 | eqeltri 2846 |
. . . . . . . . . 10
⊢ 0 ∈
V |
53 | 52 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 0 ∈ V) |
54 | 50, 43, 53 | fdmfifsupp 8441 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐹 ↾ ({𝑦} × 𝑁)) finSupp 0 ) |
55 | 7, 8, 39, 43, 50, 54 | gsumcl 18523 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))) ∈ 𝐵) |
56 | | eqid 2771 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) = (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) |
57 | 55, 56 | fmptd 6527 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))):𝐾⟶𝐵) |
58 | | ovexd 6825 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))) ∈ V) |
59 | 56, 12, 58, 27 | fsuppmptdm 8442 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) finSupp 0 ) |
60 | 7, 8, 35, 6, 12, 31, 57, 32, 59 | gsumsub 18555 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg ((𝐻 ↾ 𝐾) ∘𝑓 − (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))))) |
61 | | fvexd 6344 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐻‘𝑦) ∈ V) |
62 | 30, 21 | feqresmpt 6392 |
. . . . . . 7
⊢ (𝜑 → (𝐻 ↾ 𝐾) = (𝑦 ∈ 𝐾 ↦ (𝐻‘𝑦))) |
63 | | eqidd 2772 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) = (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) |
64 | 12, 61, 58, 62, 63 | offval2 7061 |
. . . . . 6
⊢ (𝜑 → ((𝐻 ↾ 𝐾) ∘𝑓 − (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) = (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) |
65 | 64 | oveq2d 6809 |
. . . . 5
⊢ (𝜑 → (𝐺 Σg ((𝐻 ↾ 𝐾) ∘𝑓 − (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) = (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))))) |
66 | | cmnmnd 18415 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
67 | 39, 66 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝐺 ∈ Mnd) |
68 | | simpr 471 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → 𝑦 ∈ 𝐾) |
69 | 44 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → 𝐹:(𝐴 × 𝐶)⟶𝐵) |
70 | 45 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → 𝑦 ∈ 𝐴) |
71 | 47 | sselda 3752 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → 𝑧 ∈ 𝐶) |
72 | 69, 70, 71 | fovrnd 6953 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → (𝑦𝐹𝑧) ∈ 𝐵) |
73 | | eqid 2771 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)) = (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)) |
74 | 72, 73 | fmptd 6527 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)):𝑁⟶𝐵) |
75 | | ovexd 6825 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → (𝑦𝐹𝑧) ∈ V) |
76 | 73, 41, 75, 53 | fsuppmptdm 8442 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)) finSupp 0 ) |
77 | 7, 8, 39, 41, 74, 76 | gsumcl 18523 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧))) ∈ 𝐵) |
78 | | velsn 4332 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {𝑦} ↔ 𝑤 = 𝑦) |
79 | | ovres 6947 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ {𝑦} ∧ 𝑧 ∈ 𝑁) → (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧) = (𝑤𝐹𝑧)) |
80 | 78, 79 | sylanbr 571 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 = 𝑦 ∧ 𝑧 ∈ 𝑁) → (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧) = (𝑤𝐹𝑧)) |
81 | | oveq1 6800 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑦 → (𝑤𝐹𝑧) = (𝑦𝐹𝑧)) |
82 | 81 | adantr 466 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 = 𝑦 ∧ 𝑧 ∈ 𝑁) → (𝑤𝐹𝑧) = (𝑦𝐹𝑧)) |
83 | 80, 82 | eqtrd 2805 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 = 𝑦 ∧ 𝑧 ∈ 𝑁) → (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧) = (𝑦𝐹𝑧)) |
84 | 83 | mpteq2dva 4878 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑦 → (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧)) = (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧))) |
85 | 84 | oveq2d 6809 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑦 → (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)))) |
86 | 7, 85 | gsumsn 18561 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝐾 ∧ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧))) ∈ 𝐵) → (𝐺 Σg (𝑤 ∈ {𝑦} ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧))))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)))) |
87 | 67, 68, 77, 86 | syl3anc 1476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝑤 ∈ {𝑦} ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧))))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)))) |
88 | 40 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → {𝑦} ∈ Fin) |
89 | 7, 8, 39, 88, 41, 50, 54 | gsumxp 18582 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))) = (𝐺 Σg (𝑤 ∈ {𝑦} ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑤(𝐹 ↾ ({𝑦} × 𝑁))𝑧)))))) |
90 | | ovres 6947 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝑁) → (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧) = (𝑦𝐹𝑧)) |
91 | 90 | adantll 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 ∈ 𝑁) → (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧) = (𝑦𝐹𝑧)) |
92 | 91 | mpteq2dva 4878 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧)) = (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧))) |
93 | 92 | oveq2d 6809 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦𝐹𝑧)))) |
94 | 87, 89, 93 | 3eqtr4d 2815 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))) = (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧)))) |
95 | 94 | mpteq2dva 4878 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) = (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧))))) |
96 | 95 | oveq2d 6809 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) = (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧)))))) |
97 | 7, 8, 4, 12, 16, 26, 28 | gsumxp 18582 |
. . . . . . 7
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) = (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝑧 ∈ 𝑁 ↦ (𝑦(𝐹 ↾ (𝐾 × 𝑁))𝑧)))))) |
98 | 96, 97 | eqtr4d 2808 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) = (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) |
99 | 98 | oveq2d 6809 |
. . . . 5
⊢ (𝜑 → ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝑦 ∈ 𝐾 ↦ (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) |
100 | 60, 65, 99 | 3eqtr3d 2813 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) |
101 | | oveq2 6801 |
. . . . . 6
⊢ (𝑔 = (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) → (𝐺 Σg 𝑔) = (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))))) |
102 | 101 | eleq1d 2835 |
. . . . 5
⊢ (𝑔 = (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) → ((𝐺 Σg 𝑔) ∈ 𝑇 ↔ (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) ∈ 𝑇)) |
103 | | tsmsxp.6 |
. . . . 5
⊢ (𝜑 → ∀𝑔 ∈ (𝐿 ↑𝑚 𝐾)(𝐺 Σg 𝑔) ∈ 𝑇) |
104 | | tsmsxp.x |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁)))) ∈ 𝐿) |
105 | | fveq2 6332 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦)) |
106 | | sneq 4326 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
107 | 106 | xpeq1d 5278 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ({𝑥} × 𝑁) = ({𝑦} × 𝑁)) |
108 | 107 | reseq2d 5534 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝐹 ↾ ({𝑥} × 𝑁)) = (𝐹 ↾ ({𝑦} × 𝑁))) |
109 | 108 | oveq2d 6809 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁))) = (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) |
110 | 105, 109 | oveq12d 6811 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁)))) = ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) |
111 | 110 | eleq1d 2835 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁)))) ∈ 𝐿 ↔ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) ∈ 𝐿)) |
112 | 111 | rspccva 3459 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐾 ((𝐻‘𝑥) − (𝐺 Σg (𝐹 ↾ ({𝑥} × 𝑁)))) ∈ 𝐿 ∧ 𝑦 ∈ 𝐾) → ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) ∈ 𝐿) |
113 | 104, 112 | sylan 569 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))) ∈ 𝐿) |
114 | | eqid 2771 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) = (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) |
115 | 113, 114 | fmptd 6527 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))):𝐾⟶𝐿) |
116 | | tsmsxp.l |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ 𝐽) |
117 | 116, 9 | elmapd 8023 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) ∈ (𝐿 ↑𝑚 𝐾) ↔ (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))):𝐾⟶𝐿)) |
118 | 115, 117 | mpbird 247 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁))))) ∈ (𝐿 ↑𝑚 𝐾)) |
119 | 102, 103,
118 | rspcdva 3466 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝐾 ↦ ((𝐻‘𝑦) − (𝐺 Σg (𝐹 ↾ ({𝑦} × 𝑁)))))) ∈ 𝑇) |
120 | 100, 119 | eqeltrrd 2851 |
. . 3
⊢ (𝜑 → ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) ∈ 𝑇) |
121 | | tsmsxp.4 |
. . 3
⊢ (𝜑 → ∀𝑐 ∈ 𝑆 ∀𝑑 ∈ 𝑇 (𝑐 + 𝑑) ∈ 𝑈) |
122 | | oveq1 6800 |
. . . . 5
⊢ (𝑐 = (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) → (𝑐 + 𝑑) = ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + 𝑑)) |
123 | 122 | eleq1d 2835 |
. . . 4
⊢ (𝑐 = (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) → ((𝑐 + 𝑑) ∈ 𝑈 ↔ ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + 𝑑) ∈ 𝑈)) |
124 | | oveq2 6801 |
. . . . 5
⊢ (𝑑 = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + 𝑑) = ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))))) |
125 | 124 | eleq1d 2835 |
. . . 4
⊢ (𝑑 = ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) → (((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + 𝑑) ∈ 𝑈 ↔ ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) ∈ 𝑈)) |
126 | 123, 125 | rspc2va 3473 |
. . 3
⊢ ((((𝐺 Σg
(𝐹 ↾ (𝐾 × 𝑁))) ∈ 𝑆 ∧ ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁)))) ∈ 𝑇) ∧ ∀𝑐 ∈ 𝑆 ∀𝑑 ∈ 𝑇 (𝑐 + 𝑑) ∈ 𝑈) → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) ∈ 𝑈) |
127 | 38, 120, 121, 126 | syl21anc 1475 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))) + ((𝐺 Σg (𝐻 ↾ 𝐾)) − (𝐺 Σg (𝐹 ↾ (𝐾 × 𝑁))))) ∈ 𝑈) |
128 | 37, 127 | eqeltrrd 2851 |
1
⊢ (𝜑 → (𝐺 Σg (𝐻 ↾ 𝐾)) ∈ 𝑈) |