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

Metamath Proof Explorer

Theorem gsum2dlem2

Proof