Metamath Proof Explorer

Theorem fsumsupp0

Description: Finite sum of function values, for a function of finite support. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses fsumsupp0.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumsupp0.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
Assertion fsumsupp0 ( 𝜑 → Σ 𝑘 ∈ ( 𝐹 supp 0 ) ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) )

Proof

Step Hyp Ref Expression
1 fsumsupp0.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fsumsupp0.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
4 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
5 suppvalfn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin ∧ 0 ∈ ℝ ) → ( 𝐹 supp 0 ) = { 𝑘 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑘 ) ≠ 0 } )
6 3 1 4 5 syl3anc ⊢ ( 𝜑 → ( 𝐹 supp 0 ) = { 𝑘 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑘 ) ≠ 0 } )
7 ssrab2 ⊢ { 𝑘 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑘 ) ≠ 0 } ⊆ 𝐴
8 6 7 eqsstrdi ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝐴 )
9 2 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐹 supp 0 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
10 8 sselda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐹 supp 0 ) ) → 𝑘 ∈ 𝐴 )
11 9 10 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐹 supp 0 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
12 eldifi ⊢ ( 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) → 𝑘 ∈ 𝐴 )
13 12 adantr ⊢ ( ( 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 0 ) → 𝑘 ∈ 𝐴 )
14 neqne ⊢ ( ¬ ( 𝐹 ‘ 𝑘 ) = 0 → ( 𝐹 ‘ 𝑘 ) ≠ 0 )
15 14 adantl ⊢ ( ( 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 0 ) → ( 𝐹 ‘ 𝑘 ) ≠ 0 )
16 13 15 jca ⊢ ( ( 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 0 ) → ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 0 ) )
17 rabid ⊢ ( 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑘 ) ≠ 0 } ↔ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 0 ) )
18 16 17 sylibr ⊢ ( ( 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 0 ) → 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑘 ) ≠ 0 } )
19 18 adantll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 0 ) → 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑘 ) ≠ 0 } )
20 6 eleq2d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐹 supp 0 ) ↔ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑘 ) ≠ 0 } ) )
21 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 0 ) → ( 𝑘 ∈ ( 𝐹 supp 0 ) ↔ 𝑘 ∈ { 𝑘 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑘 ) ≠ 0 } ) )
22 19 21 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 0 ) → 𝑘 ∈ ( 𝐹 supp 0 ) )
23 eldifn ⊢ ( 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) → ¬ 𝑘 ∈ ( 𝐹 supp 0 ) )
24 23 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ) ∧ ¬ ( 𝐹 ‘ 𝑘 ) = 0 ) → ¬ 𝑘 ∈ ( 𝐹 supp 0 ) )
25 22 24 condan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ‘ 𝑘 ) = 0 )
26 8 11 25 1 fsumss ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝐹 supp 0 ) ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ 𝐴 ( 𝐹 ‘ 𝑘 ) )