Theorem gsumcllem

Description: Lemma for gsumcl and related theorems. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 24-Apr-2016) (Revised by AV, 31-May-2019)

	Ref	Expression
Hypotheses	gsumcllem.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	gsumcllem.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsumcllem.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
	gsumcllem.s	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
Assertion	gsumcllem	⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumcllem.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		gsumcllem.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		gsumcllem.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
4		gsumcllem.s	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
5	1	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
6	5	adantr	⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) )
7		difeq2	⊢ ( 𝑊 = ∅ → ( 𝐴 ∖ 𝑊 ) = ( 𝐴 ∖ ∅ ) )
8		dif0	⊢ ( 𝐴 ∖ ∅ ) = 𝐴
9	7 8	eqtrdi	⊢ ( 𝑊 = ∅ → ( 𝐴 ∖ 𝑊 ) = 𝐴 )
10	9	eleq2d	⊢ ( 𝑊 = ∅ → ( 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ↔ 𝑘 ∈ 𝐴 ) )
11	10	biimpar	⊢ ( ( 𝑊 = ∅ ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) )
12	1 4 2 3	suppssr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
13	11 12	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑊 = ∅ ∧ 𝑘 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
14	13	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑊 = ∅ ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
15	14	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → ( 𝑘 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝐴 ↦ 𝑍 ) )
16	6 15	eqtrd	⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ 𝑍 ) )