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

Metamath Proof Explorer

Theorem gsum2dlem1

Description: Lemma 1 for gsum2d . (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 8-Jun-2019)

Ref Expression
Hypotheses gsum2d.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsum2d.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsum2d.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsum2d.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsum2d.r ⊢ ( 𝜑 → Rel 𝐴 )
gsum2d.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
gsum2d.s ⊢ ( 𝜑 → dom 𝐴 ⊆ 𝐷 )
gsum2d.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsum2d.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion gsum2dlem1 ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 gsum2d.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsum2d.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsum2d.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsum2d.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 gsum2d.r ⊢ ( 𝜑 → Rel 𝐴 )
6 gsum2d.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
7 gsum2d.s ⊢ ( 𝜑 → dom 𝐴 ⊆ 𝐷 )
8 gsum2d.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
9 gsum2d.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
10 imaexg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 “ { 𝑗 } ) ∈ V )
11 4 10 syl ⊢ ( 𝜑 → ( 𝐴 “ { 𝑗 } ) ∈ V )
12 vex ⊢ 𝑗 ∈ V
13 vex ⊢ 𝑘 ∈ V
14 12 13 elimasn ⊢ ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↔ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 )
15 df-ov ⊢ ( 𝑗 𝐹 𝑘 ) = ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ )
16 8 ffvelcdmda ⊢ ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 ) → ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) ∈ 𝐵 )
17 15 16 eqeltrid ⊢ ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
18 14 17 sylan2b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ) → ( 𝑗 𝐹 𝑘 ) ∈ 𝐵 )
19 18 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) : ( 𝐴 “ { 𝑗 } ) ⟶ 𝐵 )
20 9 fsuppimpd ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ∈ Fin )
21 rnfi ⊢ ( ( 𝐹 supp 0 ) ∈ Fin → ran ( 𝐹 supp 0 ) ∈ Fin )
22 20 21 syl ⊢ ( 𝜑 → ran ( 𝐹 supp 0 ) ∈ Fin )
23 14 biimpi ⊢ ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 )
24 12 13 opelrn ⊢ ( ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) → 𝑘 ∈ ran ( 𝐹 supp 0 ) )
25 24 con3i ⊢ ( ¬ 𝑘 ∈ ran ( 𝐹 supp 0 ) → ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) )
26 23 25 anim12i ⊢ ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ∧ ¬ 𝑘 ∈ ran ( 𝐹 supp 0 ) ) → ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 ∧ ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) ) )
27 eldif ⊢ ( 𝑘 ∈ ( ( 𝐴 “ { 𝑗 } ) ∖ ran ( 𝐹 supp 0 ) ) ↔ ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ∧ ¬ 𝑘 ∈ ran ( 𝐹 supp 0 ) ) )
28 eldif ⊢ ( ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ↔ ( ⟨ 𝑗 , 𝑘 ⟩ ∈ 𝐴 ∧ ¬ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐹 supp 0 ) ) )
29 26 27 28 3imtr4i ⊢ ( 𝑘 ∈ ( ( 𝐴 “ { 𝑗 } ) ∖ ran ( 𝐹 supp 0 ) ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) )
30 ssidd ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ ( 𝐹 supp 0 ) )
31 2 fvexi ⊢ 0 ∈ V
32 31 a1i ⊢ ( 𝜑 → 0 ∈ V )
33 8 30 4 32 suppssr ⊢ ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝐹 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = 0 )
34 15 33 eqtrid ⊢ ( ( 𝜑 ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝐴 ∖ ( 𝐹 supp 0 ) ) ) → ( 𝑗 𝐹 𝑘 ) = 0 )
35 29 34 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝐴 “ { 𝑗 } ) ∖ ran ( 𝐹 supp 0 ) ) ) → ( 𝑗 𝐹 𝑘 ) = 0 )
36 35 11 suppss2 ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) supp 0 ) ⊆ ran ( 𝐹 supp 0 ) )
37 22 36 ssfid ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) supp 0 ) ∈ Fin )
38 1 2 3 11 19 37 gsumcl2 ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 “ { 𝑗 } ) ↦ ( 𝑗 𝐹 𝑘 ) ) ) ∈ 𝐵 )