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