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 ⊢ φ → F : A ⟶ B
gsumcllem.a ⊢ φ → A ∈ V
gsumcllem.z ⊢ φ → Z ∈ U
gsumcllem.s ⊢ φ → F supp Z ⊆ W
Assertion gsumcllem ⊢ φ ∧ W = ∅ → F = k ∈ A ⟼ Z

Proof

Step Hyp Ref Expression
1 gsumcllem.f ⊢ φ → F : A ⟶ B
2 gsumcllem.a ⊢ φ → A ∈ V
3 gsumcllem.z ⊢ φ → Z ∈ U
4 gsumcllem.s ⊢ φ → F supp Z ⊆ W
5 1 feqmptd ⊢ φ → F = k ∈ A ⟼ F ⁡ k
6 5 adantr ⊢ φ ∧ W = ∅ → F = k ∈ A ⟼ F ⁡ k
7 difeq2 ⊢ W = ∅ → A ∖ W = A ∖ ∅
8 dif0 ⊢ A ∖ ∅ = A
9 7 8 eqtrdi ⊢ W = ∅ → A ∖ W = A
10 9 eleq2d ⊢ W = ∅ → k ∈ A ∖ W ↔ k ∈ A
11 10 biimpar ⊢ W = ∅ ∧ k ∈ A → k ∈ A ∖ W
12 1 4 2 3 suppssr ⊢ φ ∧ k ∈ A ∖ W → F ⁡ k = Z
13 11 12 sylan2 ⊢ φ ∧ W = ∅ ∧ k ∈ A → F ⁡ k = Z
14 13 anassrs ⊢ φ ∧ W = ∅ ∧ k ∈ A → F ⁡ k = Z
15 14 mpteq2dva ⊢ φ ∧ W = ∅ → k ∈ A ⟼ F ⁡ k = k ∈ A ⟼ Z
16 6 15 eqtrd ⊢ φ ∧ W = ∅ → F = k ∈ A ⟼ Z