Step |
Hyp |
Ref |
Expression |
1 |
|
gsumsplit2.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
gsumsplit2.z |
⊢ 0 = ( 0g ‘ 𝐺 ) |
3 |
|
gsumsplit2.p |
⊢ + = ( +g ‘ 𝐺 ) |
4 |
|
gsumsplit2.g |
⊢ ( 𝜑 → 𝐺 ∈ CMnd ) |
5 |
|
gsumsplit2.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
6 |
|
gsumsplit2.f |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 ) |
7 |
|
gsumsplit2.w |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp 0 ) |
8 |
|
gsumsplit2.i |
⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ ) |
9 |
|
gsumsplit2.u |
⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) ) |
10 |
6
|
fmpttd |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) : 𝐴 ⟶ 𝐵 ) |
11 |
1 2 3 4 5 10 7 8 9
|
gsumsplit |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐶 ) ) + ( 𝐺 Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐷 ) ) ) ) |
12 |
|
ssun1 |
⊢ 𝐶 ⊆ ( 𝐶 ∪ 𝐷 ) |
13 |
12 9
|
sseqtrrid |
⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 ) |
14 |
13
|
resmptd |
⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐶 ) = ( 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) |
15 |
14
|
oveq2d |
⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐶 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) ) |
16 |
|
ssun2 |
⊢ 𝐷 ⊆ ( 𝐶 ∪ 𝐷 ) |
17 |
16 9
|
sseqtrrid |
⊢ ( 𝜑 → 𝐷 ⊆ 𝐴 ) |
18 |
17
|
resmptd |
⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐷 ) = ( 𝑘 ∈ 𝐷 ↦ 𝑋 ) ) |
19 |
18
|
oveq2d |
⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐷 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐷 ↦ 𝑋 ) ) ) |
20 |
15 19
|
oveq12d |
⊢ ( 𝜑 → ( ( 𝐺 Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐶 ) ) + ( 𝐺 Σg ( ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ↾ 𝐷 ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ 𝐷 ↦ 𝑋 ) ) ) ) |
21 |
11 20
|
eqtrd |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ 𝐷 ↦ 𝑋 ) ) ) ) |