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 = ( 0_g ‘ 𝐺 )
	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 = ( 0_g ‘ 𝐺 )
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	ffvelcdmda	⊢ ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 ) → ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) ∈ 𝐵 )
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	eqtrid	⊢ ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 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 → ( 2^nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) : ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑗 } ) )
146	115 145	mp1i	⊢ ( 𝜑 → ( 2^nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) : ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) –1-1-onto→ ( 𝐴 “ { 𝑗 } ) )
147	1 2 3 114 122 144 146	gsumf1o	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) = ( 𝐺 Σ_g ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ∘ ( 2^nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) ) ) )
148		1st2nd2	⊢ ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
149		xp1st	⊢ ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → ( 1^st ‘ 𝑥 ) ∈ { 𝑗 } )
150		elsni	⊢ ( ( 1^st ‘ 𝑥 ) ∈ { 𝑗 } → ( 1^st ‘ 𝑥 ) = 𝑗 )
151	149 150	syl	⊢ ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → ( 1^st ‘ 𝑥 ) = 𝑗 )
152	151	opeq1d	⊢ ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ = ⟨ 𝑗 , ( 2^nd ‘ 𝑥 ) ⟩ )
153	148 152	eqtrd	⊢ ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → 𝑥 = ⟨ 𝑗 , ( 2^nd ‘ 𝑥 ) ⟩ )
154	153	fveq2d	⊢ ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ⟨ 𝑗 , ( 2^nd ‘ 𝑥 ) ⟩ ) )
155		df-ov	⊢ ( 𝑗 𝐹 ( 2^nd ‘ 𝑥 ) ) = ( 𝐹 ‘ ⟨ 𝑗 , ( 2^nd ‘ 𝑥 ) ⟩ )
156	154 155	eqtr4di	⊢ ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝑗 𝐹 ( 2^nd ‘ 𝑥 ) ) )
157	156	mpteq2ia	⊢ ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 𝑗 𝐹 ( 2^nd ‘ 𝑥 ) ) )
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	⊢ ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) → ( 2^nd ‘ 𝑥 ) ∈ ( 𝐴 “ { 𝑗 } ) )
168	167	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) → ( 2^nd ‘ 𝑥 ) ∈ ( 𝐴 “ { 𝑗 } ) )
169		fo2nd	⊢ 2^nd : V –onto→ V
170		fof	⊢ ( 2^nd : V –onto→ V → 2^nd : V ⟶ V )
171	169 170	mp1i	⊢ ( 𝜑 → 2^nd : V ⟶ V )
172	171	feqmptd	⊢ ( 𝜑 → 2^nd = ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) )
173	172	reseq1d	⊢ ( 𝜑 → ( 2^nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) = ( ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) )
174		ssv	⊢ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ⊆ V
175		resmpt	⊢ ( ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ⊆ V → ( ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) = ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 2^nd ‘ 𝑥 ) ) )
176	174 175	ax-mp	⊢ ( ( 𝑥 ∈ V ↦ ( 2^nd ‘ 𝑥 ) ) ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) = ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 2^nd ‘ 𝑥 ) )
177	173 176	eqtrdi	⊢ ( 𝜑 → ( 2^nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) = ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 2^nd ‘ 𝑥 ) ) )
178		eqidd	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) = ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) )
179		oveq2	⊢ ( 𝑘 = ( 2^nd ‘ 𝑥 ) → ( 𝑗 𝐹 𝑘 ) = ( 𝑗 𝐹 ( 2^nd ‘ 𝑥 ) ) )
180	168 177 178 179	fmptco	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ∘ ( 2^nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) ) = ( 𝑥 ∈ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ↦ ( 𝑗 𝐹 ( 2^nd ‘ 𝑥 ) ) ) )
181	157 166 180	3eqtr4a	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ↾ { 𝑗 } ) ) = ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ∘ ( 2^nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) ) )
182	181	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐴 ↾ { 𝑗 } ) ) ) = ( 𝐺 Σ_g ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ∘ ( 2^nd ↾ ( { 𝑗 } × ( 𝐴 “ { 𝑗 } ) ) ) ) ) )
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	imbitrrid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 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 ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ) ) )

Metamath Proof Explorer

Theorem gsum2dlem2

Proof