This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝜑 ∧ 𝑊 = ∅ ) → 𝐹 = ( 𝑘 ∈ 𝐴 ↦ 𝑍 ) )