Metamath Proof Explorer

Theorem tsmsxplem1

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.ks ⊢ ( 𝜑 → dom 𝐷 ⊆ 𝐾 )
tsmsxp.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) )
Assertion tsmsxplem1 ( 𝜑 → ∃ 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ran 𝐷 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σ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.ks ⊢ ( 𝜑 → dom 𝐷 ⊆ 𝐾 )
17 tsmsxp.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) )
18 15 elin2d ⊢ ( 𝜑 → 𝐾 ∈ Fin )
19 elfpw ⊢ ( 𝐾 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝐾 ⊆ 𝐴 ∧ 𝐾 ∈ Fin ) )
20 19 simplbi ⊢ ( 𝐾 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝐾 ⊆ 𝐴 )
21 15 20 syl ⊢ ( 𝜑 → 𝐾 ⊆ 𝐴 )
22 21 sselda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) → 𝑗 ∈ 𝐴 )
23 eqid ⊢ ( 𝒫 𝐶 ∩ Fin ) = ( 𝒫 𝐶 ∩ Fin )
24 2 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐺 ∈ CMnd )
25 tgptps ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopSp )
26 3 25 syl ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐺 ∈ TopSp )
28 5 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑊 )
29 fovrn ⊢ ( ( 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
30 6 29 syl3an1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
31 30 3expa ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐶 ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
32 31 fmpttd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) : 𝐶 ⟶ 𝐵 )
33 df-ima ⊢ ( ( 𝑔 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) “ 𝐿 ) = ran ( ( 𝑔 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ↾ 𝐿 )
34 9 1 tgptopon ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
35 3 34 syl ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
36 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝐿 ∈ 𝐽 ) → 𝐿 ⊆ 𝐵 )
37 35 13 36 syl2anc ⊢ ( 𝜑 → 𝐿 ⊆ 𝐵 )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐿 ⊆ 𝐵 )
39 38 resmptd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑔 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ↾ 𝐿 ) = ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) )
40 39 rneqd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ran ( ( 𝑔 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ↾ 𝐿 ) = ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) )
41 33 40 eqtrid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑔 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) “ 𝐿 ) = ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) )
42 7 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑗 ) ∈ 𝐵 )
43 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
44 1 11 43 12 grpsubval ⊢ ( ( ( 𝐻 ‘ 𝑗 ) ∈ 𝐵 ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) = ( ( 𝐻 ‘ 𝑗 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ) )
45 42 44 sylan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) = ( ( 𝐻 ‘ 𝑗 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ) )
46 45 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑔 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) = ( 𝑔 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ) ) )
47 tgpgrp ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ Grp )
48 3 47 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
49 48 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐺 ∈ Grp )
50 1 43 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑔 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ∈ 𝐵 )
51 49 50 sylan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑔 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ∈ 𝐵 )
52 1 43 grpinvf ⊢ ( 𝐺 ∈ Grp → ( invg ‘ 𝐺 ) : 𝐵 ⟶ 𝐵 )
53 49 52 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( invg ‘ 𝐺 ) : 𝐵 ⟶ 𝐵 )
54 53 feqmptd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( invg ‘ 𝐺 ) = ( 𝑔 ∈ 𝐵 ↦ ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ) )
55 eqidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) + 𝑦 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) + 𝑦 ) ) )
56 oveq2 ⊢ ( 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) → ( ( 𝐻 ‘ 𝑗 ) + 𝑦 ) = ( ( 𝐻 ‘ 𝑗 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ) )
57 51 54 55 56 fmptco ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) + 𝑦 ) ) ∘ ( invg ‘ 𝐺 ) ) = ( 𝑔 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) + ( ( invg ‘ 𝐺 ) ‘ 𝑔 ) ) ) )
58 46 57 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑔 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) = ( ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) + 𝑦 ) ) ∘ ( invg ‘ 𝐺 ) ) )
59 3 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐺 ∈ TopGrp )
60 9 43 grpinvhmeo ⊢ ( 𝐺 ∈ TopGrp → ( invg ‘ 𝐺 ) ∈ ( 𝐽 Homeo 𝐽 ) )
61 59 60 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( invg ‘ 𝐺 ) ∈ ( 𝐽 Homeo 𝐽 ) )
62 eqid ⊢ ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) + 𝑦 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) + 𝑦 ) )
63 62 1 11 9 tgplacthmeo ⊢ ( ( 𝐺 ∈ TopGrp ∧ ( 𝐻 ‘ 𝑗 ) ∈ 𝐵 ) → ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) + 𝑦 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
64 59 42 63 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) + 𝑦 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
65 hmeoco ⊢ ( ( ( invg ‘ 𝐺 ) ∈ ( 𝐽 Homeo 𝐽 ) ∧ ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) + 𝑦 ) ) ∈ ( 𝐽 Homeo 𝐽 ) ) → ( ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) + 𝑦 ) ) ∘ ( invg ‘ 𝐺 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
66 61 64 65 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑦 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) + 𝑦 ) ) ∘ ( invg ‘ 𝐺 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
67 58 66 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑔 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ∈ ( 𝐽 Homeo 𝐽 ) )
68 13 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐿 ∈ 𝐽 )
69 hmeoima ⊢ ( ( ( 𝑔 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ∈ ( 𝐽 Homeo 𝐽 ) ∧ 𝐿 ∈ 𝐽 ) → ( ( 𝑔 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) “ 𝐿 ) ∈ 𝐽 )
70 67 68 69 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑔 ∈ 𝐵 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) “ 𝐿 ) ∈ 𝐽 )
71 41 70 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ∈ 𝐽 )
72 1 10 12 grpsubid1 ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐻 ‘ 𝑗 ) ∈ 𝐵 ) → ( ( 𝐻 ‘ 𝑗 ) − 0 ) = ( 𝐻 ‘ 𝑗 ) )
73 49 42 72 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑗 ) − 0 ) = ( 𝐻 ‘ 𝑗 ) )
74 14 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 0 ∈ 𝐿 )
75 ovex ⊢ ( ( 𝐻 ‘ 𝑗 ) − 0 ) ∈ V
76 eqid ⊢ ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) = ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) )
77 oveq2 ⊢ ( 𝑔 = 0 → ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) = ( ( 𝐻 ‘ 𝑗 ) − 0 ) )
78 76 77 elrnmpt1s ⊢ ( ( 0 ∈ 𝐿 ∧ ( ( 𝐻 ‘ 𝑗 ) − 0 ) ∈ V ) → ( ( 𝐻 ‘ 𝑗 ) − 0 ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) )
79 74 75 78 sylancl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑗 ) − 0 ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) )
80 73 79 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑗 ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) )
81 1 9 23 24 27 28 32 8 71 80 tsmsi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ∃ 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) )
82 22 81 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) → ∃ 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) )
83 82 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐾 ∃ 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) )
84 sseq1 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑗 ) → ( 𝑦 ⊆ 𝑧 ↔ ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 ) )
85 84 imbi1d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑗 ) → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ↔ ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ) )
86 85 ralbidv ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑗 ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ↔ ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ) )
87 86 ac6sfi ⊢ ( ( 𝐾 ∈ Fin ∧ ∀ 𝑗 ∈ 𝐾 ∃ 𝑦 ∈ ( 𝒫 𝐶 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ) → ∃ 𝑓 ( 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ∧ ∀ 𝑗 ∈ 𝐾 ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ) )
88 18 83 87 syl2anc ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ∧ ∀ 𝑗 ∈ 𝐾 ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ) )
89 frn ⊢ ( 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) → ran 𝑓 ⊆ ( 𝒫 𝐶 ∩ Fin ) )
90 89 adantl ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ran 𝑓 ⊆ ( 𝒫 𝐶 ∩ Fin ) )
91 inss1 ⊢ ( 𝒫 𝐶 ∩ Fin ) ⊆ 𝒫 𝐶
92 90 91 sstrdi ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ran 𝑓 ⊆ 𝒫 𝐶 )
93 sspwuni ⊢ ( ran 𝑓 ⊆ 𝒫 𝐶 ↔ ∪ ran 𝑓 ⊆ 𝐶 )
94 92 93 sylib ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ∪ ran 𝑓 ⊆ 𝐶 )
95 elfpw ⊢ ( 𝐷 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) ↔ ( 𝐷 ⊆ ( 𝐴 × 𝐶 ) ∧ 𝐷 ∈ Fin ) )
96 95 simplbi ⊢ ( 𝐷 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) → 𝐷 ⊆ ( 𝐴 × 𝐶 ) )
97 rnss ⊢ ( 𝐷 ⊆ ( 𝐴 × 𝐶 ) → ran 𝐷 ⊆ ran ( 𝐴 × 𝐶 ) )
98 17 96 97 3syl ⊢ ( 𝜑 → ran 𝐷 ⊆ ran ( 𝐴 × 𝐶 ) )
99 rnxpss ⊢ ran ( 𝐴 × 𝐶 ) ⊆ 𝐶
100 98 99 sstrdi ⊢ ( 𝜑 → ran 𝐷 ⊆ 𝐶 )
101 100 adantr ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ran 𝐷 ⊆ 𝐶 )
102 94 101 unssd ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ∪ ran 𝑓 ∪ ran 𝐷 ) ⊆ 𝐶 )
103 18 adantr ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → 𝐾 ∈ Fin )
104 ffn ⊢ ( 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) → 𝑓 Fn 𝐾 )
105 104 adantl ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → 𝑓 Fn 𝐾 )
106 dffn4 ⊢ ( 𝑓 Fn 𝐾 ↔ 𝑓 : 𝐾 –onto→ ran 𝑓 )
107 105 106 sylib ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → 𝑓 : 𝐾 –onto→ ran 𝑓 )
108 fofi ⊢ ( ( 𝐾 ∈ Fin ∧ 𝑓 : 𝐾 –onto→ ran 𝑓 ) → ran 𝑓 ∈ Fin )
109 103 107 108 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ran 𝑓 ∈ Fin )
110 inss2 ⊢ ( 𝒫 𝐶 ∩ Fin ) ⊆ Fin
111 90 110 sstrdi ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ran 𝑓 ⊆ Fin )
112 unifi ⊢ ( ( ran 𝑓 ∈ Fin ∧ ran 𝑓 ⊆ Fin ) → ∪ ran 𝑓 ∈ Fin )
113 109 111 112 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ∪ ran 𝑓 ∈ Fin )
114 elinel2 ⊢ ( 𝐷 ∈ ( 𝒫 ( 𝐴 × 𝐶 ) ∩ Fin ) → 𝐷 ∈ Fin )
115 rnfi ⊢ ( 𝐷 ∈ Fin → ran 𝐷 ∈ Fin )
116 17 114 115 3syl ⊢ ( 𝜑 → ran 𝐷 ∈ Fin )
117 116 adantr ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ran 𝐷 ∈ Fin )
118 unfi ⊢ ( ( ∪ ran 𝑓 ∈ Fin ∧ ran 𝐷 ∈ Fin ) → ( ∪ ran 𝑓 ∪ ran 𝐷 ) ∈ Fin )
119 113 117 118 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ∪ ran 𝑓 ∪ ran 𝐷 ) ∈ Fin )
120 elfpw ⊢ ( ( ∪ ran 𝑓 ∪ ran 𝐷 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ↔ ( ( ∪ ran 𝑓 ∪ ran 𝐷 ) ⊆ 𝐶 ∧ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ∈ Fin ) )
121 102 119 120 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ∪ ran 𝑓 ∪ ran 𝐷 ) ∈ ( 𝒫 𝐶 ∩ Fin ) )
122 121 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ∧ ∀ 𝑗 ∈ 𝐾 ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ) ) → ( ∪ ran 𝑓 ∪ ran 𝐷 ) ∈ ( 𝒫 𝐶 ∩ Fin ) )
123 ssun2 ⊢ ran 𝐷 ⊆ ( ∪ ran 𝑓 ∪ ran 𝐷 )
124 123 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ∧ ∀ 𝑗 ∈ 𝐾 ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ) ) → ran 𝐷 ⊆ ( ∪ ran 𝑓 ∪ ran 𝐷 ) )
125 121 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ∪ ran 𝑓 ∪ ran 𝐷 ) ∈ ( 𝒫 𝐶 ∩ Fin ) )
126 fvssunirn ⊢ ( 𝑓 ‘ 𝑗 ) ⊆ ∪ ran 𝑓
127 ssun1 ⊢ ∪ ran 𝑓 ⊆ ( ∪ ran 𝑓 ∪ ran 𝐷 )
128 126 127 sstri ⊢ ( 𝑓 ‘ 𝑗 ) ⊆ ( ∪ ran 𝑓 ∪ ran 𝐷 )
129 id ⊢ ( 𝑧 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → 𝑧 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) )
130 128 129 sseqtrrid ⊢ ( 𝑧 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 )
131 pm5.5 ⊢ ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ↔ ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) )
132 130 131 syl ⊢ ( 𝑧 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ↔ ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) )
133 reseq2 ⊢ ( 𝑧 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) = ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) )
134 133 oveq2d ⊢ ( 𝑧 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) = ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) )
135 134 eleq1d ⊢ ( 𝑧 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ↔ ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) )
136 132 135 bitrd ⊢ ( 𝑧 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ↔ ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) )
137 136 rspcv ⊢ ( ( ∪ ran 𝑓 ∪ ran 𝐷 ) ∈ ( 𝒫 𝐶 ∩ Fin ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) )
138 125 137 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) )
139 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → 𝐺 ∈ CMnd )
140 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
141 139 140 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → 𝐺 ∈ Mnd )
142 simplr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → 𝑗 ∈ 𝐾 )
143 119 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ∪ ran 𝑓 ∪ ran 𝐷 ) ∈ Fin )
144 102 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ∪ ran 𝑓 ∪ ran 𝐷 ) ⊆ 𝐶 )
145 144 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) → 𝑘 ∈ 𝐶 )
146 6 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) → 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 )
147 146 22 jca ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) → ( 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 ∧ 𝑗 ∈ 𝐴 ) )
148 29 3expa ⊢ ( ( ( 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐶 ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
149 147 148 sylan ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑘 ∈ 𝐶 ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
150 149 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ 𝐶 ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
151 145 150 syldan ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
152 151 fmpttd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑗 𝐹 𝑘 ) ) : ( ∪ ran 𝑓 ∪ ran 𝐷 ) ⟶ 𝐵 )
153 eqid ⊢ ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑗 𝐹 𝑘 ) ) = ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑗 𝐹 𝑘 ) )
154 ovexd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) → ( 𝑗 𝐹 𝑘 ) ∈ V )
155 10 fvexi ⊢ 0 ∈ V
156 155 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → 0 ∈ V )
157 153 143 154 156 fsuppmptdm ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑗 𝐹 𝑘 ) ) finSupp 0 )
158 1 10 139 143 152 157 gsumcl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐺 Σg ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ∈ 𝐵 )
159 velsn ⊢ ( 𝑦 ∈ { 𝑗 } ↔ 𝑦 = 𝑗 )
160 ovres ⊢ ( ( 𝑦 ∈ { 𝑗 } ∧ 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) → ( 𝑦 ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) 𝑘 ) = ( 𝑦 𝐹 𝑘 ) )
161 159 160 sylanbr ⊢ ( ( 𝑦 = 𝑗 ∧ 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) → ( 𝑦 ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) 𝑘 ) = ( 𝑦 𝐹 𝑘 ) )
162 oveq1 ⊢ ( 𝑦 = 𝑗 → ( 𝑦 𝐹 𝑘 ) = ( 𝑗 𝐹 𝑘 ) )
163 162 adantr ⊢ ( ( 𝑦 = 𝑗 ∧ 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) → ( 𝑦 𝐹 𝑘 ) = ( 𝑗 𝐹 𝑘 ) )
164 161 163 eqtrd ⊢ ( ( 𝑦 = 𝑗 ∧ 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) → ( 𝑦 ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) 𝑘 ) = ( 𝑗 𝐹 𝑘 ) )
165 164 mpteq2dva ⊢ ( 𝑦 = 𝑗 → ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑦 ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) 𝑘 ) ) = ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑗 𝐹 𝑘 ) ) )
166 165 oveq2d ⊢ ( 𝑦 = 𝑗 → ( 𝐺 Σg ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑦 ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) 𝑘 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) )
167 1 166 gsumsn ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑗 ∈ 𝐾 ∧ ( 𝐺 Σg ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑦 ∈ { 𝑗 } ↦ ( 𝐺 Σg ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑦 ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) 𝑘 ) ) ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) )
168 141 142 158 167 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐺 Σg ( 𝑦 ∈ { 𝑗 } ↦ ( 𝐺 Σg ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑦 ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) 𝑘 ) ) ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) )
169 snfi ⊢ { 𝑗 } ∈ Fin
170 169 a1i ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → { 𝑗 } ∈ Fin )
171 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → 𝐹 : ( 𝐴 × 𝐶 ) ⟶ 𝐵 )
172 22 adantr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → 𝑗 ∈ 𝐴 )
173 172 snssd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → { 𝑗 } ⊆ 𝐴 )
174 xpss12 ⊢ ( ( { 𝑗 } ⊆ 𝐴 ∧ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ⊆ 𝐶 ) → ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ⊆ ( 𝐴 × 𝐶 ) )
175 173 144 174 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ⊆ ( 𝐴 × 𝐶 ) )
176 171 175 fssresd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) : ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ⟶ 𝐵 )
177 xpfi ⊢ ( ( { 𝑗 } ∈ Fin ∧ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ∈ Fin ) → ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ∈ Fin )
178 169 143 177 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ∈ Fin )
179 176 178 156 fdmfifsupp ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) finSupp 0 )
180 1 10 139 170 143 176 179 gsumxp ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) = ( 𝐺 Σg ( 𝑦 ∈ { 𝑗 } ↦ ( 𝐺 Σg ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑦 ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) 𝑘 ) ) ) ) ) )
181 144 resmptd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) = ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑗 𝐹 𝑘 ) ) )
182 181 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) )
183 168 180 182 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) )
184 183 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ↔ ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) )
185 ovex ⊢ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ∈ V
186 76 185 elrnmpti ⊢ ( ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ↔ ∃ 𝑔 ∈ 𝐿 ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) = ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) )
187 isabl ⊢ ( 𝐺 ∈ Abel ↔ ( 𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd ) )
188 48 2 187 sylanbrc ⊢ ( 𝜑 → 𝐺 ∈ Abel )
189 188 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑔 ∈ 𝐿 ) → 𝐺 ∈ Abel )
190 22 42 syldan ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) → ( 𝐻 ‘ 𝑗 ) ∈ 𝐵 )
191 190 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑔 ∈ 𝐿 ) → ( 𝐻 ‘ 𝑗 ) ∈ 𝐵 )
192 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → 𝐿 ⊆ 𝐵 )
193 192 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑔 ∈ 𝐿 ) → 𝑔 ∈ 𝐵 )
194 1 12 189 191 193 ablnncan ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑔 ∈ 𝐿 ) → ( ( 𝐻 ‘ 𝑗 ) − ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) = 𝑔 )
195 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑔 ∈ 𝐿 ) → 𝑔 ∈ 𝐿 )
196 194 195 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑔 ∈ 𝐿 ) → ( ( 𝐻 ‘ 𝑗 ) − ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ∈ 𝐿 )
197 oveq2 ⊢ ( ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) = ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) → ( ( 𝐻 ‘ 𝑗 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) = ( ( 𝐻 ‘ 𝑗 ) − ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) )
198 197 eleq1d ⊢ ( ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) = ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) → ( ( ( 𝐻 ‘ 𝑗 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ↔ ( ( 𝐻 ‘ 𝑗 ) − ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ∈ 𝐿 ) )
199 196 198 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑔 ∈ 𝐿 ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) = ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) → ( ( 𝐻 ‘ 𝑗 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ) )
200 199 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ∃ 𝑔 ∈ 𝐿 ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) = ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) → ( ( 𝐻 ‘ 𝑗 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ) )
201 186 200 syl5bi ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) → ( ( 𝐻 ‘ 𝑗 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ) )
202 184 201 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) → ( ( 𝐻 ‘ 𝑗 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ) )
203 138 202 syld ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐾 ) ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) → ( ( 𝐻 ‘ 𝑗 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ) )
204 203 an32s ⊢ ( ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑗 ∈ 𝐾 ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) → ( ( 𝐻 ‘ 𝑗 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ) )
205 204 ralimdva ⊢ ( ( 𝜑 ∧ 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ) → ( ∀ 𝑗 ∈ 𝐾 ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) → ∀ 𝑗 ∈ 𝐾 ( ( 𝐻 ‘ 𝑗 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ) )
206 205 impr ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ∧ ∀ 𝑗 ∈ 𝐾 ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ) ) → ∀ 𝑗 ∈ 𝐾 ( ( 𝐻 ‘ 𝑗 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 )
207 fveq2 ⊢ ( 𝑗 = 𝑥 → ( 𝐻 ‘ 𝑗 ) = ( 𝐻 ‘ 𝑥 ) )
208 sneq ⊢ ( 𝑗 = 𝑥 → { 𝑗 } = { 𝑥 } )
209 208 xpeq1d ⊢ ( 𝑗 = 𝑥 → ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) = ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) )
210 209 reseq2d ⊢ ( 𝑗 = 𝑥 → ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) = ( 𝐹 ↾ ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) )
211 210 oveq2d ⊢ ( 𝑗 = 𝑥 → ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) )
212 207 211 oveq12d ⊢ ( 𝑗 = 𝑥 → ( ( 𝐻 ‘ 𝑗 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) = ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) )
213 212 eleq1d ⊢ ( 𝑗 = 𝑥 → ( ( ( 𝐻 ‘ 𝑗 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ↔ ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ) )
214 213 cbvralvw ⊢ ( ∀ 𝑗 ∈ 𝐾 ( ( 𝐻 ‘ 𝑗 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑗 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ↔ ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 )
215 206 214 sylib ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ∧ ∀ 𝑗 ∈ 𝐾 ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ) ) → ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 )
216 sseq2 ⊢ ( 𝑛 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( ran 𝐷 ⊆ 𝑛 ↔ ran 𝐷 ⊆ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) )
217 xpeq2 ⊢ ( 𝑛 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( { 𝑥 } × 𝑛 ) = ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) )
218 217 reseq2d ⊢ ( 𝑛 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) = ( 𝐹 ↾ ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) )
219 218 oveq2d ⊢ ( 𝑛 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) )
220 219 oveq2d ⊢ ( 𝑛 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) = ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) )
221 220 eleq1d ⊢ ( 𝑛 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝐿 ↔ ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ) )
222 221 ralbidv ⊢ ( 𝑛 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝐿 ↔ ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ) )
223 216 222 anbi12d ⊢ ( 𝑛 = ( ∪ ran 𝑓 ∪ ran 𝐷 ) → ( ( ran 𝐷 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝐿 ) ↔ ( ran 𝐷 ⊆ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ) ) )
224 223 rspcev ⊢ ( ( ( ∪ ran 𝑓 ∪ ran 𝐷 ) ∈ ( 𝒫 𝐶 ∩ Fin ) ∧ ( ran 𝐷 ⊆ ( ∪ ran 𝑓 ∪ ran 𝐷 ) ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × ( ∪ ran 𝑓 ∪ ran 𝐷 ) ) ) ) ) ∈ 𝐿 ) ) → ∃ 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ran 𝐷 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝐿 ) )
225 122 124 215 224 syl12anc ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐾 ⟶ ( 𝒫 𝐶 ∩ Fin ) ∧ ∀ 𝑗 ∈ 𝐾 ∀ 𝑧 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝑓 ‘ 𝑗 ) ⊆ 𝑧 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐶 ↦ ( 𝑗 𝐹 𝑘 ) ) ↾ 𝑧 ) ) ∈ ran ( 𝑔 ∈ 𝐿 ↦ ( ( 𝐻 ‘ 𝑗 ) − 𝑔 ) ) ) ) ) → ∃ 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ran 𝐷 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝐿 ) )
226 88 225 exlimddv ⊢ ( 𝜑 → ∃ 𝑛 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ran 𝐷 ⊆ 𝑛 ∧ ∀ 𝑥 ∈ 𝐾 ( ( 𝐻 ‘ 𝑥 ) − ( 𝐺 Σg ( 𝐹 ↾ ( { 𝑥 } × 𝑛 ) ) ) ) ∈ 𝐿 ) )