Metamath Proof Explorer

Theorem tsmsxplem2

Description: Lemma for tsmsxp . (Contributed by Mario Carneiro, 21-Sep-2015)

Ref Expression
Hypotheses tsmsxp.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
tsmsxp.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tsmsxp.2 ⊢ ( 𝜑 → 𝐺 ∈ TopGrp )
tsmsxp.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tsmsxp.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
tsmsxp.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 )
tsmsxp.h ⊢ ( 𝜑 → 𝐻 : 𝐴 ⟶ 𝐵 )
tsmsxp.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑗 ) ∈ ( 𝐺 tsums ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ) )
tsmsxp.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
tsmsxp.z ⊢ 0 = ( 0g ‘ 𝐺 )
tsmsxp.p ⊢ + = ( +g ‘ 𝐺 )
tsmsxp.m ⊢ − = ( -g ‘ 𝐺 )
tsmsxp.l ⊢ ( 𝜑 → 𝐿 ∈ 𝐽 )
tsmsxp.3 ⊢ ( 𝜑 → 0 ∈ 𝐿 )
tsmsxp.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝒫 𝐴 ∩ Fin ) )
tsmsxp.4 ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝑆 ∀ 𝑑 ∈ 𝑇 ( 𝑐 + 𝑑 ) ∈ 𝑈 )
tsmsxp.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝒫 𝐶 ∩ Fin ) )
tsmsxp.s ⊢ ( 𝜑 → 𝐷 ⊆ ( 𝐾 × 𝑁 ) )
tsmsxp.x ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑁 ) ) ) ) ∈ 𝐿 )
tsmsxp.5 ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐾 × 𝑁 ) ) ) ∈ 𝑆 )
tsmsxp.6 ⊢ ( 𝜑 → ∀ 𝑔 ∈ ( 𝐿 ↑m 𝐾 ) ( 𝐺 Σg 𝑔 ) ∈ 𝑇 )
Assertion tsmsxplem2 ( 𝜑 → ( 𝐺 Σg ( 𝐻 ↾ 𝐾 ) ) ∈ 𝑈 )

Proof

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 fovcdmd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ 𝑧 ∈ 𝑁 ) → ( 𝑦 𝐹 𝑧 ) ∈ 𝐵 )
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 ( 𝐻 ↾ 𝐾 ) ) ∈ 𝑈 )