Theorem gsum2dlem1

Description: Lemma 1 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	gsum2dlem1	⊢ ( 𝜑 → ( 𝐺 Σ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		imaexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 “ { 𝑗 } ) ∈ V )
11	4 10	syl	⊢ ( 𝜑 → ( 𝐴 “ { 𝑗 } ) ∈ V )
12		vex	⊢ 𝑗 ∈ V
13		vex	⊢ 𝑘 ∈ V
14	12 13	elimasn	⊢ ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↔ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 )
15		df-ov	⊢ ( 𝑗 𝐹 𝑘 ) = ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ )
16	8	ffvelrnda	⊢ ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 ) → ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) ∈ 𝐵 )
17	15 16	eqeltrid	⊢ ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
18	14 17	sylan2b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
19	18	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) : ( 𝐴 “ { 𝑗 } ) ⟶ 𝐵 )
20	9	fsuppimpd	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
21		rnfi	⊢ ( ( 𝐹 supp 0 ) ∈ Fin → ran ( 𝐹 supp 0 ) ∈ Fin )
22	20 21	syl	⊢ ( 𝜑 → ran ( 𝐹 supp 0 ) ∈ Fin )
23	14	biimpi	⊢ ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 )
24	12 13	opelrn	⊢ ( ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) → 𝑘 ∈ ran ( 𝐹 supp 0 ) )
25	24	con3i	⊢ ( ¬ 𝑘 ∈ ran ( 𝐹 supp 0 ) → ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) )
26	23 25	anim12i	⊢ ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ∧ ¬ 𝑘 ∈ ran ( 𝐹 supp 0 ) ) → ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 ∧ ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) ) )
27		eldif	⊢ ( 𝑘 ∈ ( ( 𝐴 “ { 𝑗 } ) ∖ ran ( 𝐹 supp 0 ) ) ↔ ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ∧ ¬ 𝑘 ∈ ran ( 𝐹 supp 0 ) ) )
28		eldif	⊢ ( ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ↔ ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 ∧ ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) ) )
29	26 27 28	3imtr4i	⊢ ( 𝑘 ∈ ( ( 𝐴 “ { 𝑗 } ) ∖ ran ( 𝐹 supp 0 ) ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) )
30		ssidd	⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
31	2	fvexi	⊢ 0 ∈ V
32	31	a1i	⊢ ( 𝜑 → 0 ∈ V )
33	8 30 4 32	suppssr	⊢ ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = 0 )
34	15 33	syl5eq	⊢ ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝑗 𝐹 𝑘 ) = 0 )
35	29 34	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐴 “ { 𝑗 } ) ∖ ran ( 𝐹 supp 0 ) ) ) → ( 𝑗 𝐹 𝑘 ) = 0 )
36	35 11	suppss2	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) supp 0 ) ⊆ ran ( 𝐹 supp 0 ) )
37	22 36	ssfid	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) supp 0 ) ∈ Fin )
38	1 2 3 11 19 37	gsumcl2	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ∈ 𝐵 )