Description: Split a group sum expressed as mapping with a finite domain into two parts using restrictions. (Contributed by AV, 23-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsummptfidmsplit.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
gsummptfidmsplit.p | ⊢ + = ( +g ‘ 𝐺 ) | ||
gsummptfidmsplit.g | ⊢ ( 𝜑 → 𝐺 ∈ CMnd ) | ||
gsummptfidmsplit.a | ⊢ ( 𝜑 → 𝐴 ∈ Fin ) | ||
gsummptfidmsplit.y | ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 ) | ||
gsummptfidmsplit.i | ⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ ) | ||
gsummptfidmsplit.u | ⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) ) | ||
gsummptfidmsplitres.f | ⊢ 𝐹 = ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) | ||
Assertion | gsummptfidmsplitres | ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) + ( 𝐺 Σg ( 𝐹 ↾ 𝐷 ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gsummptfidmsplit.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
2 | gsummptfidmsplit.p | ⊢ + = ( +g ‘ 𝐺 ) | |
3 | gsummptfidmsplit.g | ⊢ ( 𝜑 → 𝐺 ∈ CMnd ) | |
4 | gsummptfidmsplit.a | ⊢ ( 𝜑 → 𝐴 ∈ Fin ) | |
5 | gsummptfidmsplit.y | ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 ) | |
6 | gsummptfidmsplit.i | ⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ ) | |
7 | gsummptfidmsplit.u | ⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) ) | |
8 | gsummptfidmsplitres.f | ⊢ 𝐹 = ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) | |
9 | eqid | ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) | |
10 | 5 8 | fmptd | ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 ) |
11 | fvexd | ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ V ) | |
12 | 8 4 5 11 | fsuppmptdm | ⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝐺 ) ) |
13 | 1 9 2 3 4 10 12 6 7 | gsumsplit | ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) + ( 𝐺 Σg ( 𝐹 ↾ 𝐷 ) ) ) ) |