Metamath Proof Explorer


Theorem gsum2dlem2

Description: Lemma for gsum2d . (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 8-Jun-2019)

Ref Expression
Hypotheses gsum2d.b 𝐵 = ( Base ‘ 𝐺 )
gsum2d.z 0 = ( 0g𝐺 )
gsum2d.g ( 𝜑𝐺 ∈ CMnd )
gsum2d.a ( 𝜑𝐴𝑉 )
gsum2d.r ( 𝜑 → Rel 𝐴 )
gsum2d.d ( 𝜑𝐷𝑊 )
gsum2d.s ( 𝜑 → dom 𝐴𝐷 )
gsum2d.f ( 𝜑𝐹 : 𝐴𝐵 )
gsum2d.w ( 𝜑𝐹 finSupp 0 )
Assertion gsum2dlem2 ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ dom ( 𝐹 supp 0 ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsum2d.b 𝐵 = ( Base ‘ 𝐺 )
2 gsum2d.z 0 = ( 0g𝐺 )
3 gsum2d.g ( 𝜑𝐺 ∈ CMnd )
4 gsum2d.a ( 𝜑𝐴𝑉 )
5 gsum2d.r ( 𝜑 → Rel 𝐴 )
6 gsum2d.d ( 𝜑𝐷𝑊 )
7 gsum2d.s ( 𝜑 → dom 𝐴𝐷 )
8 gsum2d.f ( 𝜑𝐹 : 𝐴𝐵 )
9 gsum2d.w ( 𝜑𝐹 finSupp 0 )
10 9 fsuppimpd ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
11 dmfi ( ( 𝐹 supp 0 ) ∈ Fin → dom ( 𝐹 supp 0 ) ∈ Fin )
12 10 11 syl ( 𝜑 → dom ( 𝐹 supp 0 ) ∈ Fin )
13 reseq2 ( 𝑥 = ∅ → ( 𝐴𝑥 ) = ( 𝐴 ↾ ∅ ) )
14 res0 ( 𝐴 ↾ ∅ ) = ∅
15 13 14 eqtrdi ( 𝑥 = ∅ → ( 𝐴𝑥 ) = ∅ )
16 15 reseq2d ( 𝑥 = ∅ → ( 𝐹 ↾ ( 𝐴𝑥 ) ) = ( 𝐹 ↾ ∅ ) )
17 res0 ( 𝐹 ↾ ∅ ) = ∅
18 16 17 eqtrdi ( 𝑥 = ∅ → ( 𝐹 ↾ ( 𝐴𝑥 ) ) = ∅ )
19 18 oveq2d ( 𝑥 = ∅ → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑥 ) ) ) = ( 𝐺 Σg ∅ ) )
20 mpteq1 ( 𝑥 = ∅ → ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) = ( 𝑗 ∈ ∅ ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) )
21 mpt0 ( 𝑗 ∈ ∅ ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) = ∅
22 20 21 eqtrdi ( 𝑥 = ∅ → ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) = ∅ )
23 22 oveq2d ( 𝑥 = ∅ → ( 𝐺 Σg ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) = ( 𝐺 Σg ∅ ) )
24 19 23 eqeq12d ( 𝑥 = ∅ → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑥 ) ) ) = ( 𝐺 Σg ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ↔ ( 𝐺 Σg ∅ ) = ( 𝐺 Σg ∅ ) ) )
25 24 imbi2d ( 𝑥 = ∅ → ( ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑥 ) ) ) = ( 𝐺 Σg ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) ↔ ( 𝜑 → ( 𝐺 Σg ∅ ) = ( 𝐺 Σg ∅ ) ) ) )
26 reseq2 ( 𝑥 = 𝑦 → ( 𝐴𝑥 ) = ( 𝐴𝑦 ) )
27 26 reseq2d ( 𝑥 = 𝑦 → ( 𝐹 ↾ ( 𝐴𝑥 ) ) = ( 𝐹 ↾ ( 𝐴𝑦 ) ) )
28 27 oveq2d ( 𝑥 = 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑥 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑦 ) ) ) )
29 mpteq1 ( 𝑥 = 𝑦 → ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) = ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) )
30 29 oveq2d ( 𝑥 = 𝑦 → ( 𝐺 Σg ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) = ( 𝐺 Σg ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )
31 28 30 eqeq12d ( 𝑥 = 𝑦 → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑥 ) ) ) = ( 𝐺 Σg ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑦 ) ) ) = ( 𝐺 Σg ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) )
32 31 imbi2d ( 𝑥 = 𝑦 → ( ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑥 ) ) ) = ( 𝐺 Σg ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) ↔ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑦 ) ) ) = ( 𝐺 Σg ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) ) )
33 reseq2 ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐴𝑥 ) = ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) )
34 33 reseq2d ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐹 ↾ ( 𝐴𝑥 ) ) = ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) )
35 34 oveq2d ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑥 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ) )
36 mpteq1 ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) = ( 𝑗 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) )
37 36 oveq2d ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝐺 Σg ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )
38 35 37 eqeq12d ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑥 ) ) ) = ( 𝐺 Σg ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) )
39 38 imbi2d ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑥 ) ) ) = ( 𝐺 Σg ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) ↔ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) ) )
40 reseq2 ( 𝑥 = dom ( 𝐹 supp 0 ) → ( 𝐴𝑥 ) = ( 𝐴 ↾ dom ( 𝐹 supp 0 ) ) )
41 40 reseq2d ( 𝑥 = dom ( 𝐹 supp 0 ) → ( 𝐹 ↾ ( 𝐴𝑥 ) ) = ( 𝐹 ↾ ( 𝐴 ↾ dom ( 𝐹 supp 0 ) ) ) )
42 41 oveq2d ( 𝑥 = dom ( 𝐹 supp 0 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑥 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ dom ( 𝐹 supp 0 ) ) ) ) )
43 mpteq1 ( 𝑥 = dom ( 𝐹 supp 0 ) → ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) = ( 𝑗 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) )
44 43 oveq2d ( 𝑥 = dom ( 𝐹 supp 0 ) → ( 𝐺 Σg ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )
45 42 44 eqeq12d ( 𝑥 = dom ( 𝐹 supp 0 ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑥 ) ) ) = ( 𝐺 Σg ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ dom ( 𝐹 supp 0 ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) )
46 45 imbi2d ( 𝑥 = dom ( 𝐹 supp 0 ) → ( ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑥 ) ) ) = ( 𝐺 Σg ( 𝑗𝑥 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) ↔ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ dom ( 𝐹 supp 0 ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) ) )
47 eqidd ( 𝜑 → ( 𝐺 Σg ∅ ) = ( 𝐺 Σg ∅ ) )
48 oveq1 ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑦 ) ) ) = ( 𝐺 Σg ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑦 ) ) ) ( +g𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) ) = ( ( 𝐺 Σg ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ( +g𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) ) )
49 eqid ( +g𝐺 ) = ( +g𝐺 )
50 3 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → 𝐺 ∈ CMnd )
51 4 resexd ( 𝜑 → ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ∈ V )
52 51 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ∈ V )
53 resss ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ⊆ 𝐴
54 fssres ( ( 𝐹 : 𝐴𝐵 ∧ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) : ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ⟶ 𝐵 )
55 8 53 54 sylancl ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) : ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ⟶ 𝐵 )
56 55 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) : ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ⟶ 𝐵 )
57 8 ffund ( 𝜑 → Fun 𝐹 )
58 57 funresd ( 𝜑 → Fun ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) )
59 58 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → Fun ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) )
60 10 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( 𝐹 supp 0 ) ∈ Fin )
61 8 4 fexd ( 𝜑𝐹 ∈ V )
62 2 fvexi 0 ∈ V
63 ressuppss ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
64 61 62 63 sylancl ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
65 64 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
66 60 65 ssfid ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) supp 0 ) ∈ Fin )
67 61 resexd ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ V )
68 isfsupp ( ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) finSupp 0 ↔ ( Fun ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∧ ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) supp 0 ) ∈ Fin ) ) )
69 67 62 68 sylancl ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) finSupp 0 ↔ ( Fun ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∧ ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) supp 0 ) ∈ Fin ) ) )
70 69 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) finSupp 0 ↔ ( Fun ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ∧ ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) supp 0 ) ∈ Fin ) ) )
71 59 66 70 mpbir2and ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) finSupp 0 )
72 simprr ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ¬ 𝑧𝑦 )
73 disjsn ( ( 𝑦 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧𝑦 )
74 72 73 sylibr ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( 𝑦 ∩ { 𝑧 } ) = ∅ )
75 74 reseq2d ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( 𝐴 ↾ ( 𝑦 ∩ { 𝑧 } ) ) = ( 𝐴 ↾ ∅ ) )
76 resindi ( 𝐴 ↾ ( 𝑦 ∩ { 𝑧 } ) ) = ( ( 𝐴𝑦 ) ∩ ( 𝐴 ↾ { 𝑧 } ) )
77 75 76 14 3eqtr3g ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( ( 𝐴𝑦 ) ∩ ( 𝐴 ↾ { 𝑧 } ) ) = ∅ )
78 resundi ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( 𝐴𝑦 ) ∪ ( 𝐴 ↾ { 𝑧 } ) )
79 78 a1i ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) = ( ( 𝐴𝑦 ) ∪ ( 𝐴 ↾ { 𝑧 } ) ) )
80 1 2 49 50 52 56 71 77 79 gsumsplit ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ) = ( ( 𝐺 Σg ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ↾ ( 𝐴𝑦 ) ) ) ( +g𝐺 ) ( 𝐺 Σg ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) ) )
81 ssun1 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } )
82 ssres2 ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( 𝐴𝑦 ) ⊆ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) )
83 resabs1 ( ( 𝐴𝑦 ) ⊆ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) → ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ↾ ( 𝐴𝑦 ) ) = ( 𝐹 ↾ ( 𝐴𝑦 ) ) )
84 81 82 83 mp2b ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ↾ ( 𝐴𝑦 ) ) = ( 𝐹 ↾ ( 𝐴𝑦 ) )
85 84 oveq2i ( 𝐺 Σg ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ↾ ( 𝐴𝑦 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑦 ) ) )
86 ssun2 { 𝑧 } ⊆ ( 𝑦 ∪ { 𝑧 } )
87 ssres2 ( { 𝑧 } ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( 𝐴 ↾ { 𝑧 } ) ⊆ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) )
88 resabs1 ( ( 𝐴 ↾ { 𝑧 } ) ⊆ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) → ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ↾ ( 𝐴 ↾ { 𝑧 } ) ) = ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) )
89 86 87 88 mp2b ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ↾ ( 𝐴 ↾ { 𝑧 } ) ) = ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) )
90 89 oveq2i ( 𝐺 Σg ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) )
91 85 90 oveq12i ( ( 𝐺 Σg ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ↾ ( 𝐴𝑦 ) ) ) ( +g𝐺 ) ( 𝐺 Σg ( ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) ) = ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑦 ) ) ) ( +g𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) )
92 80 91 eqtrdi ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ) = ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑦 ) ) ) ( +g𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) ) )
93 simprl ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → 𝑦 ∈ Fin )
94 1 2 3 4 5 6 7 8 9 gsum2dlem1 ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ∈ 𝐵 )
95 94 ad2antrr ( ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) ∧ 𝑗𝑦 ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ∈ 𝐵 )
96 vex 𝑧 ∈ V
97 96 a1i ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → 𝑧 ∈ V )
98 sneq ( 𝑗 = 𝑧 → { 𝑗 } = { 𝑧 } )
99 98 imaeq2d ( 𝑗 = 𝑧 → ( 𝐴 “ { 𝑗 } ) = ( 𝐴 “ { 𝑧 } ) )
100 oveq1 ( 𝑗 = 𝑧 → ( 𝑗 𝐹 𝑘 ) = ( 𝑧 𝐹 𝑘 ) )
101 99 100 mpteq12dv ( 𝑗 = 𝑧 → ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) = ( 𝑘 ∈ ( 𝐴 “ { 𝑧 } ) ↦ ( 𝑧 𝐹 𝑘 ) ) )
102 101 oveq2d ( 𝑗 = 𝑧 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑧 } ) ↦ ( 𝑧 𝐹 𝑘 ) ) ) )
103 102 eleq1d ( 𝑗 = 𝑧 → ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ∈ 𝐵 ↔ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑧 } ) ↦ ( 𝑧 𝐹 𝑘 ) ) ) ∈ 𝐵 ) )
104 103 imbi2d ( 𝑗 = 𝑧 → ( ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ∈ 𝐵 ) ↔ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑧 } ) ↦ ( 𝑧 𝐹 𝑘 ) ) ) ∈ 𝐵 ) ) )
105 104 94 chvarvv ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑧 } ) ↦ ( 𝑧 𝐹 𝑘 ) ) ) ∈ 𝐵 )
106 105 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑧 } ) ↦ ( 𝑧 𝐹 𝑘 ) ) ) ∈ 𝐵 )
107 1 49 50 93 95 97 72 106 102 gsumunsn ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( 𝐺 Σg ( 𝑗 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) = ( ( 𝐺 Σg ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ( +g𝐺 ) ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑧 } ) ↦ ( 𝑧 𝐹 𝑘 ) ) ) ) )
108 98 reseq2d ( 𝑗 = 𝑧 → ( 𝐴 ↾ { 𝑗 } ) = ( 𝐴 ↾ { 𝑧 } ) )
109 108 reseq2d ( 𝑗 = 𝑧 → ( 𝐹 ↾ ( 𝐴 ↾ { 𝑗 } ) ) = ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) )
110 109 oveq2d ( 𝑗 = 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑗 } ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) )
111 102 110 eqeq12d ( 𝑗 = 𝑧 → ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑗 } ) ) ) ↔ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑧 } ) ↦ ( 𝑧 𝐹 𝑘 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) ) )
112 111 imbi2d ( 𝑗 = 𝑧 → ( ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑗 } ) ) ) ) ↔ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑧 } ) ↦ ( 𝑧 𝐹 𝑘 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) ) ) )
113 imaexg ( 𝐴𝑉 → ( 𝐴 “ { 𝑗 } ) ∈ V )
114 4 113 syl ( 𝜑 → ( 𝐴 “ { 𝑗 } ) ∈ V )
115 vex 𝑗 ∈ V
116 vex 𝑘 ∈ V
117 115 116 elimasn ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↔ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 )
118 df-ov ( 𝑗 𝐹 𝑘 ) = ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ )
119 8 ffvelrnda ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 ) → ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) ∈ 𝐵 )
120 118 119 eqeltrid ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
121 117 120 sylan2b ( ( 𝜑𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
122 121 fmpttd ( 𝜑 → ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) : ( 𝐴 “ { 𝑗 } ) ⟶ 𝐵 )
123 funmpt Fun ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) )
124 123 a1i ( 𝜑 → Fun ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) )
125 rnfi ( ( 𝐹 supp 0 ) ∈ Fin → ran ( 𝐹 supp 0 ) ∈ Fin )
126 10 125 syl ( 𝜑 → ran ( 𝐹 supp 0 ) ∈ Fin )
127 117 biimpi ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 )
128 115 116 opelrn ( ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) → 𝑘 ∈ ran ( 𝐹 supp 0 ) )
129 128 con3i ( ¬ 𝑘 ∈ ran ( 𝐹 supp 0 ) → ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) )
130 127 129 anim12i ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ∧ ¬ 𝑘 ∈ ran ( 𝐹 supp 0 ) ) → ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 ∧ ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) ) )
131 eldif ( 𝑘 ∈ ( ( 𝐴 “ { 𝑗 } ) ∖ ran ( 𝐹 supp 0 ) ) ↔ ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ∧ ¬ 𝑘 ∈ ran ( 𝐹 supp 0 ) ) )
132 eldif ( ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ↔ ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 ∧ ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) ) )
133 130 131 132 3imtr4i ( 𝑘 ∈ ( ( 𝐴 “ { 𝑗 } ) ∖ ran ( 𝐹 supp 0 ) ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) )
134 ssidd ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
135 62 a1i ( 𝜑0 ∈ V )
136 8 134 4 135 suppssr ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = 0 )
137 118 136 syl5eq ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝑗 𝐹 𝑘 ) = 0 )
138 133 137 sylan2 ( ( 𝜑𝑘 ∈ ( ( 𝐴 “ { 𝑗 } ) ∖ ran ( 𝐹 supp 0 ) ) ) → ( 𝑗 𝐹 𝑘 ) = 0 )
139 138 114 suppss2 ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) supp 0 ) ⊆ ran ( 𝐹 supp 0 ) )
140 126 139 ssfid ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) supp 0 ) ∈ Fin )
141 114 mptexd ( 𝜑 → ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ∈ V )
142 isfsupp ( ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ∈ V ∧ 0 ∈ V ) → ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) finSupp 0 ↔ ( Fun ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ∧ ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) supp 0 ) ∈ Fin ) ) )
143 141 62 142 sylancl ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) finSupp 0 ↔ ( Fun ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ∧ ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) supp 0 ) ∈ Fin ) ) )
144 124 140 143 mpbir2and ( 𝜑 → ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) finSupp 0 )
145 2ndconst ( 𝑗 ∈ V → ( 2nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) : ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑗 } ) )
146 115 145 mp1i ( 𝜑 → ( 2nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) : ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑗 } ) )
147 1 2 3 114 122 144 146 gsumf1o ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) = ( 𝐺 Σg ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ∘ ( 2nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) ) ) )
148 1st2nd2 ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → 𝑥 = ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ )
149 xp1st ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → ( 1st𝑥 ) ∈ { 𝑗 } )
150 elsni ( ( 1st𝑥 ) ∈ { 𝑗 } → ( 1st𝑥 ) = 𝑗 )
151 149 150 syl ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → ( 1st𝑥 ) = 𝑗 )
152 151 opeq1d ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → ⟨ ( 1st𝑥 ) , ( 2nd𝑥 ) ⟩ = ⟨ 𝑗 , ( 2nd𝑥 ) ⟩ )
153 148 152 eqtrd ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → 𝑥 = ⟨ 𝑗 , ( 2nd𝑥 ) ⟩ )
154 153 fveq2d ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → ( 𝐹𝑥 ) = ( 𝐹 ‘ ⟨ 𝑗 , ( 2nd𝑥 ) ⟩ ) )
155 df-ov ( 𝑗 𝐹 ( 2nd𝑥 ) ) = ( 𝐹 ‘ ⟨ 𝑗 , ( 2nd𝑥 ) ⟩ )
156 154 155 eqtr4di ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → ( 𝐹𝑥 ) = ( 𝑗 𝐹 ( 2nd𝑥 ) ) )
157 156 mpteq2ia ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 𝐹𝑥 ) ) = ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 𝑗 𝐹 ( 2nd𝑥 ) ) )
158 8 feqmptd ( 𝜑𝐹 = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) )
159 158 reseq1d ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ↾ { 𝑗 } ) ) = ( ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) ↾ ( 𝐴 ↾ { 𝑗 } ) ) )
160 resss ( 𝐴 ↾ { 𝑗 } ) ⊆ 𝐴
161 resmpt ( ( 𝐴 ↾ { 𝑗 } ) ⊆ 𝐴 → ( ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) ↾ ( 𝐴 ↾ { 𝑗 } ) ) = ( 𝑥 ∈ ( 𝐴 ↾ { 𝑗 } ) ↦ ( 𝐹𝑥 ) ) )
162 160 161 ax-mp ( ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) ↾ ( 𝐴 ↾ { 𝑗 } ) ) = ( 𝑥 ∈ ( 𝐴 ↾ { 𝑗 } ) ↦ ( 𝐹𝑥 ) )
163 ressn ( 𝐴 ↾ { 𝑗 } ) = ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) )
164 163 mpteq1i ( 𝑥 ∈ ( 𝐴 ↾ { 𝑗 } ) ↦ ( 𝐹𝑥 ) ) = ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 𝐹𝑥 ) )
165 162 164 eqtri ( ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) ↾ ( 𝐴 ↾ { 𝑗 } ) ) = ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 𝐹𝑥 ) )
166 159 165 eqtrdi ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ↾ { 𝑗 } ) ) = ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 𝐹𝑥 ) ) )
167 xp2nd ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → ( 2nd𝑥 ) ∈ ( 𝐴 “ { 𝑗 } ) )
168 167 adantl ( ( 𝜑𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) → ( 2nd𝑥 ) ∈ ( 𝐴 “ { 𝑗 } ) )
169 fo2nd 2nd : V –onto→ V
170 fof ( 2nd : V –onto→ V → 2nd : V ⟶ V )
171 169 170 mp1i ( 𝜑 → 2nd : V ⟶ V )
172 171 feqmptd ( 𝜑 → 2nd = ( 𝑥 ∈ V ↦ ( 2nd𝑥 ) ) )
173 172 reseq1d ( 𝜑 → ( 2nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) = ( ( 𝑥 ∈ V ↦ ( 2nd𝑥 ) ) ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) )
174 ssv ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ⊆ V
175 resmpt ( ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ⊆ V → ( ( 𝑥 ∈ V ↦ ( 2nd𝑥 ) ) ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) = ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 2nd𝑥 ) ) )
176 174 175 ax-mp ( ( 𝑥 ∈ V ↦ ( 2nd𝑥 ) ) ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) = ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 2nd𝑥 ) )
177 173 176 eqtrdi ( 𝜑 → ( 2nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) = ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 2nd𝑥 ) ) )
178 eqidd ( 𝜑 → ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) = ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) )
179 oveq2 ( 𝑘 = ( 2nd𝑥 ) → ( 𝑗 𝐹 𝑘 ) = ( 𝑗 𝐹 ( 2nd𝑥 ) ) )
180 168 177 178 179 fmptco ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ∘ ( 2nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) ) = ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 𝑗 𝐹 ( 2nd𝑥 ) ) ) )
181 157 166 180 3eqtr4a ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ↾ { 𝑗 } ) ) = ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ∘ ( 2nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) ) )
182 181 oveq2d ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑗 } ) ) ) = ( 𝐺 Σg ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ∘ ( 2nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) ) ) )
183 147 182 eqtr4d ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑗 } ) ) ) )
184 112 183 chvarvv ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑧 } ) ↦ ( 𝑧 𝐹 𝑘 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) )
185 184 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑧 } ) ↦ ( 𝑧 𝐹 𝑘 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) )
186 185 oveq2d ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( ( 𝐺 Σg ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ( +g𝐺 ) ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑧 } ) ↦ ( 𝑧 𝐹 𝑘 ) ) ) ) = ( ( 𝐺 Σg ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ( +g𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) ) )
187 107 186 eqtrd ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( 𝐺 Σg ( 𝑗 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) = ( ( 𝐺 Σg ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ( +g𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) ) )
188 92 187 eqeq12d ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ↔ ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑦 ) ) ) ( +g𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) ) = ( ( 𝐺 Σg ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ( +g𝐺 ) ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ { 𝑧 } ) ) ) ) ) )
189 48 188 syl5ibr ( ( 𝜑 ∧ ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑦 ) ) ) = ( 𝐺 Σg ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) )
190 189 expcom ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) → ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑦 ) ) ) = ( 𝐺 Σg ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) ) )
191 190 a2d ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧𝑦 ) → ( ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴𝑦 ) ) ) = ( 𝐺 Σg ( 𝑗𝑦 ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) → ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ ( 𝑦 ∪ { 𝑧 } ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ ( 𝑦 ∪ { 𝑧 } ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) ) )
192 25 32 39 46 47 191 findcard2s ( dom ( 𝐹 supp 0 ) ∈ Fin → ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ dom ( 𝐹 supp 0 ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) ) )
193 12 192 mpcom ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ↾ dom ( 𝐹 supp 0 ) ) ) ) = ( 𝐺 Σg ( 𝑗 ∈ dom ( 𝐹 supp 0 ) ↦ ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )