Step |
Hyp |
Ref |
Expression |
1 |
|
tsmsxp.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
tsmsxp.g |
⊢ ( 𝜑 → 𝐺 ∈ CMnd ) |
3 |
|
tsmsxp.2 |
⊢ ( 𝜑 → 𝐺 ∈ TopGrp ) |
4 |
|
tsmsxp.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
5 |
|
tsmsxp.c |
⊢ ( 𝜑 → 𝐶 ∈ 𝑊 ) |
6 |
|
tsmsxp.f |
⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 ) |
7 |
|
tsmsxp.h |
⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 ) |
8 |
|
tsmsxp.1 |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑗 ) ∈ ( 𝐺 tsums ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) |
9 |
|
tsmsxp.j |
⊢ 𝐽 = ( TopOpen ‘ 𝐺 ) |
10 |
|
tsmsxp.z |
⊢ 0 = ( 0g ‘ 𝐺 ) |
11 |
|
tsmsxp.p |
⊢ + = ( +g ‘ 𝐺 ) |
12 |
|
tsmsxp.m |
⊢ − = ( -g ‘ 𝐺 ) |
13 |
|
tsmsxp.l |
⊢ ( 𝜑 → 𝐿 ∈ 𝐽 ) |
14 |
|
tsmsxp.3 |
⊢ ( 𝜑 → 0 ∈ 𝐿 ) |
15 |
|
tsmsxp.k |
⊢ ( 𝜑 → 𝐾 ∈ ( 𝒫 𝐴 ∩ Fin ) ) |
16 |
|
tsmsxp.4 |
⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝑆 ∀ 𝑑 ∈ 𝑇 ( 𝑐 + 𝑑 ) ∈ 𝑈 ) |
17 |
|
tsmsxp.n |
⊢ ( 𝜑 → 𝑁 ∈ ( 𝒫 𝐶 ∩ Fin ) ) |
18 |
|
tsmsxp.s |
⊢ ( 𝜑 → 𝐷 ⊆ ( 𝐾 × 𝑁 ) ) |
19 |
|
tsmsxp.x |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑁 ) ) ) ) ∈ 𝐿 ) |
20 |
|
tsmsxp.5 |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ∈ 𝑆 ) |
21 |
|
tsmsxp.6 |
⊢ ( 𝜑 → ∀ 𝑔 ∈ ( 𝐿 ↑m 𝐾 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑇 ) |
22 |
|
tgpgrp |
⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp ) |
23 |
3 22
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ Grp ) |
24 |
|
isabl |
⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) ) |
25 |
23 2 24
|
sylanbrc |
⊢ ( 𝜑 → 𝐺 ∈ Abel ) |
26 |
15
|
elin2d |
⊢ ( 𝜑 → 𝐾 ∈ Fin ) |
27 |
17
|
elin2d |
⊢ ( 𝜑 → 𝑁 ∈ Fin ) |
28 |
|
xpfi |
⊢ ( ( 𝐾 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝐾 × 𝑁 ) ∈ Fin ) |
29 |
26 27 28
|
syl2anc |
⊢ ( 𝜑 → ( 𝐾 × 𝑁 ) ∈ Fin ) |
30 |
|
elfpw |
⊢ ( 𝐾 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝐾 ⊆ 𝐴 ∧ 𝐾 ∈ Fin ) ) |
31 |
30
|
simplbi |
⊢ ( 𝐾 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝐾 ⊆ 𝐴 ) |
32 |
15 31
|
syl |
⊢ ( 𝜑 → 𝐾 ⊆ 𝐴 ) |
33 |
|
elfpw |
⊢ ( 𝑁 ∈ ( 𝒫 𝐶 ∩ Fin ) ↔ ( 𝑁 ⊆ 𝐶 ∧ 𝑁 ∈ Fin ) ) |
34 |
33
|
simplbi |
⊢ ( 𝑁 ∈ ( 𝒫 𝐶 ∩ Fin ) → 𝑁 ⊆ 𝐶 ) |
35 |
17 34
|
syl |
⊢ ( 𝜑 → 𝑁 ⊆ 𝐶 ) |
36 |
|
xpss12 |
⊢ ( ( 𝐾 ⊆ 𝐴 ∧ 𝑁 ⊆ 𝐶 ) → ( 𝐾 × 𝑁 ) ⊆ ( 𝐴 × 𝐶 ) ) |
37 |
32 35 36
|
syl2anc |
⊢ ( 𝜑 → ( 𝐾 × 𝑁 ) ⊆ ( 𝐴 × 𝐶 ) ) |
38 |
6 37
|
fssresd |
⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) : ( 𝐾 × 𝑁 ) ⟶ 𝐵 ) |
39 |
38 29 14
|
fdmfifsupp |
⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) finSupp 0 ) |
40 |
1 10 2 29 38 39
|
gsumcl |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ∈ 𝐵 ) |
41 |
7 32
|
fssresd |
⊢ ( 𝜑 → ( 𝐻 ↾ 𝐾 ) : 𝐾 ⟶ 𝐵 ) |
42 |
41 26 14
|
fdmfifsupp |
⊢ ( 𝜑 → ( 𝐻 ↾ 𝐾 ) finSupp 0 ) |
43 |
1 10 2 15 41 42
|
gsumcl |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) ∈ 𝐵 ) |
44 |
1 11 12
|
ablpncan3 |
⊢ ( ( 𝐺 ∈ Abel ∧ ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ∈ 𝐵 ∧ ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) ∈ 𝐵 ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) + ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ) ) = ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) ) |
45 |
25 40 43 44
|
syl12anc |
⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) + ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ) ) = ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) ) |
46 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → 𝐺 ∈ CMnd ) |
47 |
|
snfi |
⊢ { 𝑦 } ∈ Fin |
48 |
27
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → 𝑁 ∈ Fin ) |
49 |
|
xpfi |
⊢ ( ( { 𝑦 } ∈ Fin ∧ 𝑁 ∈ Fin ) → ( { 𝑦 } × 𝑁 ) ∈ Fin ) |
50 |
47 48 49
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( { 𝑦 } × 𝑁 ) ∈ Fin ) |
51 |
6
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 ) |
52 |
32
|
sselda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → 𝑦 ∈ 𝐴 ) |
53 |
52
|
snssd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → { 𝑦 } ⊆ 𝐴 ) |
54 |
35
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → 𝑁 ⊆ 𝐶 ) |
55 |
|
xpss12 |
⊢ ( ( { 𝑦 } ⊆ 𝐴 ∧ 𝑁 ⊆ 𝐶 ) → ( { 𝑦 } × 𝑁 ) ⊆ ( 𝐴 × 𝐶 ) ) |
56 |
53 54 55
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( { 𝑦 } × 𝑁 ) ⊆ ( 𝐴 × 𝐶 ) ) |
57 |
51 56
|
fssresd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) : ( { 𝑦 } × 𝑁 ) ⟶ 𝐵 ) |
58 |
10
|
fvexi |
⊢ 0 ∈ V |
59 |
58
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → 0 ∈ V ) |
60 |
57 50 59
|
fdmfifsupp |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) finSupp 0 ) |
61 |
1 10 46 50 57 60
|
gsumcl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ∈ 𝐵 ) |
62 |
61
|
fmpttd |
⊢ ( 𝜑 → ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) : 𝐾 ⟶ 𝐵 ) |
63 |
|
eqid |
⊢ ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) = ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) |
64 |
|
ovexd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ∈ V ) |
65 |
63 26 64 14
|
fsuppmptdm |
⊢ ( 𝜑 → ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) finSupp 0 ) |
66 |
1 10 12 25 15 41 62 42 65
|
gsumsub |
⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝐻 ↾ 𝐾 ) ∘f − ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) ) = ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) ) ) |
67 |
|
fvexd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐻 ‘ 𝑦 ) ∈ V ) |
68 |
7 32
|
feqresmpt |
⊢ ( 𝜑 → ( 𝐻 ↾ 𝐾 ) = ( 𝑦 ∈ 𝐾 ↦ ( 𝐻 ‘ 𝑦 ) ) ) |
69 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) = ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) |
70 |
15 67 64 68 69
|
offval2 |
⊢ ( 𝜑 → ( ( 𝐻 ↾ 𝐾 ) ∘f − ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) = ( 𝑦 ∈ 𝐾 ↦ ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) ) |
71 |
70
|
oveq2d |
⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝐻 ↾ 𝐾 ) ∘f − ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) ) = ( 𝐺 Σg ( 𝑦 ∈ 𝐾 ↦ ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) ) ) |
72 |
|
cmnmnd |
⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd ) |
73 |
46 72
|
syl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → 𝐺 ∈ Mnd ) |
74 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → 𝑦 ∈ 𝐾 ) |
75 |
51
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 ∈ 𝑁 ) → 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 ) |
76 |
52
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 ∈ 𝑁 ) → 𝑦 ∈ 𝐴 ) |
77 |
54
|
sselda |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 ∈ 𝑁 ) → 𝑧 ∈ 𝐶 ) |
78 |
75 76 77
|
fovrnd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 ∈ 𝑁 ) → ( 𝑦 𝐹 𝑧 ) ∈ 𝐵 ) |
79 |
78
|
fmpttd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 𝐹 𝑧 ) ) : 𝑁 ⟶ 𝐵 ) |
80 |
|
eqid |
⊢ ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 𝐹 𝑧 ) ) = ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 𝐹 𝑧 ) ) |
81 |
|
ovexd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 ∈ 𝑁 ) → ( 𝑦 𝐹 𝑧 ) ∈ V ) |
82 |
80 48 81 59
|
fsuppmptdm |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 𝐹 𝑧 ) ) finSupp 0 ) |
83 |
1 10 46 48 79 82
|
gsumcl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 𝐹 𝑧 ) ) ) ∈ 𝐵 ) |
84 |
|
velsn |
⊢ ( 𝑤 ∈ { 𝑦 } ↔ 𝑤 = 𝑦 ) |
85 |
|
ovres |
⊢ ( ( 𝑤 ∈ { 𝑦 } ∧ 𝑧 ∈ 𝑁 ) → ( 𝑤 ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) 𝑧 ) = ( 𝑤 𝐹 𝑧 ) ) |
86 |
84 85
|
sylanbr |
⊢ ( ( 𝑤 = 𝑦 ∧ 𝑧 ∈ 𝑁 ) → ( 𝑤 ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) 𝑧 ) = ( 𝑤 𝐹 𝑧 ) ) |
87 |
|
oveq1 |
⊢ ( 𝑤 = 𝑦 → ( 𝑤 𝐹 𝑧 ) = ( 𝑦 𝐹 𝑧 ) ) |
88 |
87
|
adantr |
⊢ ( ( 𝑤 = 𝑦 ∧ 𝑧 ∈ 𝑁 ) → ( 𝑤 𝐹 𝑧 ) = ( 𝑦 𝐹 𝑧 ) ) |
89 |
86 88
|
eqtrd |
⊢ ( ( 𝑤 = 𝑦 ∧ 𝑧 ∈ 𝑁 ) → ( 𝑤 ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) 𝑧 ) = ( 𝑦 𝐹 𝑧 ) ) |
90 |
89
|
mpteq2dva |
⊢ ( 𝑤 = 𝑦 → ( 𝑧 ∈ 𝑁 ↦ ( 𝑤 ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) 𝑧 ) ) = ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 𝐹 𝑧 ) ) ) |
91 |
90
|
oveq2d |
⊢ ( 𝑤 = 𝑦 → ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑤 ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) 𝑧 ) ) ) = ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 𝐹 𝑧 ) ) ) ) |
92 |
1 91
|
gsumsn |
⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝐾 ∧ ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 𝐹 𝑧 ) ) ) ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑤 ∈ { 𝑦 } ↦ ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑤 ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) 𝑧 ) ) ) ) ) = ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 𝐹 𝑧 ) ) ) ) |
93 |
73 74 83 92
|
syl3anc |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐺 Σg ( 𝑤 ∈ { 𝑦 } ↦ ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑤 ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) 𝑧 ) ) ) ) ) = ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 𝐹 𝑧 ) ) ) ) |
94 |
47
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → { 𝑦 } ∈ Fin ) |
95 |
1 10 46 94 48 57 60
|
gsumxp |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) = ( 𝐺 Σg ( 𝑤 ∈ { 𝑦 } ↦ ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑤 ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) 𝑧 ) ) ) ) ) ) |
96 |
|
ovres |
⊢ ( ( 𝑦 ∈ 𝐾 ∧ 𝑧 ∈ 𝑁 ) → ( 𝑦 ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) 𝑧 ) = ( 𝑦 𝐹 𝑧 ) ) |
97 |
96
|
adantll |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 ∈ 𝑁 ) → ( 𝑦 ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) 𝑧 ) = ( 𝑦 𝐹 𝑧 ) ) |
98 |
97
|
mpteq2dva |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) 𝑧 ) ) = ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 𝐹 𝑧 ) ) ) |
99 |
98
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) 𝑧 ) ) ) = ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 𝐹 𝑧 ) ) ) ) |
100 |
93 95 99
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) = ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) 𝑧 ) ) ) ) |
101 |
100
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) = ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) 𝑧 ) ) ) ) ) |
102 |
101
|
oveq2d |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) = ( 𝐺 Σg ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) 𝑧 ) ) ) ) ) ) |
103 |
1 10 2 26 27 38 39
|
gsumxp |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) = ( 𝐺 Σg ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝑧 ∈ 𝑁 ↦ ( 𝑦 ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) 𝑧 ) ) ) ) ) ) |
104 |
102 103
|
eqtr4d |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ) |
105 |
104
|
oveq2d |
⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝑦 ∈ 𝐾 ↦ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) ) = ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ) ) |
106 |
66 71 105
|
3eqtr3d |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑦 ∈ 𝐾 ↦ ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) ) = ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ) ) |
107 |
|
oveq2 |
⊢ ( 𝑔 = ( 𝑦 ∈ 𝐾 ↦ ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) → ( 𝐺 Σg 𝑔 ) = ( 𝐺 Σg ( 𝑦 ∈ 𝐾 ↦ ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) ) ) |
108 |
107
|
eleq1d |
⊢ ( 𝑔 = ( 𝑦 ∈ 𝐾 ↦ ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) → ( ( 𝐺 Σg 𝑔 ) ∈ 𝑇 ↔ ( 𝐺 Σg ( 𝑦 ∈ 𝐾 ↦ ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) ) ∈ 𝑇 ) ) |
109 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑦 ) ) |
110 |
|
sneq |
⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } ) |
111 |
110
|
xpeq1d |
⊢ ( 𝑥 = 𝑦 → ( { 𝑥 } × 𝑁 ) = ( { 𝑦 } × 𝑁 ) ) |
112 |
111
|
reseq2d |
⊢ ( 𝑥 = 𝑦 → ( 𝐹 ↾ ( { 𝑥 } × 𝑁 ) ) = ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) |
113 |
112
|
oveq2d |
⊢ ( 𝑥 = 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑁 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) |
114 |
109 113
|
oveq12d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑁 ) ) ) ) = ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) |
115 |
114
|
eleq1d |
⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑁 ) ) ) ) ∈ 𝐿 ↔ ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ∈ 𝐿 ) ) |
116 |
115
|
rspccva |
⊢ ( ( ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑁 ) ) ) ) ∈ 𝐿 ∧ 𝑦 ∈ 𝐾 ) → ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ∈ 𝐿 ) |
117 |
19 116
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ∈ 𝐿 ) |
118 |
117
|
fmpttd |
⊢ ( 𝜑 → ( 𝑦 ∈ 𝐾 ↦ ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) : 𝐾 ⟶ 𝐿 ) |
119 |
13 15
|
elmapd |
⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐾 ↦ ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) ∈ ( 𝐿 ↑m 𝐾 ) ↔ ( 𝑦 ∈ 𝐾 ↦ ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) : 𝐾 ⟶ 𝐿 ) ) |
120 |
118 119
|
mpbird |
⊢ ( 𝜑 → ( 𝑦 ∈ 𝐾 ↦ ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) ∈ ( 𝐿 ↑m 𝐾 ) ) |
121 |
108 21 120
|
rspcdva |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑦 ∈ 𝐾 ↦ ( ( 𝐻 ‘ 𝑦 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑦 } × 𝑁 ) ) ) ) ) ) ∈ 𝑇 ) |
122 |
106 121
|
eqeltrrd |
⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ) ∈ 𝑇 ) |
123 |
|
oveq1 |
⊢ ( 𝑐 = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) → ( 𝑐 + 𝑑 ) = ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) + 𝑑 ) ) |
124 |
123
|
eleq1d |
⊢ ( 𝑐 = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) → ( ( 𝑐 + 𝑑 ) ∈ 𝑈 ↔ ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) + 𝑑 ) ∈ 𝑈 ) ) |
125 |
|
oveq2 |
⊢ ( 𝑑 = ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) + 𝑑 ) = ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) + ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ) ) ) |
126 |
125
|
eleq1d |
⊢ ( 𝑑 = ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ) → ( ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) + 𝑑 ) ∈ 𝑈 ↔ ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) + ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ) ) ∈ 𝑈 ) ) |
127 |
124 126
|
rspc2va |
⊢ ( ( ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ∈ 𝑆 ∧ ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ) ∈ 𝑇 ) ∧ ∀ 𝑐 ∈ 𝑆 ∀ 𝑑 ∈ 𝑇 ( 𝑐 + 𝑑 ) ∈ 𝑈 ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) + ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ) ) ∈ 𝑈 ) |
128 |
20 122 16 127
|
syl21anc |
⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) + ( ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) − ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ) ) ∈ 𝑈 ) |
129 |
45 128
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) ∈ 𝑈 ) |